Alternating timed automata

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Alternating timed automata

Full text

Pdf (215 KB)

Source

ACM Transactions on Computational Logic (TOCL) archive
Volume 9 , Issue 2 (March 2008) table of contents

Article No. 10

Year of Publication: 2008

ISSN:1529-3785

Authors

Slawomir Lasota	Institute of Informatics, Warsaw University, Banacha, Warszawa
Igor Walukiewicz	LaBRI, Université Bordeaux-1, Talence cedex, France

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 99, Citation Count: 3

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1342991.1342994 What is a DOI?

ABSTRACT

A notion of alternating timed automata is proposed. It is shown that such automata with only one clock have decidable emptiness problem over finite words. This gives a new class of timed languages that is closed under boolean operations and which has an effective presentation. We prove that the complexity of the emptiness problem for alternating timed automata with one clock is nonprimitive recursive. The proof gives also the same lower bound for the universality problem for nondeterministic timed automata with one clock. We investigate extension of the model with epsilon-transitions and prove that emptiness is undecidable. Over infinite words, we show undecidability of the universality problem.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Parosh Aziz Abdulla , Bengt Jonsson, Verifying Networks of Timed Processes (Extended Abstract), Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.298-312, March 28-April 04, 1998
	2	Parosh Aziz Abdulla , Aletta Nylén, Timed Petri Nets and BQOs, Proceedings of the 22nd International Conference on Application and Theory of Petri Nets, p.53-70, June 25-29, 2001
	3	P. A. Abdulla , K. Cerans , B. Jonsson , Yih-Kuen Tsay, General decidability theorems for infinite-state systems, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.313, July 27-30, 1996
	4	Abdulla, P. A., Deneux, J., Ouaknine, J., and Worrell, J. 2005. Decidability and complexity results for timed automata via channel machines. In Proceedings of the International Colloquium on Automata, Language and Programming (ICALP'05). Lecture Notes in Computer Science, vol. 3580. Springer-Verlag, New York, 1089--1101.
	5	Alur, R., Bernadsky, M., and Madhusudan, P. 2004. Optimal reachability for weighted timed games. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 3124. Springer-Verlag, New York, 122--133.
	6	Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
	7	Rajeev Alur , Limor Fix , Thomas A. Henzinger, Event-clock automata: a determinizable class of timed automata, Theoretical Computer Science, v.211 n.1-2, p.253-273, Jan. 28, 1999 [doi>10.1016/S0304-3975(97)00173-4]
	8	Rajeev Alur , Thomas A. Henzinger , Moshe Y. Vardi, Parametric real-time reasoning, Proceedings of the twenty-fifth annual ACM symposium on Theory of computing, p.592-601, May 16-18, 1993, San Diego, California, United States [doi>10.1145/167088.167242]
	9	Asarin, E., Maler, O., Pnueli, A., , and Sifakis, J. 1998. Controller synthesis for timed automata. In Proceedings of the IFAC Symposium on System Structure and Control. 469--474.
	10	Béatrice Bérard , Antoine Petit , Volker Diekert , Paul Gastin, Characterization of the expressive power of silent transitions in timed automata, Fundamenta Informaticae, v.36 n.2-3, p.145-182, Nov. 1998
	11	Bouyer, P., Cassez, F., Fleury, E., and Larsen, K. G. 2004. Optimal strategies in priced timed game automata. In Proceedings of the FSTTCS'04. Lecture Notes in Computer Science, vol. 3328. Springer-Verlag, New York, 148--160.
	12	Bouyer, P., D'Souza, D., Madhusudan, P., and Petit, A. 2003. Timed control with partial observability. In Proceedings of the CAV'03, Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, 180--192.
	13	Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
	14	Franck Cassez , Thomas A. Henzinger , Jean-François Raskin, A Comparison of Control Problems for Timed and Hybrid Systems, Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control, p.134-148, March 25-27, 2002
	15	Martin Dickhöfer , Thomas Wilke, Timed Alternating Tree Automata: The Automata-Theoretic Solution to the TCTL Model Checking Problem, Proceedings of the 26th International Colloquium on Automata, Languages and Programming, p.281-290, July 11-15, 1999
	16	Catalin Dima, Real-Time Automata and the Kleene Algebra of Sets of Real Numbers, Proceedings of the 17th Annual Symposium on Theoretical Aspects of Computer Science, p.279-289, February 01, 2000
	17	A. Finkel , Ph. Schnoebelen, Well-structured transition systems everywhere!, Theoretical Computer Science, v.256 n.1-2, p.63-92, April 6, 2001 [doi>10.1016/S0304-3975(00)00102-X]
	18	Higman, G. 1952. Ordering by divisibility in abstract algebras. Proc. London Math. Soc. 2, 7, 326--336.
	19	Laroussinie, F., Markey, N., and Schnoebelen, P. 2004. Model checking timed automata with one or two clocks. In Proceedings of the CONCUR'04. Lecture Notes in Computer Science, vol. 3170. Springer-Verlag, New York, 387--401.
	20	Joel Ouaknine , James Worrell, On the Language Inclusion Problem for Timed Automata: Closing a Decidability Gap, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.54-63, July 13-17, 2004 [doi>10.1109/LICS.2004.30]
	21	Joël Ouaknine , James Worrell, On the Decidability of Metric Temporal Logic, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.188-197, June 26-29, 2005 [doi>10.1109/LICS.2005.33]
	22	Ph. Schnoebelen, Verifying lossy channel systems has nonprimitive recursive complexity, Information Processing Letters, v.83 n.5, p.251-261, 15 September 2002 [doi>10.1016/S0020-0190(01)00337-4]
	23	Salvatore La Torre , Margherita Napoli, Timed tree automata with an application to temporal logic, Acta Informatica, v.38 n.2, p.89-116, November 2001 [doi>10.1007/s002360100067]

CITED BY 3

	Parosh Aziz Abdulla , Johann Deneux , Joël Ouaknine , Karin Quaas , James Worrell, Universality Analysis for One-Clock Timed Automata, Fundamenta Informaticae, v.89 n.4, p.419-450, January 2009
	Patricia Bouyer, Model-checking Timed Temporal Logics, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.323-341, March, 2009
	Patricia Bouyer , Serge Haddad , Pierre-Alain Reynier, Undecidability Results for Timed Automata with Silent Transitions, Fundamenta Informaticae, v.92 n.1-2, p.1-25, January 2009