Abstract.
Timed automata has been developed as a basic semantic model for real time systems. Its algorithmic aspects for automated analysis have been well studied. But so far there is still no satisfactory algebraic theory to allow the derivation of semantical equivalence of automata by purely syntactical manipulation. The aim of this paper is to provide such a theory. We present an inference system of timed bisimulation equivalence for timed automata based on a CCS-style regular language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form \(\phi \rhd t = u\) where \(\phi\) is a clock constraint and t,u are terms denoting timed automata. The inference system is shown to be sound and complete for timed bisimulation. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
Author information
Authors and Affiliations
Additional information
Received: 10 May 2001 / 22 October 2001
Rights and permissions
About this article
Cite this article
Lin, H., Yi, W. Axiomatising timed automata. Acta Informatica 38, 277–305 (2002). https://doi.org/10.1007/s236-002-8035-2
Issue Date:
DOI: https://doi.org/10.1007/s236-002-8035-2