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].