Variable Automata over Infinite Alphabets

  • Orna Grumberg
  • Orna Kupferman
  • Sarai Sheinvald
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6031)


Automated reasoning about systems with infinite domains requires an extension of regular automata to infinite alphabets. Existing formalisms of such automata cope with the infiniteness of the alphabet by adding to the automaton a set of registers or pebbles, or by attributing the alphabet by labels from an auxiliary finite alphabet that is read by an intermediate transducer. These formalisms involve a complicated mechanism on top of the transition function of automata over finite alphabets and are therefore difficult to understand and to work with.

We introduce and study variable finite automata over infinite alphabets (VFA). VFA form a natural and simple extension of regular (and ω-regular) automata, in which the alphabet consists of letters as well as variables that range over the infinite alphabet domain. Thus, VFAs have the same structure as regular automata, only that some of the transitions are labeled by variables. We compare VFA with existing formalisms, and study their closure properties and classical decision problems. We consider the settings of both finite and infinite words. In addition, we identify and study the deterministic fragment of VFA. We show that while this fragment is sufficiently strong to express many interesting properties, it is closed under union, intersection, and complementation, and its nonemptiness and containment problems are decidable. Finally, we describe a determinization process for a determinizable subset of VFA.


Bounded Variable Closure Property Input Word Intersection Construction Membership Problem 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bojańczyk, M., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data trees and xml reasoning. J. ACM 56(3), 1–48 (2009)CrossRefMathSciNetGoogle Scholar
  2. 2.
    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, Los Alamitos (2006)Google Scholar
  3. 3.
    Bouajjani, A., Habermehl, P., Mayr, R.: Automatic verification of recursive procedures with one integer parameter. Theoretical Computer Science 295, 85–106 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In: Csuhaj-Varjú, E., Ésik, Z. (eds.) FCT 2007. LNCS, vol. 4639, pp. 1–22. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  5. 5.
    Brambilla, M., Ceri, S., Comai, S., Fraternali, P., Manolescu, I.: Specification and design of workflow-driven hypertexts. J. Web Eng. 1(2), 163–182 (2003)Google Scholar
  6. 6.
    Büchi, J.: On a decision method in restricted second order arithmetic. In: Int. Congress on Logic, Method, and Philosophy of Science, pp. 1–12. Stanford University Press, Stanford (1962)Google Scholar
  7. 7.
    Ceri, S., Fraternali, P., Bongio, A., Brambilla, M., Comai, S., Matera, M.: Designing Data-Intensive Web Applications. Morgan Kaufmann Publishers Inc., San Francisco (2002)Google Scholar
  8. 8.
    Demri, S., Lazic, R., Nowak, D.: On the freeze quantifier in constraint ltl: Decidability and complexity. Information and Computation 7, 2–24 (2007)CrossRefMathSciNetGoogle Scholar
  9. 9.
    Kaminski, M., Zeitlin, D.: Extending finite-memory automata with non-deterministic reassignment. In: Csuhaj-Varjú, E., Ézik, Z. (eds.) AFL, pp. 195–207 (2008)Google Scholar
  10. 10.
    Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2), 329–363 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  11. 11.
    Markey, N., Schnoebelen, P.: Model checking a path. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 251–265. Springer, Heidelberg (2003)Google Scholar
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    Shemesh, Y., Francez, N.: Finite-state unification automata and relational languages. Information and Computation 114, 192–213 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 14.
    Tan, T.: Pebble Automata for Data Languages: Separation, Decidability, and Undecidability. PhD thesis, Technion - Computer Science Department (2009)Google Scholar
  15. 15.
    Vianu, V.: Automatic verification of database-driven systems: a new frontier. In: ICDT 2009, pp. 1–13. ACM, New York (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Orna Grumberg
    • 1
  • Orna Kupferman
    • 2
  • Sarai Sheinvald
    • 2
  1. 1.Department of Computer ScienceThe TechnionHaifaIsrael
  2. 2.School of Computer Science and EngineeringHebrew UniversityJerusalemIsrael

Personalised recommendations