«Abstract. Automated reasoning about systems with inﬁnite domains requires an extension of regular automata to inﬁnite alphabets. Existing ...»
Proof: Assume by way of contradiction that there is a Turing Machine M that, given a VFA, returns an equivalent DVFA or returns that no such DVFA exists. We construct from M a Turing machine M that decides the universality problem for VFA, which, according to Theorem 5, is undecidable.
The machine M proceeds as follows. Given a VFA A, it runs M on A. If M returns that A does not have an equivalent DVFA, then M returns that A is not universal.
Otherwise, M returns a DVFA A equivalent to A. By Theorem 10, M can then check A for universality.
However, it turns out that VFA have an expressive determinizable fragment.
Deﬁnition 2. A VFA is syntactically determinizable if it has no y transitions.
Theorem 13. A syntactically determinizable VFA has an equivalent DVFA.
The full details of the construction are given in the full paper. Here, we show the result of applying the algorithm on the VFA described in Figure 3. For clarity, we do not include in the ﬁgure the transition to the rejecting sinks.
¨ 5 Variable Buchi Automata In , B¨ chi extended NFAs to nondeterministic B¨ chi automata, which run on inﬁnite u u words. The similarity between VFAs and NFAs enables us to extend VFAs to nondeterministic variable B¨ chi automata (VBA, for short). Formally, a VBA is A = Σ, A, u where A is a nondeterministic B¨ chi automaton (NBA). Thus, a run of the pattern auu tomaton A is accepting iff it visits the set of accepting states inﬁnitely often. Similar straightforward extensions can be described for additional acceptance conditions for inﬁnite words. As we specify below, the properties and decision procedures for VFAs generalize to VBA in the expected way, demonstrating the robustness of the VFA formalism.
We start with closure properties. The union construction for VBA is identical to the union construction for VFA. The intersection construction for NBAs involves two copies of the product automaton. Recall that the intersection construction for VFAs involves several copies of the product automaton. Combining the two constructions, we construct the intersection of two VBAs by taking two copies of these several copies.
Therefore, we have the following.
12 O. Grumberg, O. Kupferman, and S. Sheinvald Theorem 14. VBA and DVBA are closed under union and intersection.
As with VFAs, VBAs are not closed under complementation. Recall that a DVFA can be complemented by complementing its pattern automaton. Since deterministic B¨ chi automata are not closed under complementation, so are DVBA. Like determinisu tic B¨ chi automata, a DVFA can be complemented to a VBA, by translating its pattern u automaton to a complementing NBA.
Theorem 15. VBAs and DVBAs are not closed under complementation. A DVBA can be complemented to a VBA.
As for the various decision problems, the complexities and reductions of VFAs all apply, with minor modiﬁcations.
Theorem 16. – The nonemptiness problem for VBA and DVBA is NL-complete.
– The membership problem for VBA is NP-complete and for DVBA is in PTIME.
– The containment problem for VBA is undecidable and for DVBA is in co-NP.
– Deciding whether a given VBA is a DVBA is NL-complete.
1. Boja´ czyk, M., Muscholl, A., Schwentick, T., Segouﬁn, L.: Two-variable logic on data trees n and xml reasoning. J. ACM 56(3) (2009) 1–48
2. Bojanczyk, M., Muscholl, A., Schwentick, T., Segouﬁn, L., David, C.: Two-variable logic on words with data. In: LICS, IEEE Computer Society (2006) 7–16
3. Bouajjani, A., Habermehl, P., Mayr, R.: Automatic veriﬁcation of recursive procedures with one integer parameter. Theoretical Computer Science 295 (2003) 85–106
4. Bouajjani, A., Habermehl, P., Jurski, Y., Sighireanu, M.: Rewriting systems with data. In ´ Csuhaj-Varj´, E., Esik, Z., eds.: FCT. Volume 4639 of LNCS., Springer (2007) 1–22 u
5. Brambilla, M., Ceri, S., Comai, S., Fraternali, P., Manolescu, I.: Speciﬁcation and design of workﬂow-driven hypertexts. J. Web Eng. 1(2) (2003) 163–182
6. B¨ chi, J.: On a decision method in restricted second order arithmetic. In: Int. Congress on u Logic, Method, and Philosophy of Science, Stanford University Press (1962) 1–12
7. Ceri, S., Fraternali, P., Bongio, A., Brambilla, M., Comai, S., Matera, M.: Designing DataIntensive Web Applications. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA (2002)
8. Demri, S., Lazic, R., Nowak, D.: On the freeze quantiﬁer in constraint ltl: Decidability and complexity. Information and Computation 07 (2007) 2–24
9. Kaminski, M., Zeitlin, D.: Extending ﬁnite-memory automata with non-deterministic reas´ signment. In Csuhaj-Varj´, E., Ezik, Z., eds.: AFL, In eds.: (2008) 195–207 u
10. Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2) (1994) 329–363
11. Markey, N., Schnoebelen, P.: Model checking a path. In Amadio, R.M., Lugiez, D., eds.:
CONCUR. Volume 2761 of LNCS., Springer (2003) 248–262
12. Neven, F., Schwentick, T., Vianu, V.: Towards regular languages over inﬁnite alphabets. In:
MFCS ’01, London, UK, Springer-Verlag (2001) 560–572
13. Shemesh, Y., Francez, N.: Finite-state uniﬁcation automata and relational languages. Information and Computation 114 (1994) 192–213
14. Tan, T.: Pebble Automata for Data Languages: Separation, Decidability, and Undecidability.
PhD thesis, Technion - Computer Science Department (2009)
15. Vianu, V.: Automatic veriﬁcation of database-driven systems: a new frontier. In: ICDT ’09, ACM (2009) 1–13