TIME-ACTION ALTERNATING MODEL FOR TIMED PROCESSES AND ITS SYMBOLIC VERIFICATION OF BISIMULATION EQUIVALENCE

Verification of timed bisimulation equivalence is generally difficult because of the stare explosion caused by concrete time values. In this paper. we propose a verification method to verify rimed bisimulation equivalence of two timed processes using a symbolic technique similar to [1]. We first propose a new model of timed processes. Alternating T imed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, eac h stair has some parameter variables, whose values determine irs behav iour. Each transition in an A-TSLTS has a guard predicate. The transit ion is executable if and only if its guard predicate is true under spe cified parameter values. In the proposed method, we can obtain the wea kest condition for a state-pair in a finite A-TSLTS, which the paramet er values in the weakest condition must satisfy make the state-pair be timed bisimulation equivalent.