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

Varování

Publikace nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

JACOBSEN Lasse JACOBSEN Morten MOLLER Mikael H. SRBA Jiří

Rok publikování 2010
Druh Článek ve sborníku
Konference Proceedings of the 7th European Performance Engineering Workshop (EPEW'10)
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-642-15784-4_6
Obor Informatika
Klíčová slova TCTL model checking; timed transition systems; timed automata; Petri nets
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info