maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2020-4-428-441mais-1434Research ArticleTheory of ComputingО задаче верификации моделей программ для одного расширения логики CTL*On the Model Checking Problem for Some Extension of CTL*https://orcid.org/0000-0003-1499-2090ГнатенкоАнтон РомановичGnatenkoAnton Romanovich

Студент

Student

gnatenko.cmc@gmail.comhttps://orcid.org/0000-0002-3794-9565ЗахаровВладимир АнатольевичZakharovVladimir Anatolyevich

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

Dr. of Science, professor

zakh@cs.msu.ruНациональный исследовательский университет «Высшая школа экономики»РоссияResearch University Higher School of EconomicsRussian FederationНациональный исследовательский университет «Высшая школа экономики»; Институт системного программирования имени В.П. Иванникова РАНРоссияResearch University Higher School of Economics; Ivannikov Institute for System Programming of the RASRussian Federation202019122020274428441Copyright © Гнатенко А.Р., Захаров В.А., 20202020Гнатенко А.Р., Захаров В.А.Gnatenko A.R., Zakharov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1434

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

Sequential reactive systems include programs and devices that work with two streams of data and convert input streams of data into output streams. Such information processing systems include controllers, device drivers, computer interpreters. The result of the operation of such computing systems are infinite sequences of pairs of events of the request-response type, and, therefore, finite transducers are most often used as formal models for them. The behavior of transducers is represented by binary relations on infinite sequences, and so, traditional applied temporal logics (like HML, LTL, CTL, mu-calculus) are poorly suited as specification languages, since omega-languages, not binary relations on omega-words are used for interpretation of their formulae. To provide temporal logics with the ability to define properties of transformations that characterize the behavior ofreactive systems, we introduced new extensions ofthese logics, which have two distinctive features: 1) temporal operators are parameterized, and languages in the input alphabet oftransducers are used as parameters; 2) languages in the output alphabet oftransducers are used as basic predicates. Previously, we studied the expressive power ofnew extensions Reg-LTL and Reg-CTL ofthe well-known temporal logics oflinear and branching time LTL and CTL, in which it was allowed to use only regular languages for parameterization of temporal operators and basic predicates. We discovered that such a parameterization increases the expressive capabilities oftemporal logic, but preserves the decidability of the model checking problem. For the logics mentioned above, we have developed algorithms for the verification of finite transducers. At the next stage of our research on the new extensions of temporal logic designed for the specification and verification of sequential reactive systems, we studied the verification problem for these systems using the temporal logic Reg-CTL*, which is an extension ofthe Generalized Computational Tree Logics CTL*. In this paper we present an algorithm for checking the satisfiability of Reg-CTL* formulae on models of finite state transducers and show that this problem belongs to the complexity class ExpSpace.

реагирующая системаверификация моделей программконечный автомат-преобразовательтемпоральная логикарегулярный языкспецификацияreactive systemmodel checkingfinite state transducertemporal logicregular languagespecificationРФФИ, проект № 18-01-00854RFBR, project 18-01-00854ReferencesR. 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.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.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.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.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.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.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.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.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.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.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.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.E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking. MIT press, 1999.E. M. Clarke Jr, O. Grumberg, D. Kroening, D. Peled, and H. Veith, Model checking. MIT press, 1999.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.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.J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 1979.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.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.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.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.P. Wolper, «Temporal Logic Can Be More Expressive», Information and control, vol. 56, no. 1-2, pp. 72-99, 1983.P. Wolper, «Temporal Logic Can Be More Expressive», Information and control, vol. 56, no. 1-2, pp. 72-99, 1983.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.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.M. Y. Vardi and P. Wolper, «Yet another process logic», in Lecture Notes in Computer Science, Springer, vol. 14, 1983, pp. 501-512.M. Y. Vardi and P. Wolper, «Yet another process logic», in Lecture Notes in Computer Science, Springer, vol. 14, 1983, pp. 501-512.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.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.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.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.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.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.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.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.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.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.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.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.W. J. Savitch, «Relationships between nondeterministic and deterministic tape complexities», Journal of computer and system sciences, vol. 4, no. 2, pp. 177-192, 1970.W. J. Savitch, «Relationships between nondeterministic and deterministic tape complexities», Journal of computer and system sciences, vol. 4, no. 2, pp. 177-192, 1970.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.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.A. Mader, «A classification of PLC models and applications», in Discrete Event Systems, vol. 569, Springer, 2000, pp. 239-246.A. Mader, «A classification of PLC models and applications», in Discrete Event Systems, vol. 569, Springer, 2000, pp. 239-246.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.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.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.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.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.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.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.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.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.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.

The authors declare that there are no conflicts of interest present.