TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed Automata

Joakim Byg, Morten Jacobsen, Lasse Jacobsen, Kenneth Yrke Jørgensen, Mikael Harkjær Møller, Jiri Srba

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

5 Citationer (Scopus)

Abstrakt

We present a framework for TCTL-preserving translations between time-dependent modeling formalisms. The framework guarantees that once the original and the translated system are in one-by-many correspondence relation (a notion of behavioral equivalence between timed transition systems) then TCTL properties of the original system can be transformed too while preserving the verification answers. We demonstrate the usability of the technique on two reductions from bounded timed-arc Petri nets to networks for timed automata, providing unified proofs of the translations implemented in the verification tool TAPAAL. We evaluate the efficiency of the approach on a number of experiments: alternating bit protocol, Fischer’s protocol, Lynch–Shavit protocol, MPEG-2 encoder, engine workshop and medical workflow. The results are encouraging and confirm the practical applicability of the approach.
OriginalsprogEngelsk
TidsskriftTheoretical Computer Science
Vol/bind537
Udgave nummer5
Sider (fra-til)3-28
Antal sider26
ISSN0304-3975
DOI
StatusUdgivet - 2014

Fingeraftryk Dyk ned i forskningsemnerne om 'TCTL-Preserving Translations from Timed-Arc Petri Nets to Networks of Timed Automata'. Sammen danner de et unikt fingeraftryk.

Citationsformater