Undecidable Problems About Timed Automata

We solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. 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 Buchi automata accepting infinite timed words some of these problems are Π11-hard, hence highly undecidable (located beyond the arithmetical hierarchy).

• Publication year

  2006

• Venue

  International Conference on Formal Modeling and Analysis of Timed Systems

• Publication date

  2006-09-25

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1007/11867340_14arXiv 0712.1363
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• On the Shuffle of Regular Timed Languages

  2006cited by this paper
• Decidability and Complexity Results for Timed Automata via Channel Machines

  2005cited by this paper
• On Decision Problems for Timed Automata

  2005cited by this paper
• Timed Shuffle Expressions

  2005cited by this paper
• On the language inclusion problem for timed automata: closing a decidability gap

  2004cited by this paper
• Challenges in Timed Languages: from applied theory to basic theory (Column: Concurrency)

  2004cited by this paper
• Decision Problems for Timed Automata: A Survey

  2004cited by this paper
• Folk Theorems on the Determinization and Minimization of Timed Automata

  2003cited by this paper
• Undecidability of Topological and Arithmetical Properties of Infinitary Rational Relations

  2003cited by this paper
• Timed regular expressions

  2002cited by this paper
• The Expressive Power of Clocks

  1995cited by this paper
• A Theory of Timed Automata

  1994cited by this paper
• Theory of Recursive Functions and Effective Computability.

  1969cited by this paper

• Enforcement of Opacity for Interval Weighted Discrete-Event System by Supervisory Control

  2026cites this paper
• Complex Event Recognition under Time Constraints: Towards a Formal Framework for Efficient Query Evaluation

  2025cites this paper
• State estimation for constant-time labeled automata under dense time

  2024cites this paper
• History-Deterministic Timed Automata

  2023cites this paper
• Tame the infinite—simplification problems for infinite-state systems PhD dissertation in Computer Science

  2022influential citation
• Diagnosing timed automata using timed markings

  2021cites this paper
• Quasi-Equal Clock Reduction On-the-Fly ⋆

  2021cites this paper
• Determinisability of register and timed automata

  2021influential citation
• Equivalence checking and intersection of deterministic timed finite state machines

  2021cites this paper
• Timed games and deterministic separability

  2020cites this paper
• Determinisability of one-clock timed automata

  2020cites this paper
• Clock Reduction in Timed Automata While Preserving Design Parameters

  2019cites this paper
• Timed Automata with Silent Transitions

  2019cites this paper
• Automate sur les structures temporisée

  2019cites this paper
• How to be sure a faulty system does not always appear healthy?

  2019cites this paper
• Real-Time Systems Modeling and Analysis

  2018cites this paper
• On the verification of strictly deterministic behaviour of Timed Finite State Machines

  2018cites this paper
• Clock Allocation in Timed Automata and Graph Colouring

  2018cites this paper
• Control strategies for off-line testing of timed systems

  2018cites this paper
• Online Timed Pattern Matching Using Automata

  2018cites this paper
• Efficient Timed Diagnosis Using Automata with Timed Domains

  2018cites this paper
• On the Determinization of Timed Systems

  2017cites this paper
• Optimal Clock Allocation for a Class of Timed Automata

  2017cites this paper
• Predictive runtime verification of timed properties

  2017cites this paper
• Compositional schedulability analysis of real-time actor-based systems

  2016cites this paper
• Predictive runtime enforcement

  2016cites this paper
• Optimal Clock Allocation for Synthesized Acyclic Timed Automata

  2016cites this paper
• On-the-Fly Determinization of Bounded Networks of Timed Automata

  2016cites this paper
• A Model for Hierarchical Open Real-Time Systems

  2015cites this paper
• Bounded determinization of timed automata with silent transitions

  2015cites this paper
• Synthesis of correct-by-design schedulers for hybrid systems. (Synthèse d'ordonnanceurs corrects par conception pour les systèmes hybrides)

  2014cites this paper
• Almost Periodicity and the Timestamp of Timed Automata

  2014cites this paper
• The Timestamp of Timed Automata

  2014cites this paper
• On alternating timed automata for MITL

  2014cites this paper
• Reducing Clocks in Timed Automata while Preserving Bisimulation

  2014influential citation
• Survey A survey of timed automata for the development of real-time systems

  2013cites this paper
• Contribution to the Verification of Timed Automata: Determinization, Quantitative Verification and Reachability in Networks of Automata. (Contribution à la vérification des automates temporisés : déterminisation, vérification quantitative et accessibilité dans les réseaux d'automates)

  2013cites this paper
• A survey of timed automata for the development of real-time systems

  2013cites this paper
• An Introduction to Timed Automata

  2013cites this paper
• Contribution à la vérification d'automates temporisés : déterminisation, vérification quantitative et accessibilité dans les réseaux d'automates

  2013cites this paper
• Study of concurrency in real-time distributed systems. (La concurrence dans les systèmes temps-réel distribués)

  2012cites this paper
• A Machine-Independent Characterization of Timed Languages

  2012cites this paper
• Three Applications to Rational Relations of the High Undecidability of the Infinite Post Correspondence Problem in a Regular ω-Language

  2011cites this paper
• A game approach to determinize timed automata

  2011cites this paper
• Off-Line Test Selection with Test Purposes for Non-deterministic Timed Automata

  2011cites this paper
• Timed Automata for the Development of Real-Time Systems

  2011cites this paper
• Utilization of timed automata as a verification tool for real-time security protocols

  2010cites this paper
• Introduction Intro to timed automata Region abstraction Limits Extensions Implementation Conclusion

  2010cites this paper
• Kleene-Schützenberger and Büchi theorems for weighted timed automata

  2010cites this paper
• A Game Approach to Determinize Timed Automata ∗ Amélie Stainer

  2010cites this paper
• Formal language properties of hybrid systems with strong resets

  2010cites this paper
• Integer Reset Timed Automata: Clock Reduction and Determinizability

  2010cites this paper
• Highly Undecidable Problems For Infinite Computations

  2009cites this paper
• Undecidability Results for Timed Automata with Silent Transitions

  2009influential citation
• When Are Timed Automata Determinizable?

  2009cites this paper
• Embedded and Real-time Systems

  2009cites this paper
• Determinization and Expressiveness of Integer Reset Timed Automata with Silent Transitions

  2009cites this paper
• Timed Automata with Integer Resets: Language Inclusion and Expressiveness

  2008cites this paper
• An Introduction to Timed Automata

  2005cites this paper
• Predictive Runtime Verification of Timed Properties

  year unknowncites this paper