×

zbMATH — the first resource for mathematics

Branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha }\) with operations Until and Since based on bundles of integer numbers, logical consecutions, deciding algorithms. (English) Zbl 1148.03011
Summary: This paper is intended as an attempt to describe logical consequence in branching time logics. We study temporal branching time logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\) which use the standard operations Until and Next and dual operations Since and Previous (LTL, as standard, uses only Until and Next). Temporal logics \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\) are generated by semantics based on Kripke/Hintikka structures with linear frames of integer numbers \(\mathcal {Z}\) with a single node (glued zeros). For \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\), the permissible branching of the node is limited by \(\alpha\) (where \(1\leq \alpha \leq \omega)\). We prove that any logic \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\) is decidable w.r.t. admissible consecutions (inference rules), i.e. we find an algorithm recognizing consecutions admissible in \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\). As a consequence, it implies that \(\mathcal {BTL}^{\text{U,S}}_{\text{N},\text{N}^{-1}}(\mathcal {Z})_{\alpha}\) itself is decidable and solves the satisfiability problem.

MSC:
03B44 Temporal logic
03B25 Decidability of theories and sets of sentences
03B70 Logic in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barringer, H., Fisher, M., Gabbay, D., Gough, G.: Advances in Temporal Logic. Applied Logic Series, vol. 16. Kluwer Academic, Dordrecht (1999) · Zbl 0931.00025
[2] Bloem, R., Ravi, K., Somenzi, F.: Efficient decision procedures for model checking of linear time logic properties. In: Conference on Computer Aided Verification (CAV), Trento, Italy. Lecture Notes in Computer Science, vol. 1633. Springer, Berlin (1999) · Zbl 1046.68579
[3] Carsten, F.: Constructing Büchi automaton from linear temporal logic using simulation relations for alternating Büchi automata. In: Lecture Notes in Computer Science, vol. 2759, pp. 35–48. Springer, Berlin (2003) · Zbl 1279.68152
[4] Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: (CAV’99), International Conference on Computer-Aided Verification, Trento, Italy (1999) · Zbl 1046.68588
[5] Emerson, E.A.: Temporal and modal logics. In: van Leenwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier Science, Amsterdam (1990) · Zbl 0900.03030
[6] Friedman, H.: One hundred and two problems in mathematical logic. J. Symb. Log. 40(3), 113–130 (1975) · Zbl 0318.02002 · doi:10.2307/2271891
[7] Gabbay, D.: An irreflexivity lemma with applications to axiomatizations of conditions of linear frames. In: Monnich, V. (ed.) Aspects of Phil. Logic, pp. 67–89. Reidel, Dordrecht (1981) · Zbl 0519.03008
[8] Gabbay, D.: The declarative past and imperative future: executable temporal logic for interactive systems. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Proceedings of the 1st Conference on Temporal Logic in Specification. Lecture Notes in Computer Science, vol. 398, pp. 409–448. Springer, Berlin (1987)
[9] Gabbay, D.M., Hodkinson, I.M.: An axiomatisation of the temporal logic with Until and Since over the real numbers. J. Log. Comput. 1, 229–260 (1990) · Zbl 0744.03018 · doi:10.1093/logcom/1.2.229
[10] Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal Logic: Mathematical Foundations and Computational Aspects, vol. 1. Clarendon, Oxford (1994) · Zbl 0921.03023
[11] Ghilardi, S.: Unification in intuitionistic logic. J. Symb. Log. 64(2), 859–880 (1999) · Zbl 0930.03009 · doi:10.2307/2586506
[12] Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes, vol. 7. Stanford University Press, Stanford (1992) · Zbl 0635.03024
[13] Goldblatt, R.: Mathematical modal logic: a view of its evolution. J. Appl. Log. 1(5/6), 309–392 (2003) · Zbl 1041.03015 · doi:10.1016/S1570-8683(03)00008-9
[14] Goranko, V., Passy, S.: Using the universal modality: gains and questions. J. Log. Comput. 2(1), 5–30 (1992) · Zbl 0774.03003 · doi:10.1093/logcom/2.1.5
[15] Harrop, R.: Concerning formulas of the types A C, A xB(x) in intuitionistic formal system. J. Symb. Log. 25, 27–32 (1960) · Zbl 0098.24201 · doi:10.2307/2964334
[16] Iemhoff, R.: On the admissible rules of intuitionistic propositional logic. J. Symb. Log. 66, 281–294 (2001) · Zbl 0986.03013 · doi:10.2307/2694922
[17] Jerábek, E.: Admissible rules of modal logics. J. Log. Comput. 15, 411–431 (2005) · Zbl 1077.03011 · doi:10.1093/logcom/exi029
[18] Kapron, B.M.: Modal sequents and definability. J. Symb. Log. 52(3), 756–765 (1987) · Zbl 0641.03014 · doi:10.2307/2274361
[19] Lange, M.: A quick axiomatisation of LTL with past. Math. Log. Q. 51(1), 83–88 (2005) · Zbl 1058.03023 · doi:10.1002/malq.200410009
[20] Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal logic with forgettable past. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS’02), Copenhagen, Denmark, pp. 383–392 (2002)
[21] Lichtenstein, O., Pnueli, A.: Propositional temporal logics: decidability and completeness. Log. J. IGPL 8(1), 55–85 (2000) · Zbl 1033.03009 · doi:10.1093/jigpal/8.1.55
[22] Lorenzen, P.: Einführung in die Operative Logik und Mathematik. Springer, Berlin (1955) · Zbl 0068.00801
[23] Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin (1992) · Zbl 0753.68003
[24] Manna, Z., Sipma, H.: Alternating the temporal picture for safety. In: Proceedings of the 27th Int. Colloq. Aut. Lang. Prog. (ICALP 2000). Lecture Notes in Computer Science, vol. 1853, pp. 429–450. Springer, Berlin (2000) · Zbl 0973.68141
[25] Mints, G.E.: Derivability of admissible rules. J. Soviet Math. 6(4), 417–421 (1976) · Zbl 0375.02014 · doi:10.1007/BF01084082
[26] Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46–57. IEEE, New York (1977)
[27] Rybakov, V.V.: A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic. Alg. Log. 23(5), 369–384 (1984) (Engl. translation) · Zbl 0598.03013 · doi:10.1007/BF01982031
[28] Rybakov, V.V.: The bases for admissible rules of logics S4 and int. Alg. Log. 24, 55–68 (1985) (English translation) · Zbl 0598.03014 · doi:10.1007/BF01978706
[29] Rybakov, V.V.: Rules of inference with parameters for intuitionistic logic. J. Symb. Log. 57(3), 912–923 (1992) · Zbl 0788.03007 · doi:10.2307/2275439
[30] Rybakov, V.V.: Hereditarily structurally complete modal logics. J. Symb. Log. 60(1), 266–288 (1995) · Zbl 0836.03014 · doi:10.2307/2275521
[31] Rybakov, V.V.: Modal logics preserving admissible for S4 inference rules. In: Proceedings of the Conference CSL’94. Lecture Notes in Computer Science, vol. 993, pp. 512–526. Springer, Berlin (1995) · Zbl 1044.03515
[32] Rybakov, V.V.: Admissible Logical Inference Rules. Studies in Logic and the Foundations of Mathematics, vol. 136. Elsevier Science/North-Holland, New York/Amsterdam (1997) · Zbl 0872.03002
[33] Rybakov, V.V.: Quasi-characteristic inference rules. In: Adian, S., Nerode, A. (eds.) Lecture Notes in Computer Science, vol. 1234, pp. 333–342. Springer, Berlin (1997) · Zbl 0887.03014
[34] Rybakov, V.V., Kiyatkin, V.R., Oner, T.: On finite model property for admissible rules. Math. Log. Q. 45(4), 505–520 (1999) · Zbl 0938.03033 · doi:10.1002/malq.19990450409
[35] Rybakov, V.V., Terziler, M., Rimazki, V.: Basis in semi-reduced form for the admissible rules of the intuitionistic logic IPC. Math. Log. Q. 46(2), 207–218 (2000) · Zbl 0955.03037 · doi:10.1002/(SICI)1521-3870(200005)46:2<207::AID-MALQ207>3.0.CO;2-E
[36] Rybakov, V.V.: Construction of an explicit basis for rules admissible in modal system S4. Math. Log. Q. 47(4), 441–451 (2001) · Zbl 0992.03027 · doi:10.1002/1521-3870(200111)47:4<441::AID-MALQ441>3.0.CO;2-J
[37] Rybakov, V.V.: Logical consecutions in intransitive temporal linear logic of finite intervals. J. Log. Comput. 15(5), 633–657 (2005) · Zbl 1091.03002 · doi:10.1093/logcom/exi025
[38] Rybakov, V.V.: Logical consecutions in discrete linear temporal logic. J. Symb. Log. 70(4), 1137–1149 (2005) · Zbl 1110.03010 · doi:10.2178/jsl/1129642119
[39] Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. J. ACM 32(3), 733–749 (1985) · Zbl 0632.68034 · doi:10.1145/3828.3837
[40] Thomason, S.K.: Semantic analysis of tense logic. J. Symb. Log. 37(1), 00–00 (1972)
[41] van Benthem, J.: The Logic of Time. Synthese Library, vol. 156. Reidel, Dordrecht (1983) · Zbl 0508.03008
[42] Vardi, M.: An automata-theoretic approach to linear temporal logic. In: Proceedings of the Banff Workshop on Knowledge Acquisition (Banff’94) (1994)
[43] Vardi, M.: Reasoning about the past with two-way automata. In: Proceedings of the 25th International Colloquium on Automata, Languages, and Programming. Lecture Notes in Computer Science, vol. 1443, pp. 628–641. Springer, Berlin (1998) · Zbl 0909.03019
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.