On the Model Checking Problem for Some Extension of CTL*

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.

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.