Fast detection of cycles in timed automata

TL;DR

This paper introduces a polynomial-time algorithm for detecting infinitely repeatable cycles in timed automata, improving efficiency over existing exponential methods and enhancing B"uchi property verification.

Contribution

The paper presents a novel polynomial-time algorithm for cycle detection in timed automata, reducing complexity from exponential to logarithmic in the number of clocks.

Findings

Significant reduction in search space during experiments

Algorithm effectively integrates with B"uchi property verification

Demonstrates practical efficiency improvements

Abstract

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.