Axiomatising timed automata |
| |
Authors: | Huimin Lin Wang Yi |
| |
Affiliation: | (1) Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, People's Republic of China (e-mail: lhm@ios.ac.cn), CN;(2) Department of Computer Systems, Uppsala University, Sweden (e-mail: yi@csd.uu.se), SE |
| |
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 where 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.
Received: 10 May 2001 / 22 October 2001 |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|