TY - GEN
T1 - A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking
AU - Jacobsen, Lasse
AU - Jacobsen, Morten
AU - Møller, Mikael Harkjær
AU - Srba, Jiri
PY - 2010
Y1 - 2010
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 itpreserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.
AB - 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 itpreserves the full TCTL. The translation has been implemented in the verification tool TAPAAL.
U2 - 10.1007/978-3-642-15784-4_6
DO - 10.1007/978-3-642-15784-4_6
M3 - Conference article in Journal
SN - 0302-9743
VL - 6342
SP - 83
EP - 98
JO - Lecture Notes in Computer Science
JF - Lecture Notes in Computer Science
ER -