×

zbMATH — the first resource for mathematics

Linear temporal logic with until and next, logical consecutions. (English) Zbl 1147.03008
Summary: While specifications and verifications of concurrent systems employ Linear Temporal Logic (\(\mathcal{LTL}\)), it is increasingly likely that logical consequence in \(\mathcal{LTL}\) will be used in the description of computations and parallel reasoning. Our paper considers logical consequence in the standard \(\mathcal{LTL}\) with temporal operations \(\mathbf U\) (until) and \(\mathbf N\) (next). The prime result is an algorithm recognizing consecutions admissible in \(\mathcal{LTL}\), so we prove that \(\mathcal{LTL}\) is decidable w.r.t. admissible inference rules. As a consequence we obtain algorithms verifying the validity of consecutions in \(\mathcal{LTL}\) and solving the satisfiability problem. We start by a simple reduction of logical consecutions (inference rules) of \(\mathcal{LTL}\) to equivalent ones in the reduced normal form (which have uniform structure and consist of formulas of temporal degree 1). Then we apply a semantic technique based on \(\mathcal{LTL}\)-Kripke structures with formula definable subsets. This yields necessary and sufficient conditions for a consecution to be not admissible in \(\mathcal{LTL}\). These conditions lead to an algorithm which recognizes consecutions (rules) admissible in \(\mathcal{LTL}\) by verifying the validity of consecutions in special finite Kripke structures of size square polynomial in reduced normal forms of the consecutions. As a consequence, this also solves the satisfiability problem for \(\mathcal{LTL}\).

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., ()
[2] Bloem, R.; Ravi, K.; Somenzi, F., Efficient decision procedures for model checking of linear time logic properties, () · Zbl 1046.68579
[3] Carsten, Fritz, Constructing Büchi automaton from linear temporal logic using simulation relations for alternating Büchi automata, (), 35-48 · Zbl 1279.68152
[4] Clarke, E.; Grumberg, O.; Hamaguchi, K.P., Another look at LTL model checking, ()
[5] M. Daniele, F. Giunchiglia, M. Vardi, Improved automata generation for linear temporal logic, in: (CAV’99), International Conference on Computer-Aided Verification, Trento, Italy, 1999 · Zbl 1046.68588
[6] Emerson, E.A., Temporal and modal logics, (), 996-1072 · Zbl 0900.03030
[7] Friedman, H., One hundred and two problems in mathematical logic, Journal of symbolic logic, 40, 3, 113-130, (1975) · Zbl 0318.02002
[8] Gabbay, D., The declarative past and imperative future: executable temporal logic for interactive systems, (), 409-448
[9] Gabbay, D., An irreflexivity lemma with applications to axiomatizations of conditions of linear frames, (), 67-89
[10] Ghilardi, S., Unification in intuitionistic logic, Journal of symbolic logic, 64, 2, 859-880, (1999) · Zbl 0930.03009
[11] Goldblatt, R., Logics of time and computation, () · Zbl 0635.03024
[12] Goranko, V.; Passy, S., Using the universal modality: gains and questions, Journal of logic and computation, 2, 1, 5-30, (1992) · Zbl 0774.03003
[13] Harrop, R., Concerning formulas of the types \(A \rightarrow B \vee C\), \(A \rightarrow \exists x B(x)\) in intuitionistic formal system, Journal of symbolic logic, 25, 27-32, (1960) · Zbl 0098.24201
[14] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, Journal of symbolic logic, 66, 281-294, (2001) · Zbl 0986.03013
[15] Jerábek, E., Admissible rules of modal logics, Journal of logic and computation, 15, 411-431, (2005) · Zbl 1077.03011
[16] Kapron, B.M., Modal sequents and definability, Journal of symbolic logic, 52, 3, 756-765, (1987) · Zbl 0641.03014
[17] Kesten, Y.; Manna, Z.; McGuire, H.; Pnueli, A., A decision algorithm for full propositional temporal logic, (), 97-109
[18] F. Laroussinie, N. Markey, Ph. Schnoebelen, 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
[19] Lange, M., A quick axiomatisation of LTL with past, Mathematical logic quarterly, 51, 1, 83-88, (2005) · Zbl 1058.03023
[20] Lorenzen, P., Einführung in die operative logik und Mathematik, (1955), Springer-Verlag Berlin-Göttingen, Heidelberg · Zbl 0066.24802
[21] Manna, Z; Pnueli, A., Temporal verification of reactive systems: safety, (1995), Springer-Verlag
[22] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems: specification, (1992), Springer-Verlag
[23] Mints, G.E., Derivability of admissible rules, Journal of soviet mathematics, 6, 4, 417-421, (1976) · Zbl 0375.02014
[24] Pnueli, A., The temporal logic of programs, (), 46-57
[25] Rybakov, V.V., Rules of inference with parameters for intuitionistic logic, Journal of symbolic logic, 57, 3, 912-923, (1992) · Zbl 0788.03007
[26] Rybakov, V.V., Hereditarily structurally complete modal logics, Journal of symbolic logic, 60, 1, 266-288, (1995) · Zbl 0836.03014
[27] Rybakov, V.V., Admissible logical inference rules, () · Zbl 0729.03012
[28] Rybakov, V.V.; Kiyatkin, V.R.; Oner, T., On finite model property for admissible rules, Mathematical logic quarterly, 45, 4, 505-520, (1999) · Zbl 0938.03033
[29] Rybakov, V.V., Construction of an explicit basis for rules admissible in modal system S4, Mathematical logic quarterly, 47, 4, 441-451, (2001) · Zbl 0992.03027
[30] Rybakov, V.V., Logical consecutions in discrete linear temporal logic, Journal of symbolic logic, 70, 4, 1137-1149, (2005) · Zbl 1110.03010
[31] Rybakov, V.V., Logical consecutions in intransitive temporal linear logic of finite intervals, Journal of logic computation, 15, 5, 633-657, (2005) · Zbl 1091.03002
[32] Rybakov, V.V., (), 322-334
[33] Rybakov, V., Until-Since temporal logic based on parallel time with common past. deciding algorithms, (), 487-497 · Zbl 1132.03324
[34] Sistla, A.P.; Clarke, E.M., The complexity of propositional linear temporal logic, Journal of the ACM, 32, 3, 733-749, (1985) · Zbl 0632.68034
[35] M. Vardi, An automata-theoretic approach to linear temporal logic, in: Proceedings of the Banff Workshop on Knowledge Acquisition, Banff’94, 1994
[36] M. Vardi, Reasoning about the past with two-way automata, in: Proc. 25th Int. Coll. on Automata, Languages, and Programming, LNCS, vol. 1443, 1998, pp. 628-641 · Zbl 0909.03019
[37] J. van Benthem, Time, logic and computation, REX Workshop, 1988, pp. 1-49
[38] van Benthem, J.; Bergstra, J.A., Logic of transition systems, Journal of logic, language and information, 3, 4, 247-283, (1994) · Zbl 0827.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.