Abstract
As specifications and verifications of concurrent systems employ Linear Temporal Logic (LTL), it is increasingly likely that logical consequence in LTL will be used in description of computations and parallel reasoning. We consider the linear temporal logic \(\mathcal{LTL^{U,B}_{N,N^{-1}} (Z)}\) extending the standard LTL by operations B (before) and N − 1 (previous). Two sorts of problems are studied: (i) satisfiability and (ii) description of logical consequence in \(\mathcal{LTL^{U,B}_{N,N^{-1}} (Z)}\) via admissible logical consecutions (inference rules). The model checking for LTL is a traditional way of studying such logics. Most popular technique based on automata was developed by M.Vardi (cf. [39, 6]). Our paper uses a reduction of logical consecutions and formulas of LTL to consecutions of a uniform form consisting of formulas of temporal degree 1. Based on technique of Kripke structures, we find necessary and sufficient conditions for a consecution to be not admissible in \(\mathcal{LTL^{U,B}_{N,N^{-1}} (Z)}\). This provides an algorithm recognizing consecutions (rules) admissible in \(\mathcal{LTL^{U,B}_{N,N^{-1}} (Z)}\) by Kripke structures of size linear in the reduced normal forms of the initial consecutions. As an application, this algorithm solves also the satisfiability problem for \(\mathcal{LTL^{U,B}_{N,N^{-1}} (Z)}\).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barringer, H., Fisher, M., Gabbay, D., Gough, G.: Advances in Temporal Logic. Applied logic series, vol. 16. Kluwer Academic Publishers, Dordrecht (1999)
Bloem, R., Ravi, K., Somenzi, F.: Efficient Decision Procedures for Model Checking of Linear Time Logic Properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 222–235. Springer, Heidelberg (1999)
Bruns, G., Godefroid, P.: Temporal Logic Query-Checking. In: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), Boston, MA, USA, June 2001, pp. 409–417. IEEE Computer Society, Los Alamitos (2001)
Clarke, E., Grumberg, O., Hamaguchi, K.P.: Another look at LTL Model Checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, Springer, Heidelberg (1994)
David, C., Paliath, N.: Ground Temporal Logic: A Logic for Hardware Verification. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 247–259. Springer, Heidelberg (1994)
Daniele, M., Giunchiglia, F., Vardi, M.: Improved Automata Gneration for Linear Temporal Logic. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 249–260. Springer, Heidelberg (1999)
Emerson, E.A.: Temporal and Modal Logics. In: van Leenwen, J. (ed.) Handbook of Theoretical Computer Science, pp. 996–1072. Elsevier Science Publishers, The Netherlands (1990)
Friedman, H.: One Hundred and Two Problems in Mathematical Logic. Journal of Symbolic Logic 40(3), 113–130 (1975)
Gabbay, D.: An Irreflevivity Lemma with Applications to Axiomatizations of Conditions of Linear Frames. In: Monnich, V. (ed.) Aspects of Phil. Logic, pp. 67–89. Reidel, Dordrecht (1981)
Ghilardi, S.: Unification in Intuitionistic logic. Journal of Symbolic Logic 64(2), 859–880 (1999)
Goldblatt, R.: Logics of Time and Computation. CSLI Lecture Notes, vol. (7) (1992)
Goranko, V., Passy, S.: Using the Universal Modality: Gains and Questions. J. Log. Comput. 2(1), 5–30 (1992)
van der Hoek, W., Wooldridge, M.: Model Checking Knowledge and Time. In: SPIN 2002, Proc. of the Ninth International SPIN Workshop on Model Checking of Software, Grenoble, France (2002)
Harrop, R.: Concerning Formulas of the Types A→B ∨ C, A→ ∃ x B(x) in Intuitionistic Formal System. J. of Symbolic Logic 25, 27–32 (1960)
Iemhoff, R.: On the admissible rules of Intuitionistic Propositional Logic. J. of Symbolic Logic 66, 281–294 (2001)
Jerabek, E.: Admissible Rules of Modal Logics. J. of Logic and Computation 15, 411–431 (2005)
Kapron, B.M.: Modal Sequents and Definability. J. of Symbolic Logic 52(3), 756–765 (1987)
Lichtenstein, O., Pnueli, A.: Propositional temporal logics: Decidability and completeness. Logic Journal of the IGPL 8(1), 55–85 (2000)
Laroussinie, F., Markey, N., Schnoebelen, P.: Temporal Logic with Forgettable Past. In: IEEE Symp. Logic in Computer Science (LICS 2002)
Lorenzen, P.: Einführung in die operative Logik und Mathematik. Springer, Berlin-Göttingen, Heidelberg (1955)
Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.: Verifying Temporal Properties of Reactive Systems: A Step Tutorial. Formal Methods in System Design 16, 227–270 (2000)
Manna, Z., Sipma, H.: Alternating the Temporal Picture for Safety. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 429–450. Springer, Heidelberg (2000)
Mints, G.E.: Derivability of Admissible Rules. J. of Soviet Mathematics 6(4), 417–421 (1976)
Pnueli, A.: The Temporal Logic of Programs. In: Proc. of the 18th Annual Symp. on Foundations of Computer Science, pp. 46–57. IEEE, Los Alamitos (1977)
Pnueli, A., Kesten, Y.: A deductive proof system for CTL *. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 24–40. Springer, Heidelberg (2002)
Rybakov, V.V.: A Criterion for Admissibility of Rules in the Modal System S4 and the Intuitionistic Logic. Algebra and Logic 23(5), 369–384 (1984) (Engl. Translation)
Rybakov, V.V.: The Bases for Admissible Rules of Logics S4 and Int. Algebra and Logic 24, 55–68 (1985) (English translation)
Rybakov, V.V.: Rules of Inference with Parameters for Intuitionistic logic. Journal of Symbolic Logic 57(3), 912–923 (1992)
Rybakov, V.V.: Hereditarily Structurally Complete Modal Logics. Journal of Symbolic Logic 60(1), 266–288 (1995)
Rybakov, V.V.: Modal Logics Preserving Admissible for S4 Inference Rules. In: Proceedings of the conference CSL 1994. LNCS, vol. (993), pp. 512–526. Springer, Heidelberg (1995)
Rybakov, V.V.: Admissible Logical Inference Rules. In: Studies in Logic and the Found. of Mathematics, vol. 136, p. 617. Elsevier Sci. Publ, North-Holland (1997)
Rybakov, V.V.: Quasi-characteristic Inference Rules. In: Adian, S., Nerode, A. (eds.) LFCS 1997. LNCS, vol. 1234, pp. 333–342. Springer, Heidelberg (1997)
Rybakov, V.V., Kiyatkin, V.R., Oner, T.: On Finite Model Property For Admissible Rules. Mathematical Logic Quarterly 45(4), 505–520 (1999)
Rybakov, V.V., Terziler, M., Rimazki, V.: Basis in Semi-Reduced Form for the Admissible Rules of the Intuitionistic Logic IPC. Mathematical Logic Quarterly 46(2), 207–218 (2000)
Rybakov, V.V.: Construction of an Explicit Basis for Rules Admissible in Modal System S4. Mathematical Logic Quarterly 47(4), 441–451 (2001)
Rybakov, V.V.: Logical Consecutions in Intransitive Temporal Linear Logic of Finite Intervals. Journal of Logic Computation 15(5), 633–657 (2005)
Vardi, M.: An automata-theoretic approach to linear temporal logic. In: The Book: Proceedings of the Banff Workshop on Knowledge Acquisition (Banff 1994) (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rybakov, V. (2006). Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms. In: Grigoriev, D., Harrison, J., Hirsch, E.A. (eds) Computer Science – Theory and Applications. CSR 2006. Lecture Notes in Computer Science, vol 3967. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11753728_33
Download citation
DOI: https://doi.org/10.1007/11753728_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34166-6
Online ISBN: 978-3-540-34168-0
eBook Packages: Computer ScienceComputer Science (R0)