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

Varování

Publikace nespadá pod Filozofickou fakultu, 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:	Institut Teoretické Informatiky