Fast detection of cycles in timed automata

We propose a new efficient algorithm for detecting if a cycle in a timed automaton can be iterated infinitely often. Existing methods for this problem have a complexity which is exponential in the number of clocks. Our method is polynomial: it essentially does a logarithmic number of zone canonicalizations. This method can be incorporated in algorithms for verifying B\"uchi properties on timed automata. We report on some experiments that show a significant reduction in search space when our iteratability test is used.

• Publication year

  2014

• Venue

  arXiv.org

• Publication date

  2014-10-15

• Fields of study

  Mathematics, Computer Science

• Identifiers
  arXiv 1410.4509
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Lazy abstractions for timed automata

  2013cited by this paper
• Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction

  2013cited by this paper
• Deciding Conditional Termination

  2012cited by this paper
• Using non-convex approximations for efficient analysis of timed automata

  2011cited by this paper
• Better Abstractions for Timed Automata

  2011cited by this paper
• Efficient On-the-Fly Emptiness Check for Timed Büchi Automata

  2010cited by this paper
• Comparison of Algorithms for Checking Emptiness on Büchi Automata

  2009cited by this paper
• Checking Timed Büchi Automata Emptiness Using LU-Abstractions

  2009cited by this paper
• Flat Parametric Counter Automata

  2009cited by this paper
• Proving Conditional Termination

  2008cited by this paper
• Proving non-termination

  2008cited by this paper
• Termination Of Linear Programs

  2008cited by this paper
• The Power of Hybrid Acceleration

  2006cited by this paper
• Distributed reachability analysis in timed automata

  2005cited by this paper
• Lower and upper bounds in zone-based abstractions of timed automata

  2004cited by this paper
• Relating Hierarchy of Temporal Properties to Model Checking

  2003cited by this paper
• Analysis of Timed Systems Using Time-Abstracting Bisimulations

  2001influential reference
• On-the-Fly Verification of Linear Temporal Logic

  1999cited by this paper
• Timed Automata and the Theory of Real Numbers

  1999cited by this paper
• Multiple Counters Automata, Safety Analysis and Presburger Arithmetic

  1998cited by this paper
• Model Checking of Real-Time Reachability Properties Using Abstractions

  1998cited by this paper
• On nested depth first search

  1996cited by this paper
• The Tool KRONOS

  1996cited by this paper
• Automatic verification of real-time communicating systems by constraint-solving

  1994influential reference
• A Theory of Timed Automata

  1994cited by this paper
• Timing Assumptions and Verification of Finite-State Concurrent Systems

  1989cited by this paper

• Parallel Model Checking Algorithms for Linear-Time Temporal Logic

  2018cites this paper
• Symbolic Optimal Reachability in Weighted Timed Automata

  2016cites this paper