The major problem of checking a parallel composition of real-time systems for a real-time property is the explosion of untimed states and time regions. To atack this problem, one can use bisimulation equivalence w.r.t.the property to be checked to minimise the system state space. In this paper, we define such equivalence for the integrated linear duration properties of real-time automaton networks with shared variables. To avoid exhaustive state space exploration, we define a compatibility relation, which is a one-direction simulation relation between configurations. Based on this technique, we develop an algorithm for checking a real-time automaton network with shared vriables w.r.t. a linear duration property. Our algorithm can avoid exhaustive state space exploration significantly when applied to Fischer's mutual exclusion protocol.
展开▼
