Model Checking Bounded Prioritized Time Petri Nets

DOI10.1007/978-3-540-75596-8_37MaRDI QIDQ3510821zbMATH OpenOpenAlexFDO

Authors Bernard Berthomieu, Florent Peres, François Vernadat

Publication date 3 July 2008

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-75596-8_37

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

• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• Model checking of time Petri nets using the state class timed automaton
• Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
• scientific article; zbMATH DE number 1956600
• TCTL model checking of time Petri nets

Cites work

• Automated Technology for Verification and Analysis
• Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
• CTL* model checking for time Petri nets
• Formal Methods for Components and Objects
• Formal Modeling and Analysis of Timed Systems
• scientific article; zbMATH DE number 1956600 (Why is no real title available?)
• Model Checking Timed Automata with Priorities Using DBM Subtraction
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets

Cited in

(10)

• Getting the priorities right: saturation for prioritised Petri nets
• Interpreted synchronous extension of time Petri nets. Definition, semantics and formal analysis
• scientific article; zbMATH DE number 6708300 (Why is no real title available?)
• scientific article; zbMATH DE number 6719540 (Why is no real title available?)
• A more efficient time Petri net state space abstraction useful to model checking timed linear properties
• scientific article; zbMATH DE number 2113981 (Why is no real title available?)
• Diagnosability analysis of patterns on bounded labeled prioritized Petri nets
• Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs
• Automated Technology for Verification and Analysis
• Verification of bounded Petri nets using integer programming

Describes a project that uses

Uses Software

• TINA

This page was built for publication: Model Checking Bounded Prioritized Time Petri Nets

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