WWW.THESIS.XLIBX.INFO FREE ELECTRONIC LIBRARY - Thesis, documentation, books

<< HOME
CONTACTS

Pages:     | 1 | 2 ||

# «Abstract. Automated reasoning about systems with inﬁnite domains requires an extension of regular automata to inﬁnite alphabets. Existing ...»

-- [ Page 3 ] --

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 [6], 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.

References

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

Pages:     | 1 | 2 ||

Similar works:

«Real-Time Online Video Object Silhouette Extraction Using Graph Cuts on the GPU Zachary A. Garrett and Hideo Saito Department of Information and Computer Science, Keio University 3-4-1 Hiyoshi, Kohoku-ku, Yokohama, 223-8522 JAPAN [zgarrett,saito]@hvrl.ics.keio.ac.jp Abstract. Being able to ﬁnd the silhouette of an object is a very important front-end processing step for many high-level computer vision techniques, such as Shape-from-Silhouette 3D reconstruction methods, object shape tracking,...»

«NREL/CP-500-24664 • UC Category: 1210 An Evaluation of Hourly Average Wind-Speed Estimation Techniques Jack Kline RAM Associates Michael Milligan National Renewable Energy Laboratory Presented at Windpower '98 Bakersfield, CA April 27–May 1, 1998 National Renewable Energy Laboratory 1617 Cole Boulevard Golden, Colorado 80401-3393 A national laboratory of the U.S. Department of Energy Managed by Midwest Research Institute for the U.S. Department of Energy under contract No. DE-AC36-83CH10093...»

«Europaisches Patentamt European Patent Office 0 228 846 B1 © Publication number: Office europeen des brevets EUROPEAN SPECIFICATION PATENT © Int. CI.5: C07D 213/73, //A0 1 N 4 3 / 4 0, © © Date of publication of patent specification: 22.04.92 A01 N 4 7 / 3 6 © Application number: 86309666.5 @ Date of filing: 11.12.86 The file contains technical information submitted after the application was filed and not included in this specification © Amino-trifluoromethylpyridine compound and process...»

«Interactive Live-Wire Boundary Extraction William A. Barrett and Eric N. Mortensen Brigham Young University Abstract Live-wire segmentation is a new interactive tool for efficient, accurate, and reproducible boundary extraction which requires minimal user input with a mouse. Optimal boundaries are computed and selected at interactive rates as the user moves the mouse starting from a manually specified seed point. When the mouse position comes in proximity to an object edge, a “live-wire”...»

«BENJAMIN R. LINTNER Rutgers, The State University of New Jersey Department of Environmental Sciences 14 College Farm Road New Brunswick, NJ 08901-8551 Phone: (848) 932-5731 Email: lintner@envsci.rutgers.edu URL: http://envsci.rutgers.edu/~lintner/ _EDUCATION: Ph.D., Physics, University of California-Berkeley, Berkeley, CA, 05/2003. Dissertation: Mechanisms of Passive Tracer Interhemispheric Transport: An Analysis of ModelDerived and Observational Interhemispheric Transport Climatology and...»

«Language Variation and Change, 12 (2000), 295–319. Printed in the U.S.A. © 2001 Cambridge University Press 0954-3945001 \$9.50 Developmental data on a French sociolinguistic variable: Post-consonantal word-final /R/ Jean-Pierre Chevrot Université Stendhal Laurence Beaud Université Rennes 2 R e n a t a Va r g a Université Stendhal ABSTRACT To begin, we review three theoretical problem areas in the field of research into phonological variation in children. Next, we present the results of a...»

<<  HOME   |    CONTACTS
2016 www.thesis.xlibx.info - Thesis, documentation, books

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.