Geodesic
On the satisfiability and model checking for one parameterized extension of linear-time temporal logic
Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 356-371.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: temporal logics, regular language, transducer, model checking, satisfiability checking, Buchi automata, emptiness problem. 
@article{MAIS_2021_28_4_a3,
     author = {A. R. Gnatenko and V. A. Zakharov},
     title = {On the satisfiability and model checking for one parameterized extension of linear-time temporal logic},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {356--371},
     publisher = {mathdoc},
     volume = {28},
     number = {4},
     year = {2021},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a3/}
}
TY  - JOUR
AU  - A. R. Gnatenko
AU  - V. A. Zakharov
TI  - On the satisfiability and model checking for one parameterized extension of linear-time temporal logic
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2021
SP  - 356
EP  - 371
VL  - 28
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a3/
LA  - ru
ID  - MAIS_2021_28_4_a3
ER  - 
%0 Journal Article
%A A. R. Gnatenko
%A V. A. Zakharov
%T On the satisfiability and model checking for one parameterized extension of linear-time temporal logic
%J Modelirovanie i analiz informacionnyh sistem
%D 2021
%P 356-371
%V 28
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a3/
%G ru
%F MAIS_2021_28_4_a3
A. R. Gnatenko; V. A. Zakharov. On the satisfiability and model checking for one parameterized extension of linear-time temporal logic. Modelirovanie i analiz informacionnyh sistem, Tome 28 (2021) no. 4, pp. 356-371. http://geodesic.mathdoc.fr/item/MAIS_2021_28_4_a3/

[1] A. Pnueli, “The temporal logic of programs”, Proceedings of the 18th Annual Symposium on Foundations of Computer Science, 1977, 46–57

[2] D. Gabbay, A. Pnueli, S. Shelach, J. Stavi, “The temporal analysis of fairness”, Proceedings of 7-th ACM Symposium on Principles of Programming Languages, 1980, 163–173

[3] M. Ben-Ari, Z. Manna, A. Pnueli, “The temporal logic of branching time”, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1981, 164–176 | DOI

[4] J. Ouaknine, J. Worrell, “Some recent results in Metric Temporal Logic”, Proceedings of the 6th International Conference Formal Modeling and Analysis of Timed Systems, 2008, 1–13 | Zbl

[5] Z. Manna, A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer, 1992

[6] P. Wolper, “Temporal Logic Can Be More Expressive”, Information and Control, 56 (1983), 72–99 | DOI | MR | Zbl

[7] T. French, “Quantified propositional temporal logic with repeating states”, Proceedings of the 10th International Symposium on Temporal Representation and Reasoning, 2003, 155–165

[8] J. Henriksen, P. S. Thiagarajan, “Dynamic linear time temporal logic”, Annals of Pure and Applied Logic, 96 (1999), 187–207 | DOI | MR | Zbl

[9] G. De Giacomo, M. Y. Vardi, “Linear temporal logic and linear dynamic logic on finite traces”, Proceedings of the 23th International Joint Conference on Artificial Intelligence, 2013, 854–860

[10] A. Artale, R. Konchakov, V. Ryzhikov, M. Zakharyaschev, “Tractable interval temporal propositional and description logics”, Proceedings of the 29th AAAI Conference on Artificial Intelligence, 2015, 1417–1423

[11] S. Merz, M. Wirsing, J. Zappe, “A Spatio-Temporal Logic for the Specification and Refinement of Mobile Systems”, Proceedings of the 6th International Conference on Fundamental Approaches to Software Engineering, 2003, 87–101 | DOI | Zbl

[12] C. Baier, J. Katoen, Principles of Model Checking, MIT Press, 2008 | Zbl

[13] E. M. Clarke, O. Gramberg, D. A. Peled, Model Checking, MIT Press, 1999

[14] D. G. Kozlova, V. A. Zakharov, “On the model checking of sequential reactive systems”, Proceedings of the 25th International Workshop on Concurrency, Specification and Programming, CS 2016, CEUR Workshop Proceedings, 1698, 2016, 376–389

[15] A. R. Gnatenko, V. A. Zakharov, “On the verification ofnite transducers over semigroups”, Proceedings of ISP RAS, 30 (2018), 303–324 | DOI

[16] A. Gnatenko, V. Zakharov, “On the Model Checking Problem for Some Extension of CTL*”, Modeling and Analysis of Information Systems, 27 (2020), 428–441 | DOI | MR

[17] A. Gnatenko, V. Zakharov, “On the Expressive Power of Some Extensions of Linear Temporal Logic”, Modeling and Analysis of Information Systems, 25 (2018), 506–524 | DOI

[18] M. Vardi, P. Wolper, “An Automata-Theoretic Approach to Automatic Program Verification”, Proceedings of the First Symposium on Logic in Computer Science, 1986, 322–331

[19] J. A. W. Kamp, Tense Logic and theeory of Linear Order, PhD thesis, University of California, Los Angeles, 1968

[20] K. Etessami, T. Wilke, “An Until Hierarchy and Other Applications of an Ehrenfeucht-Fraisse Game for Temporal Logic”, Information and Computation, 160 (2000), 88–108 | DOI | MR | Zbl

[21] M. Leucker, C. Sanchez, “Regular Linear Temporal Logic”, Proceedings of the 4-th International Colloquium on Theoretical Aspects of Computing, 2007, 291–305 | Zbl

[22] O. Kupferman, N. Piterman, M. Y. Vardi, “Extended Temporal Logic Revisited”, Proceedings of 12-th International Conference on Concurrency Theory, 2001, 519–535 | MR | Zbl

[23] A. R. Gnatenko, V. A. Zakharov, “O slozhnosti verifikatsii avtomatov-preobrazovateley nad kommutativnymi polugruppami”, Trudy 18 Mezhdunarodnoj konferentsii Problemy teoreticheskoy kibernetiki, 2017, 68–70

[24] V. Zakharov, G. Temerbekova, “On the Minimization of Finite State Transducers over Semigroups”, Modeling and Analysis of Information Systems, 23 (2016), 741–753 | DOI

[25] V. Zakharov, “Equivalence checking problem for finite state transducers over semigroups”, Proceedings of the 6-th International Conference on Algebraic Informatics, 2015, 208–221 | DOI | Zbl

[26] J. M. Fisher, R. E. Ladner, “Propositional Dynamic Logic of Regular Programs”, Journal of Computer and System Sciences, 18 (1979), 194–211 | DOI | MR

[27] W. J. Savitch, “Relationships between nondeterministic and deterministic tape complexities”, Journal of Computer and System Science, 4 (1970), 177–192 | DOI | Zbl

[28] D. Kozen, “Lower bounds for natural proof systems”, Proceedings of the 18th International Symposium on the Foundations of Computer Science, 1977, 254–266