Preview

Моделирование и анализ информационных систем

Расширенный поиск

LTL-спецификация ограниченных счётчиковых машин

https://doi.org/10.18255/1818-1015-2022-1-44-59

Полный текст:

Аннотация

В статье пересматриваются результаты работы, посвящённой задаче представления поведения программной системы в виде набора формул линейной темпоральной логики LTL с последующим использованием этого представления для проверки выполнимости программных свойств системы через процедуру доказательства справедливости логических выводов, выраженных в терминах логики LTL. В качестве программных систем, для спецификации поведения которых применяется логика LTL, рассматриваются счётчиковые машины Минского с ограничениями. Ранее при работе с темпоральной логикой LTL как с программной логикой фактически был введён специальный псевдооператор обращения к предыдущим значениям переменных, задействованных в элементарных высказываниях. Несмотря на то что этот псевдооператор легко реализуется в верификаторе Cadence SMV при доказательстве справедливости логических LTL-выводов, классическое определение логики LTL не предполагает его наличия. В данной статье для построения LTL-спецификации поведения ограниченной счётчиковой машины будут использоваться только бинарные переменные, а отслеживание их предыдущих значений будет осуществляться исключительно в рамках самой логики LTL посредством соответствующих формул.

Об авторе

Егор Владимирович Кузьмин
Ярославский государственный университет им. П. Г. Демидова
Россия


Список литературы

1. E. V. Kuzmin, “LTL-Specification of Counter Machines”, in Russian, Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104-119, 2021.

2. M. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, Inc., 1967.

3. R. Schroeppel, “A Two Counter Machine Cannot Calculate 2N ”, Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972, p. 32.

4. E. V. Kuzmin, Counter Machines, in Russian. Yaroslavl: Yaroslavl State University, 2010, p. 128.

5. Cadence SMV. [Online]. Available: http://www.kenmcmil.com/smv.html.

6. A. Pnueli, “The Temporal Logic of Programs”, in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE Computer Society Press, 1977, pp. 46-57.

7. E. M. Clarke, O. Grumberg, and D. A. Peled, Model Checking. The MIT Press, 2001.

8. C. Baier and J.-P. Katoen, Principles of Model Checking. The MIT Press, 2008.

9. G. Priest, An Introduction to Non-Classical Logic. From if to is. Cambridge University Press, 2008, p. 648.

10. E. V. Kuzmin, Non-Classical Propositional Logics, in Russian. Yaroslavl: P.G. Demidov Yaroslavl State University, 2016, p. 160.

11. E. Clarke, O. Grumberg, and K. Hamaguchi, “Another Look at LTL Model Checking”, Carnegie Mellon University, Tech. Rep. CMU-CS-94-114, 1994.


Рецензия

Для цитирования:


Кузьмин Е.В. LTL-спецификация ограниченных счётчиковых машин. Моделирование и анализ информационных систем. 2022;29(1):44-59. https://doi.org/10.18255/1818-1015-2022-1-44-59

For citation:


Kuzmin E.V. LTL-Specification of Bounded Counter Machines. Modeling and Analysis of Information Systems. 2022;29(1):44-59. (In Russ.) https://doi.org/10.18255/1818-1015-2022-1-44-59

Просмотров: 122


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)