Abstract
Temporal logics are a well investigated formalism for the specification and verification of reactive systems. Using formal verification techniques, we can ensure the correctness of a system with respect to its desired behavior (specification), by verifying whether a model of the system satisfies a temporal logic formula modeling the specification.
From a practical point of view, a very challenging issue in using temporal logic in formal verification is to come out with techniques that automatically allow to select small critical parts of the system to be successively verified. Another challenging issue is to extend the expressiveness of classical temporal logics, in order to model more complex specifications.
In this paper, we address both issues by extending the classical branching-time temporal logic Ctl* with minimal model quantifiers (MCtl*). These quantifiers allow to extract, from a model, minimal submodels on which we check the specification (also given by an MCtl* formula).We show that MCtl* is strictly more expressive than Ctl*. Nevertheless, we prove that the model checking problem for MCtl. remains decidable and in particular in PSpace. Moreover, differently from Ctl*, we show that MCtl* does not have the tree model property, is not bisimulation-invariant and is sensible to unwinding. As far as the satisfiability concerns, we prove that MCtl* is highly undecidable. We further investigate the model checking and satisfiability problems for MCtl* sublogics, such as MPml, MCtl, and MCtl+, for which we obtain interesting results. Among the others, we show that MPml retains the finite model property and the decidability of the satisfiability problem.
Work partially supported by MIUR PRIN Project no.2007-9E5KM8.
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
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-Time Temporal Logic. JACM 49(5), 672–713 (2002)
Abadi, M., Lamport, L.: Composing Specifications. TOPLAS 15(1), 73–132 (1993)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2004)
Berger, R.: The Undecidability of the Domino Problem. MAMS 66, 1–72 (1966)
Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The Complexity of Enriched μ-Calculi. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 540–551. Springer, Heidelberg (2006)
Bianco, A., Mogavero, F., Murano, A.: Graded Computation Tree Logic. In: LICS 2009 (to appear, 2009)
Baader, F., Sattler, U.: Expressive Number Restrictions in Description Logics. JLC 9(3), 319–350 (1999)
Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Elseaidy, W.M., Cleaveland, R., Baugh Jr., J.W.: Modeling and Verifying Active Structural Control Systems. SCP 29(1-2), 99–122 (1997)
Emerson, E.A., Halpern, J.Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. JCSS 30(1), 1–24 (1985)
Emerson, E.A.: Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, Formal Models and Sematics (B), vol. B, pp. 995–1072 (1990)
French, T., van Ditmarsch, H.P.: Undecidability for Arbitrary Public Announcement Logic. In: AIML, pp. 23–42 (2008)
Harel, D.: A Simple Highly Undecidable Domino Problem. In: CLC 1984(1984)
Knuth, D.E.: The Art of Computer Programming, Fundamental Algorithms, vol. I. Addison-Wesley, Reading (1968)
Kurshan, R.P.: The Complexity of Verification. In: STOC 1994, pp. 365–371 (1994)
Kupferman, O., Vardi, M.Y.: On the Complexity of Branching Modular Model Checking. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 408–422. Springer, Heidelberg (1995)
Kupferman, O., Vardi, M.Y.: Modular Model Checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381–401. Springer, Heidelberg (1998)
Kupferman, O., Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Branching-Time Model Checking. JACM 47(2), 312–360 (2000)
Lamport, L.: “Sometime” is Sometimes “Not Never”: On the Temporal Logic of Programs. In: POPL 1980, pp. 174–185 (1980)
Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking CTL+ and FCTL is Hard. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 318–331. Springer, Heidelberg (2001)
Löding, C., Rohde, P.: Model Checking and Satisfiability for Sabotage Modal Logic.. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 302–313. Springer, Heidelberg (2003)
Peled, D.: Combining Partial Order Reductions with On-the-Fly Model Checking.. FMSD 8(1), 39–64 (1996)
Pnueli, A.: The Temporal Logic of Programs.. In: FOCS 1977, pp. 46–57 (1977)
Pnueli, A.: The Temporal Semantics of Concurrent Programs. TCS 13, 45–60 (1981)
Queille, J.-P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: CISP 1982, pp. 337–351. Springer, Heidelberg (1982)
Robinson, R.M.: Undecidability and Nonperiodicity for Tilings of the Plane. IM 12, 177–209 (1971)
Wang, H.: Proving Theorems by Pattern Recognition II. BSTJ 40, 1–41 (1961)
Wilke, T.: CTL+ is Exponentially More Succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 110–121. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mogavero, F., Murano, A. (2009). Branching-Time Temporal Logics with Minimal Model Quantifiers. In: Diekert, V., Nowotka, D. (eds) Developments in Language Theory. DLT 2009. Lecture Notes in Computer Science, vol 5583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02737-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-02737-6_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02736-9
Online ISBN: 978-3-642-02737-6
eBook Packages: Computer ScienceComputer Science (R0)