Abstract
We introduce generalized register automata (GRAs) and study their properties and applications in reasoning about systems and specifications over infinite domains. We show that GRAs can capture both VLTL – a logic that extends LTL with variables over infinite domains, and abstract systems – finite state systems whose atomic propositions are parameterized by variable over infinite domains. VLTL and abstract systems naturally model and specify infinite-state systems in which the source of infinity is the data domain (c.f., range of processes id, context of messages). Thus, GRAs suggest an automata-theoretic approach for reasoning about such systems. We demonstrate the usefulness of the approach by pushing forward the known border of decidability for the model-checking problem in this setting. From a theoretical point of view, GRAs extend register automata and are related to other formalisms for defining languages over infinite alphabets.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Bojanczyk, M., Lasota, S.: An extension of data automata that captures xpath. Logical Methods in Computer Science 8(1) (2012)
Bojanczyk, M., Muscholl, A., Schwentick, T., Segoufin, L., David, C.: Two-variable logic on words with data. In: LICS, pp. 7–16. IEEE Computer Society (2006)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Demri, S., Lazic, R.: LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log. 10(3) (2009)
Figueira, D.: Alternating register automata on finite words and trees. LMCS 8(1) (2012)
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)
Grumberg, O., Kupferman, O., Sheinvald, S.: Model checking systems and specifications with parameterized atomic propositions. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 122–136. Springer, Heidelberg (2012)
Kaminski, M., Francez, N.: Finite-memory automata. TCS 134(2), 329–363 (1994)
Kaminski, M., Zeitlin, D.: Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci. 21(5), 741–760 (2010)
Kara, A., Schwentick, T., Tan, T.: Feasible automata for two-variable logic with successor on data words. In: Dediu, A.-H., Martín-Vide, C. (eds.) LATA 2012. LNCS, vol. 7183, pp. 351–362. Springer, Heidelberg (2012)
Manuel, A., Ramanujam, R.: Class counting automata on datawords. Int. J. Found. Comput. Sci. 22(4), 863–882 (2011)
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)
Segoufin, L.: Automata and logics for words and trees over an infinite alphabet. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 41–57. Springer, Heidelberg (2006)
Tan, T.: Pebble Automata for Data Languages: Separation, Decidability, and Undecidability. PhD thesis, Technion - Computer Science Department (2009)
Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation 115(1), 1–37 (1994)
Wu, Z.: A decidable extension of data automata. In: GandALF, pp. 116–130 (2011)
Wu, Z.: Commutative data automata. In: CSL, pp. 528–542 (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Grumberg, O., Kupferman, O., Sheinvald, S. (2013). An Automata-Theoretic Approach to Reasoning about Parameterized Systems and Specifications. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_28
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_28
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)