Abstract
In classical LTL model checking, both the system and the specification are over a finite set of atomic propositions. We present a natural extension of this model, in which the atomic propositions are parameterized by variables ranging over some (possibly infinite) domain. For example, by parameterizing the atomic propositions send and receive by a variable x ranging over possible messages, the specification \({\textsf{G} } ({\it send}.x \rightarrow{\textsf{F} }{\it receive}.x)\) specifies that not only each send signal is followed by a receive signal, but also that the content of the received message agrees with the content of the one sent.
Our extended setting consists of Variable LTL (VLTL) – a specification formalism that extends LTL with atomic propositions parameterized by variables, and abstract systems – systems in which atomic propositions may be parameterized by variables. We study the model-checking problem in this setting. We show that while the general setting is undecidable, some useful special cases are decidable. In particular, for fragments of VLTL that restrict the quantification over the variables, the model checking is PSPACE-complete, and thus is not harder than the LTL model checking problem. The latter result conveys the strength and advantage of our setting.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Barcelo, P., Libkin, L., Reutter, J.: Parameterized regular expressions and their languages. In: FSTTCS (2011)
Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about Networks with many identical Finite-State Processes. In: PODC 1986 (1986)
Clarke, E.M., Grumberg, O., Long, D.E.: Model Checking and Abstraction. In: TOPLAS 1994 (1994)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Demri, S., D’Souza, D.: An Automata-Theoretic Approach to Constraint LTL. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol. 2556, pp. 121–132. Springer, Heidelberg (2002)
Dingel, J., Filkorn, T.: Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style Reasoning and Theorem Proving. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 54–69. Springer, Heidelberg (1995)
Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S., Nutzung, D.: Efficient Algorithms for Model Checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000)
German, S., Sistla, A.P.: Reasoning about systems with many processes. JACM (1992)
Grumberg, O., Kupferman, O., Sheinvald, S.: Variable Automata over Infinite Alphabets. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 561–572. Springer, Heidelberg (2010)
Henzinger, T.A.: Hybrid Automata with Finite Bisimulations. In: Fülöp, Z. (ed.) ICALP 1995. LNCS, vol. 944, pp. 324–335. Springer, Heidelberg (1995)
Lazic, R.: Safely freezing LTL. In: FSTSTC (2006)
Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. Proc. 12th POPL (1985)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer (1992)
Neven, F., Schwentick, T., Vianu, V.: Towards Regular Languages over Infinite Alphabets. In: Sgall, J., Pultr, A., Kolman, P. (eds.) MFCS 2001. LNCS, vol. 2136, pp. 560–572. Springer, Heidelberg (2001)
Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. JACM (1985)
Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Theoretical Computer Science (1987)
Vardi, M.Y.: Personal communication (2011)
Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. Journal of Computer and Systems Science (1986)
Chomicki, J., Toman, D.: Temporal Logic in Information Systems. In: Logics for Databases and Information Systems, pp. 31–70 (1998)
Dixon, C., Fisher, M., Konev, B., Lisitsa, A.: Efficient First-Order Temporal Logic for Infinite-State Systems. CoRR (2007)
Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable Fragments of First-Order Temporal Logics. Annals of Pure and Applied Logic (1999)
Alur, R.: Timed Automata. Theoretical Computer Science, pp. 183–235 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grumberg, O., Kupferman, O., Sheinvald, S. (2012). Model Checking Systems and Specifications with Parameterized Atomic Propositions. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-33386-6_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33385-9
Online ISBN: 978-3-642-33386-6
eBook Packages: Computer ScienceComputer Science (R0)