Preview

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

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

О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени

https://doi.org/10.18255/1818-1015-2021-4-356-371

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

Аннотация

К последовательным реагирующим системам относятся компьютерные программы и вычислительные устройства, которые обрабатывают потоки входных данных или сигналов управления и генерируют на выходе последовательности команд или результатов вычислений. Для проектирования таких систем полезно иметь формальные языки спецификаций, способные выражать отношения между входными и выходными потоками данных. В предшествующих работах нами было предложено семейство таких языков спецификаций, представляющих собой расширение темпоральных логик $LTL$, $CTL$ и $CTL^*$ за счет использования регулярных языков в качестве параметров темпоральных операторов. Мы провели сравнительный анализ выразительных возможностей нового расширения темпоральной логики линейного времени $Reg$-$LTL$ и предложили алгоритмы верификации моделей для новых расширений логик $Reg$-$LTL$, $Reg$-$CTL$, и $Reg$-$CTL^*$. Однако вопрос о сложности задач верификации моделей и проверки выполнимости формул указанных логик оставался открытым. В этой статье мы восполняем этот пробел в наших исследованиях и показываем, что для темпоральной логики $Reg$-$LTL$ обе задачи являются Pspace-полными. Вычислительная трудность рассматриваемых задач легко доказывается сведением к ним проблемы пустоты пересечения семейств регулярных языков. Основным результатом статьи является алгоритм сведения задачи проверки выполнимости формул логики $Reg$-$LTL$ к проблеме пустоты автоматов Бюхи сравнительно небольшого размера и описание стратегии, позволяющей проверять пустоту полученных автоматов с использованием объема памяти, полиномального относительно размера исходных формул.

Об авторах

Антон Романович Гнатенко
Национальный исследовательский университет “Высшая школа экономики”
Россия


Владимир Анатольевич Захаров
Национальный исследовательский университет “Высшая школа экономики”;Институт системного программирования им. В. П. Иванникова РАН
Россия


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

1. A. Pnueli, “The temporal logic of programs,” in Proceedings of the 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46-57.

2. D. Gabbay, A. Pnueli, S. Shelach, and J. Stavi, “The temporal analysis of fairness,” in Proceedings of 7-th ACM Symposium on Principles of Programming Languages, 1980, pp. 163-173.

3. M. Ben-Ari, Z. Manna, and A. Pnueli, “The temporal logic of branching time,” in Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1981, pp. 164-176.

4. J. Ouaknine and J. Worrell, “Some recent results in Metric Temporal Logic,” in Proceedings of the 6th International Conference Formal Modeling and Analysis of Timed Systems, 2008, pp. 1-13.

5. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.

6. P. Wolper, “Temporal Logic Can Be More Expressive,” Information and Control, vol. 56, pp. 72-99, 1983.

7. T. French, “Quantified propositional temporal logic with repeating states,” in Proceedings of the 10th International Symposium on Temporal Representation and Reasoning, 2003, pp. 155-165.

8. J. J. Henriksen and P. S. Thiagarajan, “Dynamic linear time temporal logic,” Annals of Pure and Applied Logic, vol. 96, pp. 187-207, 1999.

9. G. De Giacomo and M. Y. Vardi, “Linear temporal logic and linear dynamic logic on finite traces,” in Proceedings of the 23th International Joint Conference on Artificial Intelligence, 2013, pp. 854-860.

10. A. Artale, R. Konchakov, V. Ryzhikov, and M. Zakharyaschev, “Tractable interval temporal propositional and description logics,” in Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, pp. 1417-1423.

11. S. Merz, M. Wirsing, and J. Zappe, “A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems,” in Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering, 2003, pp. 87-101.

12. C. Baier and J. Katoen, Principles of Model Checking. MIT Press, 2008.

13. E. M. Clarke, O. Gramberg, and D. A. Peled, Model Checking. MIT Press, 1999.

14. D. G. Kozlova and V. A. Zakharov, “On the model checking of sequential reactive systems,” in Proceedings of the 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, 2016, vol. 1698, pp. 376-389.

15. A. R. Gnatenko and V. A. Zakharov, “On the verification of finite transducers over semigroups,” Proceedings of ISP RAS, vol. 30, pp. 303-324, 2018.

16. A. Gnatenko and V. Zakharov, “On the Model Checking Problem for Some Extension of CTL*,” Modeling and Analysis of Information Systems, vol. 27, pp. 428-441, 2020.

17. A. Gnatenko and V. Zakharov, “On the Expressive Power of Some Extensions of Linear Temporal Logic,” Modeling and Analysis of Information Systems, vol. 25, pp. 506-524, 2018.

18. M. Y. Vardi and P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification,” in Proceedings of the First Symposium on Logic in Computer Science, 1986, pp. 322-331.

19. J. A. W. Kamp, Tense Logic and the Theory of Linear Order, PhD thesis. University of California, Los Angeles, 1968.

20. K. Etessami and T. Wilke, “An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic,” Information and Computation, vol. 160, pp. 88-108, 2000.

21. M. Leucker and C. Sanchez, “Regular Linear Temporal Logic,” in Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, 2007, pp. 291-305.

22. O. Kupferman, N. Piterman, and M. Y. Vardi, “Extended Temporal Logic Revisited,” in Proceedings of 12-th International Conference on Concurrency Theory, 2001, pp. 519-535.

23. A. R. Gnatenko and V. A. Zakharov, “O slozhnosti verifikatsii avtomatov-preobrazovateley nad kommutativnymi polugruppami,” in Trudy 18 Mezhdunarodnoj konferentsii Problemy teoreticheskoy kibernetiki, 2017, pp. 68-70.

24. V. A. Zakharov and G. G. Temerbekova, “On the Minimization of Finite State Transducers over Semigroups,” Modeling and Analysis of Information Systems, vol. 23, pp. 741-753, 2016.

25. V. A. Zakharov, “Equivalence checking problem for finite state transducers over semigroups,” in Proceedings of the 6-th International Conference on Algebraic Informatics, 2015, pp. 208-221.

26. J. M. Fisher and R. E. Ladner, “Propositional Dynamic Logic of Regular Programs,” Journal of Computer and System Sciences, vol. 18, pp. 194-211, 1979.

27. W. J. Savitch, “Relationships between nondeterministic and deterministic tape complexities,” Journal of Computer and System Science, vol. 4, pp. 177-192, 1970.

28. D. Kozen, “Lower bounds for natural proof systems,” in Proceedings of the 18th International Symposium on the Foundations of Computer Science, 1977, pp. 254-266.


Рецензия

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


Гнатенко А.Р., Захаров В.А. О верификации моделей и проверке выполнимости формул одного параметрического расширения темпоральной логики линейного времени. Моделирование и анализ информационных систем. 2021;28(4):356-371. https://doi.org/10.18255/1818-1015-2021-4-356-371

For citation:


Gnatenko A.R., Zakharov V.A. On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic. Modeling and Analysis of Information Systems. 2021;28(4):356-371. (In Russ.) https://doi.org/10.18255/1818-1015-2021-4-356-371

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


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


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