Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets

DOI10.1007/978-3-319-10512-3_17MaRDI QIDQ5500572zbMATH OpenOpenAlexFDO

Authors Sine Viesmose Birch, Thomas Stig Jacobsen, Jacob Jon Jensen, Christoffer Moesgaard, Niels Nørgaard Samuelsen, Jiří Srba

Publication date 6 August 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10512-3_17

Mathematics Subject Classification ID

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

• Verification of Timed-Arc Petri Nets
• Abstractions and partial order reductions for checking branching properties of time Petri nets
• scientific article; zbMATH DE number 1439078
• Model checking of time Petri nets based on partial order semantics
• Interval semantics for Petri nets with inhibitor arcs
• Specification and model checking of temporal properties in time Petri nets and timed automata
• TCTL model checking of time Petri nets
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• Verification of reachability properties for time Petri nets
• Model checking of time Petri nets using the state class timed automaton

Cited in

(5)

• Using approximation for the verification of token-scaling models
• Model checking Petri nets with MSVL
• Verification of Timed-Arc Petri Nets
• From many places to few: automatic abstraction refinement for Petri nets
• From Many Places to Few: Automatic Abstraction Refinement for Petri Nets

Describes a project that uses

Uses Software

• TAPAAL
• Uppaal

This page was built for publication: Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets

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