Classes of Timed Automata and the Undecidability of Universality

• Autorzy: Moura A.V. , Pinto G.A.
• Języki publikacji: EN

Abstrakty

EN

Universality for deterministic Timed Büchi Automata (TBA) is PSPACE-complete but becomes highly undecidable when unrestricted nondeterminism is allowed. More precisely, universality for nondeterministic TBA is P11-hard and its precise position in the analytical hierarchy is still an open question. In this paper we introduce two types of syntactical restrictions to nondeterministic TBA, which are of independent interest, and show that their universality problem is P11-complete. These restrictions define, as we prove, proper subclasses of the class of timed languages defined by nondeterministic TBA. This suggests, as we argue, that no solution to that open question will come without surprise. We also establish closure properties and the relationships between the classes of languages we describe.

Słowa kluczowe

EN

Timed Automata; universality; analytical hierarchy

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 82, nr 1-2
• Strony: 171--184
• Opis fizyczny: bibliogr. 15 poz., wykr.

Twórcy

autor

Moura A.V.

autor

Pinto G.A.

• Department of Computer Science, University of Brasilia, C.P. 4466, 70910-900, Brasilia, DF, Brazil,

Bibliografia

• [1] Alur, R., Dill, D.: A theory of timed automata, Theoretical Computer Science, 126, 1994, 183-235.
• [2] Asarin, E., Maler, O.: Achilles and the Tortoise Climbing Up the Arithmetical Hierarchy, Journal of Computer and System Sciences, 57, 1998, 389-398.
• [3] Bournez, O.: Achilles and the Tortoise Climbing Up the Hyper-Arithmetical Hierarchy, Theoretical Computer Science, 210, 1999, 21-71.
• [4] Castro, J., Cucker, F.: Nondeterministic !-Computations and the Analytical Hierarchy, Zeitschr. f. math. Logik und Grundlagen d. Math., 35, 1989, 333-342.
• [5] Choueka, Y.: Theories of Automata on !-Tapes: A Simplified Approach, Journal of Computer and System Sciences, 8, 1974, 117-141.
• [6] Courcoubetis, C., Yannakakis,M.: The Complexity of Probabilistic Verification, Journal of the ACM, 42(4), 1995, 857-907.
• [7] Harel, D., Pnueli, A., Stavi, J.: Propositional Dynamic Logic of Nonregular Programs, Journal of Computer and System Sciences, 26, 1983, 222-243.
• [8] Henzinger, T., Kopke, P., Wong-Toi, H.: The expressive power of clocks, ICALP 1995, Springer-Verlag, 1995, LNCS 944.
• [9] Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems, Information and Computation, 111, 1994, 193-244.
• [10] Herrmann, P.: Timed Automata and Recognizability, Information Processing Letters, 65, 1998, 313-318.
• [11] Miller, J.: Decidability and Complexity Results for Timed Automata and Semi-linear Hybrid Automata, Hybrid Systems'2000, Springer-Verlag, 2000, LNCS 1790.
• [12] Moura, A., Pinto, G.: Classes of Timed Automata and the Undecidability of Universality, TPTS-Theory and Practice of Timed Systems (ENTCS), 65 (6), Elsevier, 2002.
• [13] Rogers, H.: Theory of Recursive Functions and Effective Computability, The MIT Press, 1987.
• [14] Safra, S.: On the Complexity of !-Automata, Proc. of the 29th IEEE Foundations of Computer Science, October 1988.
• [15] Sistla, A. P.: On Verifying that a Concurrent Program Satisfies a Nondeterministic Specification, Information Processing Letters, 32, 1989, 17-23.