Undecidable Problems About Timed Automata

DOI10.1007/11867340_14MaRDI QIDQ3511235zbMATH OpenOpenAlexFDO

Authors Olivier Finkel

Publication date 8 July 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0712.1363

zbMATH Keywords

timed automatadecision problemsdeterminizabilitycomplementabilityuniversality problemshuffle operationminimization of the number of clockstimed Büchi automatatimed regular \((\omega )\)-languages

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Undecidability and degrees of sets of sentences (03D35)

Abstract: We solve some decision problems for timed automata which were recently raised by S. Tripakis in [ Folk Theorems on the Determinization and Minimization of Timed Automata, in the Proceedings of the International Workshop FORMATS'2003, LNCS, Volume 2791, p. 182-188, 2004 ] and by E. Asarin in [ Challenges in Timed Languages, From Applied Theory to Basic Theory, Bulletin of the EATCS, Volume 83, p. 106-120, 2004 ]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed B"uchi automata accepting infinite timed words some of these problems are Pi^1_1-hard, hence highly undecidable (located beyond the arithmetical hierarchy).

Recommendations

• Folk theorems on the determinization and minimization of timed automata
• Formal Modeling and Analysis of Timed Systems
• Undecidability Results for Timed Automata with Silent Transitions
• Automata, Languages and Programming
• When Are Timed Automata Determinizable?

Cited in

(31)

• A survey of timed automata for the development of real-time systems
• Compositional schedulability analysis of real-time actor-based systems
• scientific article; zbMATH DE number 7156375 (Why is no real title available?)
• Folk theorems on the determinization and minimization of timed automata
• CONCUR 2005 – Concurrency Theory
• Formal Modeling and Analysis of Timed Systems
• Off-line test selection with test purposes for non-deterministic timed automata
• Highly Undecidable Problems For Infinite Computations
• Time-Bounded Reachability Problem for Recursive Timed Automata is Undecidable
• A game approach to determinize timed automata
• scientific article; zbMATH DE number 7566065 (Why is no real title available?)
• Classes of timed automata and the undecidability of universality
• Task automata: Schedulability, decidability and undecidability
• History-deterministic timed automata
• State estimation for constant-time labeled automata under dense time
• Untangling the graphs of timed automata to decrease the number of clocks
• Control Strategies for Off-Line Testing of Timed Systems
• Timed Automata with Integer Resets: Language Inclusion and Expressiveness
• Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions
• Automata, Languages and Programming
• Predictive runtime enforcement
• Formal language properties of hybrid systems with strong resets
• Control strategies for off-line testing of timed systems
• Undecidability Results for Timed Automata with Silent Transitions
• Undecidability over Continuous Time
• Equivalence checking and intersection of deterministic timed finite state machines
• Bounded determinization of timed automata with silent transitions
• Bounded determinization of timed automata with silent transitions
• scientific article; zbMATH DE number 7559498 (Why is no real title available?)
• An efficient customized clock allocation algorithm for a class of timed automata
• An introduction to timed automata

This page was built for publication: Undecidable Problems About Timed Automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3511235)