In this paper we present a complete proof system for timed automata. It extends our previous axiomatisation of timed bisimulation for the class of loop-free timed automata with unique fixpoint induction. To our knowledge, this is the first algebraic theory for the whole class of timed automata with a completeness result, thus fills a gap in the theory of timed automata. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes.
CITATION STYLE
Lin, H., & Yi, W. (2000). A complete axiomatisation for timed automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1974, pp. 277–289). Springer Verlag. https://doi.org/10.1007/3-540-44450-5_22
Mendeley helps you to discover research relevant for your work.