Fast detection of cycles in timed automata
Logic in Computer Science
2014-10-17 v1 Formal Languages and Automata Theory
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.
Keywords
Cite
@article{arxiv.1410.4509,
title = {Fast detection of cycles in timed automata},
author = {Aakash Deshpande and Frédéric Herbreteau and B. Srivathsan and Thanh-Tung Tran and Igor Walukiewicz},
journal= {arXiv preprint arXiv:1410.4509},
year = {2014}
}