Preview

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

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

О задаче верификации моделей программ для одного расширения логики CTL*

https://doi.org/10.18255/1818-1015-2020-4-428-441

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

Аннотация

К последовательным реагирующим системам относятся программы и устройства, которые работают с двумя потоками данных и осуществляют преобразование входных потоков данных в выходные потоки. К числу таких систем обработки информации относятся контроллеры, драйверы устройств, компьютерные интерпретаторы. Результатом работы таких вычислительных систем являются бесконечные последовательности пар событий типа запрос-отклик, и поэтому в качестве математических моделей для них наиболее часто используются конечные автоматы-преобразователи. Поведение автоматов-преобразователей представлено бинарными отношениями на бесконечных последовательностях, и традиционные прикладные темпоральные логики (HML, LTL, CTL, mu-исчисление) плохо подходят для этой цели, поскольку для интерпретации их формул используются omega-языки, а не бинарные отношения на omega-словах. Чтобы предоставить темпоральным логикам возможность определять свойства преобразований, которые характеризуют поведение реагирующих систем, мы ввели новые расширения этих логик, имеющие две отличительные особенности: 1) темпоральные операторы в расширениях этих логик параметризованы, и в качестве параметров используются языки в входном алфавите автоматов-преобразователей; 2) в качестве базовых предикатов используются языки в выходном алфавите автоматов-преобразователей. Ранее нами были исследованы выразительные возможности новых расширений Reg-LTL и Reg-CTL известных темпоральных логик линейного и ветвящегося времени LTL и CTL, в которых для параметризации темпоральных операторов и задания базовых предикатов разрешалось использовать только регулярные языки. Мы обнаружили, что такая параметризация увеличивает выразительные возможности темпоральной логики, но сохраняет разрешимость задачи проверки выполнимости формул на конечных моделях. Для указанных выше логик нами были разработаны алгоритмы верификации конечных автоматов-преобразователей. На следующем этапе изучения новых расширений темпоральной логики, предназначенных для спецификации и верификации последовательных реагирующих систем, мы обратились к задаче верификации этих систем с использованием темпоральной логики Reg-CTL*, которая является расширением обобщенной логики деревьев вычислений CTL*. В этой статье описан алгоритм проверки выполнимости формул Reg-CTL* на моделях конечных автоматов-преобразователей и показано, что эта задача принадлежит классу сложности ExpSpace.

Об авторах

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

Студент



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

Доктор физико-математических наук, профессор



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

1. R. Alur and P. Cerny, «Streaming transducers for algorithmic verification of single-pass list-processing programs», in Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2011, pp. 599-610.

2. Q. Hu and L. D'Antoni, «Automatic program inversion using symbolic transducers», in Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2017, pp. 376-389.

3. M. Veanes, P. Hooimeijer, B. Livshits, D. Molnar, and N. Bjorner, «Symbolic finite state transducers: Algorithms and applications», in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 2012, pp. 137-150.

4. A. R. Gnatenko and V. A. Zakharov, «On the Expressive Power of Some Extensions of Linear Temporal Logic», Automatic Control and Computer Sciences, vol. 53, no. 7, pp. 663-675, 2019.

5. D. G. Zakharov, V. A. Kozlova, and D. Kozlova, «On the model checking of sequential reactive systems», in Proceedings of the 25-th International Workshop on Concurrency, Specification and Programming, Rostock, Germany, September 28-30, vol. 1698, 2016, pp. 233-244.

6. A. R. Gnatenko and V. A. Zakharov, «On the model checking of finite state transducers over semigroups», Proceedings of ISP RAS, vol. 30, no. 3, pp. 303-324, 2018.

7. E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking. MIT press, 1999.

8. A. R. Gnatenko, «On the complexity of model checking problem for finite state transducers over free semigroups», in Proceedings of the Student Session of European Summer School on Logic, Language and Information, Riga, 2019.

9. J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.

