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
Просмотров:
493
Послать статью по эл. почте 