A Framework for Relating Timed Transition Systems and
Preserving TCTL Model Checking

D 2010

A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

JACOBSEN, Lasse; Morten JACOBSEN; Mikael H. MOLLER a Jiří SRBA

Základní údaje

Originální název

A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking

Autoři

JACOBSEN, Lasse; Morten JACOBSEN; Mikael H. MOLLER a Jiří SRBA

Vydání

Holland, Proceedings of the 7th European Performance Engineering Workshop (EPEW'10), od s. 83-98, 16 s. 2010

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/10:00067235

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-15783-7

ISSN

DOI

https://doi.org/10.1007/978-3-642-15784-4_6

UT WoS

000286404900006

Klíčová slova anglicky

TCTL model checking; timed transition systems; timed automata; Petri nets

Změněno: 29. 4. 2014 06:44, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.

Návaznosti

1M0545, projekt VaV

Název: Institut Teoretické Informatiky

Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky

Citovat

JACOBSEN, Lasse; Morten JACOBSEN; Mikael H. MOLLER a Jiří SRBA. A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking. In Proceedings of the 7th European Performance Engineering Workshop (EPEW'10). Holland: Springer, 2010, s. 83-98. ISBN 978-3-642-15783-7. Dostupné z: https://doi.org/10.1007/978-3-642-15784-4_6.

@inproceedings{910570,
   author = {Jacobsen, Lasse and Jacobsen, Morten and Moller, Mikael H. and Srba, Jiří},
   address = {Holland},
   booktitle = {Proceedings of the 7th European Performance Engineering Workshop (EPEW'10)},
   doi = {https://doi.org/10.1007/978-3-642-15784-4_6},
   keywords = {TCTL model checking; timed transition systems; timed automata; Petri nets},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Holland},
   isbn = {978-3-642-15783-7},
   pages = {83-98},
   publisher = {Springer},
   title = {A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking},
   year = {2010}
}

TY  - CONF
ID  - 910570
AU  - Jacobsen, Lasse - Jacobsen, Morten - Moller, Mikael H. - Srba, Jiří
PY  - 2010
TI  - A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking
PB  - Springer
CY  - Holland
SN  - 9783642157837
KW  - TCTL model checking
KW  - timed transition systems
KW  - timed automata
KW  - Petri nets
N2  - Many formal translations between time dependent models have been proposed over the years. While some of them produce timed bisimilar models, others preserve only reachability or (weak) trace equivalence. We suggest a general framework for arguing when a translation preserves Timed Computation Tree Logic (TCTL) or its safety fragment. The framework works at the level of timed transition systems, making it independent of the modeling formalisms and applicable to many of the translations published in the literature. Finally, we present a novel translation from extended Timed-Arc Petri Nets to Networks of Timed Automata and using the framework argue that it preserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.
ER  -

JACOBSEN, Lasse; Morten JACOBSEN; Mikael H. MOLLER a Jiří SRBA. A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking. In \textit{Proceedings of the 7th European Performance Engineering Workshop (EPEW'10)}. Holland: Springer, 2010, s.~83-98. ISBN~978-3-642-15783-7. Dostupné z: https://doi.org/10.1007/978-3-642-15784-4\_{}6.

Přehled o publikaci