Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata

Tadaaki TANIMOTO; Akio NAKATA; Hideaki HASHIMOTO; Teruo HIGASHINO

doi:10.1093/ietfec/e88-a.11.3007

Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata

Tadaaki TANIMOTO, Akio NAKATA, Hideaki HASHIMOTO, Teruo HIGASHINO

Full Text Views

0

Share
Cite this

Summary :

In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E88-A No.11 pp.3007-3021

Publication Date: 2005/11/01

Publicized

Online ISSN

DOI: 10.1093/ietfec/e88-a.11.3007

Type of Manuscript: Special Section PAPER (Special Section on Concurrent/Hybrid Systems: Theory and Applications)

Category

Cite this

Copy

Tadaaki TANIMOTO, Akio NAKATA, Hideaki HASHIMOTO, Teruo HIGASHINO, "Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata" in IEICE TRANSACTIONS on Fundamentals, vol. E88-A, no. 11, pp. 3007-3021, November 2005, doi: 10.1093/ietfec/e88-a.11.3007.
Abstract: In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.
URL: https://globals.ieice.org/en_transactions/fundamentals/10.1093/ietfec/e88-a.11.3007/_p

Copy

@ARTICLE{e88-a_11_3007,
author={Tadaaki TANIMOTO, Akio NAKATA, Hideaki HASHIMOTO, Teruo HIGASHINO, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata},
year={2005},
volume={E88-A},
number={11},
pages={3007-3021},
abstract={In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.},
keywords={},
doi={10.1093/ietfec/e88-a.11.3007},
ISSN={},
month={November},}

Copy

TY - JOUR
TI - Double Depth First Search Based Parametric Analysis for Parametric Time-Interval Automata
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3007
EP - 3021
AU - Tadaaki TANIMOTO
AU - Akio NAKATA
AU - Hideaki HASHIMOTO
AU - Teruo HIGASHINO
PY - 2005
DO - 10.1093/ietfec/e88-a.11.3007
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E88-A
IS - 11
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - November 2005
AB - In this paper, we propose a parametric model checking algorithm for a subclass of Timed Automata called Parametric Time-Interval Automata (PTIA). In a PTIA, we can specify upper- and lower-bounds of the execution time (time-interval) of each transition using parameter variables. The proposed algorithm takes two inputs, a model described in a PTIA and a property described in a PTIA accepting all invalid infinite/finite runs (called a never claim), or valid finite runs of the model. In the proposed algorithm, firstly we determinize and complement the given property PTIA if it accepts valid finite runs. Secondly, we accelerate the given model, that is, we regard all the actions that are not appeared in the given property PTIA as invisible actions and eliminate them from the model while preserving the set of visible traces and their timings. Thirdly, we construct a parallel composition of the model and the property PTIAs which is accepting all invalid runs that are accepted by the model. Finally, we perform the extension of Double Depth First Search (DDFS), which is used in the automata-theoretic approach to Linear-time Temporal Logic (LTL) model checking, to derive the weakest parameter condition in order that the given model never executes the invalid runs specified by the given property.
ER -