On the expressive power of some extensions of linear temporal logic

A. R. Gnatenko ; V. A. Zakharov

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 506-524.

Résumé

One of the most simple models of computation which is suitable for representation of reactive systems behaviour is a finite state transducer which operates over an input alphabet of control signals and an output alphabet of basic actions. The behaviour of such a reactive system displays itself in the correspondence between flows of control signals and compositions of basic actions performed by the system. We believe that the behaviour of this kind requires more suitable and expressive means for formal specifications than the conventional $LTL$. In this paper, we define some new (as far as we know) extension $\mathcal{LP}$-$LTL$ of Linear Temporal Logic specifically intended for describing the properties of transducers computations. In this extension the temporal operators are parameterized by sets of words (languages) which represent distinguished flows of control signals that impact on a reactive system. Basic predicates in our variant of the temporal logic are also languages in the alphabet of basic actions of a transducer; they represent the expected response of the transducer to the specified environmental influences. In our earlier papers, we considered a model checking problem for $\mathcal{LP}$-$LTL$ and $\mathcal{LP}$-$CTL$ and showed that this problem has effective solutions. The aim of this paper is to estimate the expressive power of $\mathcal{LP}$-$LTL$ by comparing it with some well known logics widely used in the computer science for specification of reactive systems behaviour. We discovered that a restricted variant $\mathcal{LP}$-$1$-$LTL$ of our logic is more expressive than LTL and another restricted variant $\mathcal{LP}$-$n$-$LTL$ has the same expressive power as monadic second order logic S$1$S.

Détail

Keywords: temporal logics, expressive power, specification, verification, Buchi automata, infinite words.

Bibliographie

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

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

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

[4] Fisher J. M., Ladner R. E., “Propositional dynamic logic of regular programs”, Journal of Computer and System Sciences, 18 (1979), 194–211 | DOI | MR

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

[6] Gnatenko A. R., Zakharov V. A., “O slozhnosti verifikatsii avtomatov-preobrazovateley nad kommutativnymi polugruppami”, Trudy 18 Mezhdunarodnoj konferentsii “Problemy teoteticheskoy kibernetiki”, 2017, 68–70 (in Russian)

[7] Gnatenko A. R., Zakharov V. A., “On the model checking of finite state transducers over semigroups”, Proceedings of ISP RAS, 30:3, 303–324

[8] Harel D., Kozen D., Parikh P., “Process logic: Expressiveness, decidability, completeness”, Journal of Computer and System Science, 25:2 (1982), 144–170 | DOI | MR | Zbl

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

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

[11] Kozlova D. G., Zakharov V. A., “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, 233–244

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

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

[14] Manna Z., Wolper P., “Synthesis of Communicating Processes from Temporal Logic Specifications”, Lecture Notes in Computer Science, 131, 1981, 253–281 | DOI | MR

[15] Thomas W., “Automata on infinite objects”, Handbook of Theoretical Computer Science, v. B, Formal Models and Semantics, 1990, 133–192 | MR

[16] Vardi M. Y., Wolper P., “Yet Another Process Logic”, Lecture Notes in Computer Science, 14, 1983, 501–512 | MR

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

[18] Vardi M. Y., “A Temporal Fixpoint Calculus”, Proceedings of the 15-th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1989, 250–259

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

[20] Wolper P., Boigelot B., “Verifying systems with infinite but regular state spaces”, Lecture Notes in Computer Science, 1427, 1998, 88–97 | DOI | MR

[21] Zakharov V. A., “Equivalence checking problem for finite state transducers over semigroups”, Lecture Notes in Computer Science, 9270, 2015, 208–221 | DOI | MR | Zbl

[22] Zakharov V. A., Temerbekova G. G., “On the minimization of finite state trans-ducers over semigroups”, Automatic Control and Computer Sciences, 51:7 (2017), 523–530 | DOI | MR

[23] Zakharov V. A., Jaylauova S. R., “On the minimization problem for sequential programs”, Automatic Control and Computer Sciences, 51:7 (2017), 689–700 | DOI | MR