Undecidability Results for Timed Automata with Silent Transitions

• Autorzy: Bouyer P. , Haddad S. , Reynier P-A.
• Języki publikacji: EN

Abstrakty

EN

In this work, we study decision problems related to timed automata with silent transitions (TAε) which strictly extend the expressiveness of timed automata (TA). We first answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TAε can be recognized by some TA? Then we establish in the framework of TAε some old open conjectures that O. Finkel has recently solved for TA. His proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TAε , the proofs in the framework of TAε thus require more elaborated arguments. We establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We also show these results in the framework of infinite timed languages.

Słowa kluczowe

EN

Timed Automata; silent transitions; decidability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 92, nr 1-2
• Strony: 1--25
• Opis fizyczny: Bibliogr. 24 poz.

Twórcy

autor

Bouyer P.

autor

Haddad S.

autor

Reynier P-A.

• LSV, ENS Cachan, 61, avenue du Président Wilson, 94230 Cachan, France,

Bibliografia

• [1] Abdulla, P. A., Deneux, J., Ouaknine, J., Quaas, K., Worrell, J. B.: Universality Analysis for One-Clock Timed Automata, Fundamenta Informaticae, 89(4), 2008.
• [2] Adams, S., Ouaknine, J., Worrell, J.: Undecidability of Universality for Timed Automata with Minimal Resources, Proc. 5th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS' 07), 4763, Springer, 2007.
• [3] Alur, R., Dill, D. L.: Automata for Modeling Real-Time Systems, Proc. 17th International Colloquium on Automata, Languages and Programming (ICALP'90), 443, Springer, 1990.
• [4] Alur, R., Dill, D. L.: A Theory of Timed Automata, Theoretical Computer Science, 126(2), 1994, 183-235.
• [5] Alur, R., Fix, L., Henzinger, Th. A.: A Determinizable Class of Timed Automata, Proc. 6th International Conference on Computer Aided Verification (CAV'94), 818, Springer, 1994.
• [6] Alur, R., Madhusudan, P.: Decision Problems for Timed Automata: A Survey, Proc. 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Real Time (SFM-04:RT), 3185, Springer, 2004.
• [7] Asarin, E.: Challenges in Timed Languages: From Applied Theory to Basic Theory, The Bulletin of the European Association for Theoretical Computer Science, (83), 2004.
• [8] Asarin, E., Caspi, P., Maler, O.: Timed Regular Expressions, Journal of the ACM, 49(2), 2002, 172-206.
• [9] Bérard, B., Diekert, V., Gastin, P., Petit, A.: Characterization of the Expressive Power of Silent Transitions in Timed Automata, Fundamenta Informaticae, 36(2-3), 1998, 145-182.
• [10] Bouyer, P.: A Logical Characterization of Data Languages, Information Processing Letters, 84(2), 2002, 75-85.
• [11] Bouyer, P., Petit, A.: A Kleene/Büchi-like Theorem for Clock Languages, Journal of Automata, Languages and Combinatorics, 7(2), 2002, 167-186.
• [12] Bouyer, P., Petit, A., Thérien, D.: An Algebraic Approach to Data Languages and Timed Languages, Information and Computation, 2002.
• [13] Chevalier, F., D'Souza, D., Prabakhar, P.: On Continuous Timed Automata with Input-Determined Guards, Proc. 26th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'06), 4337, Springer, 2006.
• [14] Dima, C.: Kleene Theorems for Event-Clock Automata, Proc. 12th International Symposium on Fundamentals of Computation Theory (FCT'99), 1684, Springer, 1999.
• [15] Dima, C.: Real-Time Automata, Journal of Automata, Languages and Combinatorics, 6(1), 2001, 3-24.
• [16] Dima, C.: Timed Shuffle Expressions, Proc. 16th International Conference on Concurrency Theory (CONCUR' 05), 3653, Springer, 2005.
• [17] D'Souza, D.: A Logical Characterization of Event Recording Automata, Proc. 6th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'00), 1926, Springer, 2000.
• [18] Finkel, O.: Undecidable Problems About Timed Automata, Proc. 4th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'06), 4202, Springer, 2006.
• [19] Henzinger, Th. A., Kopke, P. W., Wong-Toi, H.: The Expressive Power of Clocks, Proc. 22nd International Colloquium on Automata, Languages and Programming (ICALP'95), 944, Springer, 1995.
• [20] Lasota, S., Walukiewicz, I.: Alternating Timed Automata, ACM Transactions on Computational Logic, 9(2:10), 2008.
• [21] Maler, O., Pnueli, A.: On Recognizable Timed Languages, Proc. 7th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'04), 2987, Springer, 2004.
• [22] Ouaknine, J., Worrell, J.: On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap, Proc. 19th Annual Symposium on Logic in Computer Science (LICS'04), IEEE Computer Society Press, 2004.
• [23] Tripakis, S.: Folk Theorems on the Determinization and Minimization of Timed Automata, Proc. 1st International Workshop on Formal Modeling and Analysis of Timed Systems (FORMATS'03), 2791, Springer, 2003.
• [24] Wilke, Th.: Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata, Proc. 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'94), 863, Springer, 1994.