Decidability w.r.t. Logical Consecutions of Linear Temporal Logic Extended by Since and Previous

• Autorzy: Rybakov V.V.
• Języki publikacji: EN

Abstrakty

EN

This paper aims to prove that the linear temporal logic LTLu,sn, n-1(N) , which is an extension of the standard linear temporal logic LTL by operations Since and Previous (LTL itself, as standard, uses only Until and Next) and is based on the frame of all natural numbers N, as generating Kripke/Hintikka structure, is decidable w.r.t. admissible consecutions (inference rules). We find an algorithm recognizing consecutions admissible in LTLu,sn, n-1(N) . As a consequence this algorithm solves satisfiability problem and shows that LTLu,sn, n-1(N) itself is decidable, despite LTLu,sn, n-1(N) does not have the finite model property.

Słowa kluczowe

EN

decidability; algorithms; inference rule; temporal logic; linear temporal logic; admissible inference rules

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 81, nr 1-3
• Strony: 297--313
• Opis fizyczny: bibliogr. 43 poz.

Twórcy

autor

Rybakov V.V.

• Department of Computing and Mathematics, Manchester Metropolitan University, John Dalton Building, Chester Street, Manchester M1 5GD, U.K,

Bibliografia

• [1] Barringer H, Fisher M, Gabbay D., Gough G. Advances in Temporal Logic, Vol. 16 of Applied logic series, Kluwer Academic Publishers, Dordrecht, 1999.
• [2] Bloem R., Ravi K, Somenzi F. Efficient Decision Procedures forModel Checking of Linear Time Logic Properties.- In: Conference on Computer Aided Verification (CAV), LNCS 1633, Trento, Italy, 1999, Springer-Verlag.
• [3] Carsten Fritz. Constructing Büchi Automaton fromLinear Temporal Logic Using SimulationRelations for Alternating Büchi Automata . - Lecture Notes in Computer Science (LNCS), 2759, 2003 , pp. 35 - 48.
• [4] Daniele M, Giunchiglia F, Vardi M. Improved Automata Generation for Linear Temporal Logic. - In book: (CAV'99), International Conference on Computer-Aided Verification, Trento, Italy, 1999.
• [5] Emerson E.A. Temporal and Modal Logics.- in: Handbook of Theoretical Computer Science. J. van Leenwen, Ed., Elsevier Science Publishers, the Netherlands, 1990, pp. 996 - 1072.
• [6] Friedman H. One Hundred and Two Problems in Mathematical Logic.- Journal of Symbolic Logic, Vol. 40, 1975, No. 3, pp. 113 - 130.
• [7] Gabbay D. The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proceedings of the 1st Conference on Temporal Logic in Specification, volume 398 of LNCS , 1987, pp. 409 - 448.
• [8] Gabbay D. An Irreflexivity Lemma with Applications to Axiomatizations of Conditions of Linear Frames.- Aspects of Phil. Logic (Ed. V.Monnich), Reidel, Dordrecht, 1981, pp. 67 - 89.
• [9] Gabbay D.M., Hodkinson I.M. and Reynolds M.A. Temporal Logic, - Mathematical Foundations and Computational Aspects, volume 1. Clarendon Press, Oxford, 1994.
• [10] Gabbay D.M., Hodkinson I.M. An axiomatisation of the temporal logic with Until and Since over the real numbers. - Journal of Logic and Computation, Vol. 1 (1990), pp. 229-260.
• [11] Ghilardi S. Unification in Intuitionistic logic. - Journal of Symbolic Logic, Vol. 64, No. 2 (1999) , pp. 859-880.
• [12] Goldblatt R. Logics of Time and Computation.- CSLI Lecture Notes, No.7, 1992.
• [13] Goldblatt R. Mathematical Modal Logic: A View of its Evolution. - J. Applied Logic, Vol 1 (5-6), 2003, pp. 309 - 392.
• [14] Goranko V., Passy S. Using the Universal Modality: Gains and Questions.- J. Log. Comput., Vol 2(1), 1992, pp. 5-30.
• [15] Harrop R. Concerning Formulas of the Types A ! B _ C, A ! 9xB(x) in Intuitionistic Formal System.- J. of Symbolic Logic, Vol. 25, 1960, pp. 27-32.
• [16] Iemhoff R. On the admissible rules of Intuitionistic Propositional Logic. - J.of Symbolic Logic Vol. 66, 2001, pp. 281-294.
• [17] Jerábek E. Admissible Rules of Modal Logics. -J. of Logic and Computation, 2005, Vol. 15. pp. 411-431.
• [18] Kapron B.M. Modal Sequents and Definability, J.of Symbolic Logic, Vol. 52(3), 1987, pp. 756 - 765.
• [19] Lange M. A quick axiomatisation of LTL with past. Mathematical Logic Quarterly, V, 51, No 1, 2005, pp. 83 - 88.
• [20] Laroussinie F., Markey N. and Schnoebelen Ph. Temporal Logic with Forgettable Past. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), Copenhagen, Denmark, 2002, pp 383-392.
• [21] Lichtenstein O., Pnueli A. Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL, 8(1), 2000, pp. 55 - 85.
• [22] Lorenzen P. Einf ührung in die operative Logik und Mathematik. - Berlin-Göttingen, Heidelberg, Springer-Verlag, 1955.
• [23] Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. - Springer-Verlag, 1992.
• [24] Manna Z., Sipma H. Alternating the Temporal Picture for Safety. - In Proc. 27th Intl. Colloq. Aut. Lang. Prog.(ICALP 2000). LNCS 1853, Springer-Verlag, pp. 429-450.
• [25] Mints G.E. Derivability of Admissible Rules.- J. of Soviet Mathematics, V. 6, 1976, No. 4, pp. 417 - 421.
• [26] Pnueli A. The Temporal Logic of Programs.- In Proc. of the 18th Annual Symp. on Foundations of Computer Science, IEEE, 1977, pp. 46 - 57.
• [27] Rybakov V.V. A Criterion for Admissibility of Rules in the Modal System S4 and the Intuitionistic Logic. - Algebra and Logic, V.23 (1984), No 5, pp. 369 - 384 (Engl. Translation).
• [28] Rybakov V.V. The Bases for Admissible Rules of Logics S4 and Int.- Algebra and Logic, V.24, 1985, pp. 55 - 68 (English translation).
• [29] Rybakov V.V. Rules of Inference with Parameters for Intuitionistic logic.- Journal of Symbolic Logic, Vol. 57, No. 3, 1992, pp. 912 - 923.
• [30] Rybakov V.V. Hereditarily Structurally Complete Modal Logics.- Journal of Symbolic Logic, Vol. 60, No.1, 1995, pp. 266 - 288.
• [31] Rybakov V.V. Modal Logics Preserving Admissible for S4 Inference Rules. - In Proceedings of the conference CSL'94. LNCS, No.993 (1995), Springer-Verlag, pp. 512 - 526.
• [32] Rybakov V.V. Admissible Logical Inference Rules. - Studies in Logic and the Found. ofMathematics, Vol. 136, Elsevier Sci. Publ., North-Holland, New-York- Amsterdam, 1997.
• [33] Rybakov V.V. Quasi-characteristic Inference Rules. - In Book: Eds: S.Adian, A.Nerode, LNCS, Vol. 1234, Springer, 1997, pp. 333 - 342.
• [34] Rybakov V.V., Kiyatkin V.R., Oner T., On Finite Model Property For Admissible Rules. - Mathematical Logic Quarterly, Vol.45, No 4, 1999, pp. 505 -520.
• [35] Rybakov V.V. Terziler M., Rimazki V. Basis in Semi-Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC. - Mathematical Logic Quarterly, Vol.46, No. 2 (2000), pp. 207 - 218.
• [36] Rybakov V.V. Construction of an Explicit Basis for Rules Admissible in Modal System S4. - Mathematical Logic Quarterly, Vol. 47, No. 4 (2001), pp. 441 - 451.
• [37] Rybakov V.V. Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals. - Journal of Logic Computation, (Oxford Press, London), Vol. 15 No. 5 (2005), pp. 633 - 657.
• [38] Rybakov V.V. Logical Consecutions in Discrete Linear Temporal Logic. Journal of Symbolic Logic, V.70, No 4 (2005), pp. 1137 - 1149.
• [39] Sistla A.P. and Clarke E.M. The Complexity of Propositional Linear Temporal Logic. Journal of the ACM, 32(3), 1985, pp. 733 - 749.
• [40] Thomason S.K. Semantic Analysis of Tense Logic.- Journal of Symbolic Logic, Vol. 37, No. 1 (1972).
• [41] van Benthem J. The Logic of Time. - Reidel, Dordrecht, Synthese Library, Vol. 156, 1983.
• [42] Vardi M. An automata-theoretic approach to linear temporal logic.- In Proceedings of the Banff Workshop on Knowledge Acquisition (1994), (Banff '94).
• [43] Vardi M. Reasoning about the past with two-way automata. In: Proc. 25th Int. Coll. on Automata, Languages, and Programming, Vol. 1443 of LNCS, 1998, pp. 628-641.