?
Темпоральная логика для верификации автоматов-преобразователей
С. 204-206.
Zakharov V., Козлова Д. Г.
Language:
Russian
In book
М. : Изд-во механико-математического факультета МГУ, 2016
Гнатенко А. Р., Zakharov V., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 131-133.
The expressive power of a new variant of temporal logic LP-CTL * is studied. In this logic, two classes of LP-1-LTL and LP-n-LTL formulas were distinguished and it was shown that the LP-1-LTL fragment more expressive than the known temporal logic of linear time LTL, and the LP-n-LTL fragment has the same expressive possibilities as ...
Added: June 14, 2018
Gnatenko A., Zakharov V., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 263-266.
Описаны синтаксис и семантика нового расширения Reg-CTL* темпоральной логики деревьев вычислений CTL*, предназначенного для спецификации и верификации вычислений последовательных реагирующих систем. Поеказано, что задача верификации моделей автоматов-преобразователей относительно выполнимости формул логики CTL* является PSPACE-полной. ...
Added: October 17, 2019
Gnatenko A., Zakharov V., Proceedings of the Institute for System Programming of the RAS 2018 Vol. 30 No. 3 P. 303-324
The syntax and semantics of the new temporal logic LP-CTL * designed for the formal specification of the behavior of sequential responsive programs, modeled by automata-transducers (transducers) over semigroups, are developed. An algorithm is developed for verifying the feasibility of the formulas of the proposed temporal logic on models represented by finite transducers working on ...
Added: June 14, 2018
Zakharov V., Kozlova D., , in : Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, 2016. Vol. 1698.: Humboldt-Universität zu Berlin, 2016. P. 233-244.
By sequential reactive system we mean a program which operates in the interaction with the environment permanently receiving data (requests) from it. At receiving a piece of data a program performs a sequence of actions (response) and displays the current result. Such programs usually arise at implementation of computer drivers, online algorithms, control procedures. Basic ...
Added: October 13, 2016
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2021 Т. 28 № 4 С. 356-371
Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification ...
Added: January 17, 2022
Gnatenko A., Zakharov V., Системная информатика 2020 Vol. 17 P. 21-32
Sequential reactive systems such as controllers, device drivers, computer interpreters operate with two data streams and transform input streams of data (control signals, instructions) into output streams of control signals (instructions, data). Finite state transducers are widely used as an adequate formal model for information processing systems of this kind. Since runs of transducers develop ...
Added: November 9, 2020
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences 2021 Vol. 55 No. 7 P. 776-785
Sequential reactive systems include programs and devices that work with two streams of
data and convert input streams of data into output streams. Such information processing systems
include controllers, device drivers, computer interpreters. The results of operation of such computing
systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite
transducers are most often ...
Added: January 17, 2022
Gnatenko A., Zakharov V., Automatic Control and Computer Sciences, Allerton Press Inc., United States 2019 Vol. 53 No. 7 P. 663-675
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a nite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between ows of control signals ...
Added: October 17, 2019
Zakharov V., Винарский Е. М., В кн. : Материалы XIII Международного семинара "Дискретная математика и ее приложения" имени академика О.Б. Лупанова (Москва, МГУ, 17-22 июня 2019). : М. : Изд-во механико-математического факультета МГУ, 2019. С. 257-260.
Конечные автоматы Мили, представляющие собой простейшую математическую модель преобразования потоковых данных, широко используются во многих областях информатики. Но для некоторых приложений большое значение имеют не только значения обрабатываемых данных и порядок их следования, но также интервалы времени, которые отделяют события, присходящие по ходу вычисления автомата. Такие свойства уже не описывается явно средствами классической теории конечных ...
Added: October 17, 2019
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2018 Т. 25 № 5 С. 506-524
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals ...
Added: October 26, 2018
Zakharov V., Гнатенко А. Р., В кн. : Проблемы теоретической кибернетики: XVIII международная конференция (Пенза, 19-23 июня 2017 г.). : М. : МГУ, МАКС Пресс, 2017. С. 68-71.
В статье в качестве формальной модели последовательных реагирующих систем была предложена модель вычислений конечных автоматов-преобразователей, работающих над полугруппами действий. Для спецификации поведений таких автоматов был предложен специальный вариант темпоральной логики линейного времени LTL-FL (LTL with Formal Languages). Формальные языки (множества конечных слов фиксированных алфавитов) в формулах LTL-FL используются для параметризации темпоральных операторов. В этой же ...
Added: October 22, 2017
Zakharov V., Gnatenko A., , in : Proceedings of 9th Workshop “Program Semantics, Specification and Verification: Theory and Applications" (PSSV-2018), Yaroslavl, Russia, June 21-22, 2018. : Yaroslavl : Ярославский государственный университет им. П.Г. Демидова, 2018. P. 29-36.
One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. A behaviour of such a reactive system displays itself in the correspondence between flows of control signals ...
Added: October 26, 2018
Gnatenko A., Zakharov V., Моделирование и анализ информационных систем 2020 Т. 27 № 4 С. 428-441
Sequential reactive systems include programs and devices that work with two streams of data and convert input streams ofdata into output streams. Such information processing systems include controllers, device drivers, computer interpreters.e result of the operation of such computing systems are innite sequences of pairs of events of the request–responsetype, and, therefore, nite transducers are ...
Added: January 31, 2021
Zakharov V., Temerbekova G., Системная информатика 2016 No. 7 P. 33-44
Finite state transducers over semigroups can be regarded as a formal model of sequential reactive programs. In some cases verification of such programs can be reduced to minimization and equivalence checking problems for this model of computation. To solve efficiently these problems certain requirements are imposed on a semigroup these transducers operate on. Minimization of ...
Added: October 13, 2016
Kamenskikh A. A., Логико-философские штудии 2018 Т. 16 № 1-2 С. 19-20
The work discusses an example of unexpected similarity, in the dissolve of series of logical temporality problems, between some textes of the late Neoplatonists (Iamblichus, Proclus, Damascius) and the last Leo Karsavin's manuscript, "On th Time" (1949). ...
Added: October 13, 2018
Khaitovich D., / Cornell University. Series arXiv "math". 2021. No. 2110.
Added: December 7, 2021
Zakharov V., Темербекова Г. Г., Моделирование и анализ информационных систем 2016 Т. 23 № 6 С. 741-753
Finite state transducers over semigroups are regarded as a formal model of sequential reactive programs that operate in the interaction with the environment. At receiving a piece of data a program performs a sequence of actions and displays the current result. Such programs usually arise at implementation of computer drivers, on-line algorithms, control procedures. In ...
Added: October 13, 2016
Kamenskikh A. A., В кн. : Логика и онтология в византийской догматической полемике. Очерки: Коллективная монография. Т. 19.: СПб. : Центр содействия образованию, 2020. С. 255-275.
The chapter of the collective monograph compares the temporal logics of late Neoplatonism and early Christian tradition; The problems of the genesis of the concept of time as a structure formed by a number of kairos moments, each of which may turn out to be a break point in the time series, are discussed. ...
Added: December 5, 2019
Zakharov V., Джусупекова З., В кн. : Материалы XII Международного семинара "Дискретная математика и её приложения" имени академика О.Б. Лупанова (Москва, МГУ, 20-25 июня 2016г.). : М. : Изд-во механико-математического факультета МГУ, 2016. С. 190-192.
Автоматы-преобразователи в качестве модели последовательных реагирующих программы используются в системном программировании, в компьютерной лингвистике, в криптографии, при проектировании микроэлектронных схем и др. Преобразователь принимает на входе последовательность сигналов и выполняет некоторую последовательность действий, преобразуя тем самым конечные слова входного алфавита в полугрупповое выражение, значения которых и являются результатами вычислений.
Мы рассматриваем автоматы-преобразователи над произвольной полугруппой $S$, ...
Added: October 13, 2016
Popova E., Логико-философские штудии 2022 Vol. 20 No. 1 P. 1-7
There are two approaches to merging temporal and epistemic models. The first one consists in starting with a temporal model and enriching it with epistemic dimension (as temporal epistemic logic), while the second one is supposed to start with an epistemic model introducing temporal dimension (dynamic epistemic logic, epistemic temporal logic). The proposed evolutionary epistemic ...
Added: August 1, 2022
Popova E., , in : Двенадцатые Смирновские чтения: материалы Международной научной конференции, Москва, 24–26 июня 2021 г. : М. : Русское общество истории и философии науки, 2021. P. 134-137.
This paper is concerned with the formalization problem of a wide range of scenarios of how knowledge evolves over time. We focus on combinations of temporal and epistemic modalities reflecting various properties of rational agents’ deliberation. For this purpose, we introduce the model EEM – evolutionary epistemic model. ...
Added: June 28, 2021
Avdoshin S. M., Набебин А. А., М. : ДМК Пресс, 2018
The textbook contains the basic information of formal logical systems. It is Boolean functions, Post’s theorem on functional completeness, the k-valued logic, derivatives of Boolean functions, axiomatic calculi for propositions, for predicates, for sequentions, for resolutions. Programming language Prolog and axiomatic programming language OBJ3 are introduced. Problems of monadic logic, of finite automata and of ...
Added: December 2, 2017
Zakharov V., В кн. : Дискретные модели в теории управляющих систем: Х Международная конференция, Москва и Подмосковье, 23-25 мая 2018 г. : Труды. : МГУ, МАКС Пресс, 2018. С. 128-130.
It is shown how the verification of the equivalence of two-tape deterministic automata can be reduced to the problem of checking the equivalence of weakly nondeterministic finite automata-transformers working on the semigroup of prefix regular languages with the concatenation operation. ...
Added: June 14, 2018