On the Satisfiability and Model Checking for one Parameterized Extension of Linear-time Temporal Logic

Sequential reactive systems are computer programs or hardware devices which process the flows of input data or control signals and output the streams of instructions or responses. When designing such systems one needs formal specification languages capable of expressing the relationships between the input and output flows. Previously, we introduced a family of such specification languages based on temporal logics $LTL$, $CTL$ and $CTL^*$ combined with regular languages. A characteristic feature of these new extensions of conventional temporal logics is that temporal operators and basic predicates are parameterized by regular languages. In our early papers, we estimated the expressive power of the new temporal logic $Reg$-$LTL$ and introduced a model checking algorithm for $Reg$-$LTL$, $Reg$-$CTL$, and $Reg$-$CTL^*$. The main issue which still remains unclear is the complexity of decision problems for these logics. In the paper, we give a complete solution to satisfiability checking and model checking problems for $Reg$-$LTL$ and prove that both problems are Pspace-complete. The computational hardness of the problems under consideration is easily proved by reducing to them the intersection emptyness problem for the families of regular languages. The main result of the paper is an algorithm for reducing the satisfiability of checking $Reg$-$LTL$ formulas to the emptiness problem for Buchi automata of relatively small size and a description of a technique that allows one to check the emptiness of the obtained automata within space polynomial of the size of input formulas.

temporal logics, regular language, transducer, model checking, satisfiability checking, Buchi automata, emptiness problem

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.