Time-Action Alternating Model for Timed Processes and Its Symbolic Verification of Bisimulation Equivalence

Akio NAKATA; Teruo HIGASHINO; Kenichi TANIGUCHI

Time-Action Alternating Model for Timed Processes and Its Symbolic Verification of Bisimulation Equivalence

Akio NAKATA, Teruo HIGASHINO, Kenichi TANIGUCHI

Full Text Views

0

Cite this

Summary :

Verification of timed bisimulation equivalence is generally difficult because of the 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 [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E80-A No.2 pp.400-406

Publication Date: 1997/02/25

Publicized

Online ISSN

DOI

Type of Manuscript

Category: Concurrent Systems

Cite this

Copy

Akio NAKATA, Teruo HIGASHINO, Kenichi TANIGUCHI, "Time-Action Alternating Model for Timed Processes and Its Symbolic Verification of Bisimulation Equivalence" in IEICE TRANSACTIONS on Fundamentals, vol. E80-A, no. 2, pp. 400-406, February 1997, doi: .
Abstract: Verification of timed bisimulation equivalence is generally difficult because of the 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 [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e80-a_2_400/_p

Copy

@ARTICLE{e80-a_2_400,
author={Akio NAKATA, Teruo HIGASHINO, Kenichi TANIGUCHI, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Time-Action Alternating Model for Timed Processes and Its Symbolic Verification of Bisimulation Equivalence},
year={1997},
volume={E80-A},
number={2},
pages={400-406},
abstract={Verification of timed bisimulation equivalence is generally difficult because of the 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 [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.},
keywords={},
doi={},
ISSN={},
month={February},}

Copy

TY - JOUR
TI - Time-Action Alternating Model for Timed Processes and Its Symbolic Verification of Bisimulation Equivalence
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 400
EP - 406
AU - Akio NAKATA
AU - Teruo HIGASHINO
AU - Kenichi TANIGUCHI
PY - 1997
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E80-A
IS - 2
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - February 1997
AB - Verification of timed bisimulation equivalence is generally difficult because of the 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 [1]. We first propose a new model of timed processes, Alternating Timed Symbolic Labelled Transition System (A-TSLTS). In an A-TSLTS, each state has some parameter variables, whose values determine its behaviour. Each transition in an A-TSLTS has a quard predicate. The transition is executable if and only if its guard predicate is true underspecified parameter values. In the proposed method, we can obtain the weakest condition for a state-pair in a finite A-TSLTS, which the parameter values in the weakest condition must satisfy to make the state-pair be timed bisimulation equivalent.
ER -