10. D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, «On the temporal analysis of fairness», in Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles ofprogramming languages, 1980, pp. 163-173.

11. Z. Manna and P. Wolper, «Synthesis of communicating processes from temporal logic specifications», in Workshop on Logic of Programs, Springer, vol. 131, 1981, pp. 253-281.

12. P. Wolper, «Temporal Logic Can Be More Expressive», Information and control, vol. 56, no. 1-2, pp. 72-99, 1983.

13. O. Kupferman, N. Piterman, and M. Y. Vardi, «Extended temporal logic revisited», in Proceedings of 12-th International Conference on Concurrency Theory, Springer, 2001, pp. 519-535.

14. M. Y. Vardi and P. Wolper, «Yet another process logic», in Lecture Notes in Computer Science, Springer, vol. 14, 1983, pp. 501-512.

15. M. Y. Vardi, «A Temporal Fixpoint Calculus», in Proceedings of the 15-th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1988, pp. 250-259.

16. J. G. Henriksen and P. S. Thiagarajan, «Dynamic linear time temporal logic», Annals of Pure and Applied logic, vol. 96, no. 1-3, pp. 187-207, 1999.

17. M. Leucker and C. Sanchez, «Regular Linear Temporal Logic», in Proceedings of the 4-th International colloquium on theoretical aspects ofcomputing, Springer, 2007, pp. 291-305.

18. R. Mateescu, P. T. Monteiro, E. Dumas, and H. De Jong, «CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks», Theoretical Computer Science, vol. 412, no. 26, pp. 2854-2883, 2011.

19. R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper, «Simple on-the-fly automatic verification of linear temporal logic», in International Conference on Protocol Specification, Testing and Verification, Springer, 1995, pp. 3-18.

20. 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, IEEE Computer Society, 1986, pp. 322-331.

21. W. J. Savitch, «Relationships between nondeterministic and deterministic tape complexities», Journal of computer and system sciences, vol. 4, no. 2, pp. 177-192, 1970.

22. D. Kozen, «Lower bounds for natural proof systems», in Proceedings of the 18-th Symp. on the Foundations of ComputerScience, IEEE, 1977, pp. 254-266.

23. A. Mader, «A classification of PLC models and applications», in Discrete Event Systems, vol. 569, Springer, 2000, pp. 239-246.

24. T. Ovatman, A. Aral, D. Polat, and A. O. Unver, «An overview of model checking practices on verification of PLC software», Software & Systems Modeling, vol. 15, no. 4, pp. 937-960, 2016.

25. N. Garanina, I. Anureev, V. Zyubin, A. Rozov, T. Liakh, and S. Gorlatch, «Reasoning about Programmable Logic Controllers», System Informatics, vol. 17, pp. 33-42, 2020.

26. E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, «On the expressiveness of the approach to constructing PLC-programs by LTL-specification», Automatic Control and Computer Sciences, vol. 50, no. 7, pp. 510-519, 2016.

27. O. Ljungkrantz, K. Akesson, M. Fabian, and C. Yuan, «A formal specification language for PLC-based control logic», in Proceedings of the 8th IEEE International Conference on Industrial Informatics, IEEE, 2010, pp. 1067-1072.

28. O. Ljungkrantz, K. Akesson, M. Fabian, and A. H. Ebrahimi, «An empirical study of control logic specifications for programmable logic controllers», Empirical Software Engineering, vol. 19, no. 3, pp. 655-677, 2014.


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


Гнатенко А.Р., Захаров В.А. О задаче верификации моделей программ для одного расширения логики CTL*. Моделирование и анализ информационных систем. 2020;27(4):428-441. https://doi.org/10.18255/1818-1015-2020-4-428-441

For citation:


Gnatenko A.R., Zakharov V.A. On the Model Checking Problem for Some Extension of CTL*. Modeling and Analysis of Information Systems. 2020;27(4):428-441. (In Russ.) https://doi.org/10.18255/1818-1015-2020-4-428-441

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


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


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