О выразительных возможностях некоторых расширений линейной темпоральной логики

Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Мы полагаем, что для формального описания поведения реагирующих систем такого рода требуются более сложные и выразительные средства спецификации, нежели традиционная темпоральная логика линейного времени LT L. В этой работе рассматривается новый язык формальных спецификаций LP-LT L, представляющий собой расширение темпоральной логики LT L, специально разработанное для описания свойств вычислений автоматов-преобразователей. Темпоральные операторы в формулах LP-LT L снабжены параметрами, в качестве которых используются множества слов (языки), описывающие потоки сигналов управления, поступающих на вход реагирующей системы. Базовые предикаты в формулах LP-LT L также определяются языками в алфавите элементарных действий; эти языки описывают ожидаемую реакцию системы в ответ на воздействия окружающей среды. В более ранних работах авторов этой статьи изучалась задача верификации конечных автоматов-преобразователей относительно спецификаций, представленных формулами логик LP-LT L и LP-CT L. Было показано, что для обеих логик эта задача алгоритмически разрешима. Цель данной работы — оценить выразительные возможности логики LP-LT L и сравнить ее с широко известными логиками, применяющимися в информатике для спецификации реагирующих систем. В логике LP-LT L были выделены два фрагмента LP-1-LT L и LP-n-LT L. Нам удалось установить, что язык спецификаций LP-1-LT L более выразителен, чем LT L, в то время как фрагмент LP-n-LT L обладает точно такими же выразительными возможностями, что и монадическая логика второго порядка S1S.

темпоральные логики, выразительность, спецификация, верификация, автоматы Бюхи, бесконечные слова

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

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

3. Etessami K., Wilke T., "An Until Hierarchy and Other Applications of an EhrenfeuchtFraisse Game for Temporal Logic", Information and Computation, 160:1 (2000), 88-108.

4. Fisher J. M., Ladner R. E., "Propositional dynamic logic of regular programs", Journal of Computer and System Sciences, 18 (1979), 194-211.

5. Gabbay D., Pnueli A., Shelach S., Stavi J., "The temporal analysis of fairness", Proceedings of 7-th ACM Symposium on Principles of Programming Languages, 1980, 163-173.

6. Гнатенко А. Р., Захаров В. А., “О сложности верификации конечных автоматовпреобразователей над коммутативными полугруппами”, Труды 18-й Международной конференции "Проблемы теоретической кибернетики", 2017, 68–70.

7. Гнатенко А. Р., Захаров В. А., “О верификации конечных автоматов-преобразователей над полугруппами”, Труды Института системного программирования РАН, 30:3 (2018), 303–324.

8. Harel D., Kozen D., Parikh P., "Process logic: Expressiveness, decidability, completeness", Journal of Computer and System Science, 25:2 (1982), 144-170.

9. Henriksen J. J., Thiagarajan P. S., "Dynamic linear time temporal logic", Annals of Pure and Applied Logic, 96:1-3 (1999), 187-207.

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

11. Kozlova D. G., Zakharov V. A., "On the model checking of sequential reactive systems", Proceedings of the 25th International Workshop on Concurrency, Specification and Programming (CS&P 2016), CEUR Workshop Proceedings, 1698, 2016, 233-244.

12. Kupferman O., Piterman N., Vardi M. Y., "Extended Temporal Logic Revisited", Proceedings of 12-th International Conference on Concurrency Theory, 2001, 519-535.

13. Leucker M., Sanchez C., "Regular Linear Temporal Logic", Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, 2007, 291-305.

14. Manna Z., Wolper P., "Synthesis of Communicating Processes from Temporal Logic Specifications", Lecture Notes in Computer Science, 131, 1981, 253-281.

15. Thomas W., "Automata on infinite objects", Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, 1990, 133-192.

16. Vardi M. Y., Wolper P., "Yet Another Process Logic", Lecture Notes in Computer Science, 14, 1983, 501-512.

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

18. Vardi M. Y., "A Temporal Fixpoint Calculus", Proceedings of the 15-th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, 1989, 250-259.

19. Wolper P., "Temporal Logic Can Be More Expressive", Information and Control, 56:1-2 (1983), 72-99.

20. Wolper P., Boigelot B., "Verifying systems with infinite but regular state spaces", Lecture Notes in Computer Science, 1427, 1998, 88-97.

21. Zakharov V. A., "Equivalence checking problem for finite state transducers over semigroups", Lecture Notes in Computer Science, 9270, 2015, 208-221.524 Моделирование и анализ информационных систем. Т. 25, № 5 (2018) Modeling and Analysis of Information Systems. Vol. 25, No 5 (2018).

22. Захаров В. А., Темербекова Г. Г., “О минимизации конечных автоматовпреобразователей над полугруппами”, Моделирование и анализ информационных систем, 23:6 (2016), 741–753.

23. Захаров В. А., Жайлауова Ш. Р., “О задаче минимизации последовательных программ”, Моделирование и анализ информационных систем, 24:4 (2017), 415–430.