TCTL-preserving translations from timed-arc Petri nets to networks of timed automata

DOI10.1016/J.TCS.2013.07.011MaRDI QIDQ2453531zbMATHOpenAlexFDO

Authors Joakim Byg, Morten Jacobsen, Lasse Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jiří Srba

Publication date 10 June 2014

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2013.07.011

zbMATH Keywords

timed automataformal verificationTCTLtimed-arc Petri nets

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Applications and Theory of Petri Nets 2005
• Structural translation from time Petri nets to timed automata
• From Time Petri Nets to Timed Automata: An Untimed Approach
• A concurrency-preserving translation from time Petri nets to networks of timed automata
• scientific article; zbMATH DE number 2086960

Cites work

• scientific article; zbMATH DE number 2088674 (Why is no real title available?)
• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 1228291 (Why is no real title available?)
• scientific article; zbMATH DE number 1755138 (Why is no real title available?)
• scientific article; zbMATH DE number 5499354 (Why is no real title available?)
• A theory of timed automata
• Advances in verification of time Petri nets and timed automata. A temporal logic approach.
• Applications and Theory of Petri Nets 2005
• Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
• Comparing the Expressiveness of Timed Automata and Timed Extensions of Petri Nets
• Compositional specification of timed systems
• Computer Aided Verification
• Formal Methods for the Design of Real-Time Systems
• Formal Methods for the Design of Real-Time Systems
• Formal Modeling and Analysis of Timed Systems
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Recoverability of Communication Protocols--Implications of a Theoretical Study
• TAPAAL 2.0: integrated development environment for timed-arc Petri nets
• TCTL model checking of time Petri nets
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Timed Petri nets and timed automata: On the discriminating power of Zeno sequences
• Using forward reachability analysis for verification of timed Petri nets
• Verification of Timed-Arc Petri Nets

Cited in

(6)

• From Time Petri Nets to Timed Automata: An Untimed Approach
• TAPAAL 2.0: integrated development environment for timed-arc Petri nets
• Applications and Theory of Petri Nets 2005
• Structural translation from time Petri nets to timed automata
• Verification and parameter synthesis for real-time programs using refinement of trace abstraction
• A concurrency-preserving translation from time Petri nets to networks of timed automata

Describes a project that uses

Uses Software

• Romeo
• TAPAAL
• Kronos
• TINA
• IF-2.0
• PetriNets
• Uppaal
• CMC

This page was built for publication: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2453531)