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

Lasse Jacobsen, Morten Jacobsen, Mikael Harkjær Møller, Jiri Srba

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

3 Citationer (Scopus)

Resumé

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.
OriginalsprogEngelsk
BogserieLecture Notes in Computer Science
Vol/bind6342
Sider (fra-til)83-98
ISSN0302-9743
DOI
StatusUdgivet - 2010

Fingerprint

Transition Systems
Model checking
Model Checking
Logic
Petri nets
Timed Automata
Reachability
Petri Nets
Fragment
Arc of a curve
Safety
Trace
Equivalence
Framework
Modeling
Model

Citer dette

Jacobsen, Lasse ; Jacobsen, Morten ; Møller, Mikael Harkjær ; Srba, Jiri. / A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking. I: Lecture Notes in Computer Science. 2010 ; Bind 6342. s. 83-98.
@inproceedings{2a9618d727c84142a72808c58a222c94,
title = "A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking",
abstract = "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.",
author = "Lasse Jacobsen and Morten Jacobsen and M{\o}ller, {Mikael Harkj{\ae}r} and Jiri Srba",
year = "2010",
doi = "10.1007/978-3-642-15784-4_6",
language = "English",
volume = "6342",
pages = "83--98",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Physica-Verlag",

}

A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking. / Jacobsen, Lasse; Jacobsen, Morten; Møller, Mikael Harkjær; Srba, Jiri.

I: Lecture Notes in Computer Science, Bind 6342, 2010, s. 83-98.

Publikation: Bidrag til tidsskriftKonferenceartikel i tidsskriftForskningpeer review

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

VL - 6342

SP - 83

EP - 98

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -