Time-Action Alternating Model for Timed LOTOS and
its Symbolic Verification of Bisimulation Equivalence
Akio Nakata, Teruo Higashino and Kenichi Taniguchi
Department of Information and Computer Science, Osaka University
E-mail:{nakata,higashino,taniguchi}@ics.es.osaka-u.ac.jp
Abstract
Verification of timed bisimulation equivalence is generally
difficult because of state explosion caused by concrete time values.
In this paper, we propose a verification method to verify timed
bisimulation equivalence of two timed processes using a symbolic
technique similar to [Hennessy and Lin 1995].
We first propose a new model of timed processes,
Alternating Timed Symbolic Labelled Transition System(A-TSLTS).
In A-TSLTS, each state has some parameter variables and those values
determine its behaviour. Each transition in an A-TSLTS has
a guard predicate.
The transition is executable if and only if
its guard predicate is true under specified parameter values.
In the proposed method, we can obtain the weakest condition for a
state-pair in a finite A-TSLTS
to make the state-pair be timed bisimulation
equivalent.
We also show that this result can be applied to the language
LOTOS/T[Nakata et.al. 1993], a timed extension of LOTOS[ISO 1989].