Model Checking Bounded Prioritized Time Petri Nets

DOI10.1007/978-3-540-75596-8_37zbMath1141.68451OpenAlexW1517759046MaRDI QIDQ3510821

Florent Peres, Bernard Berthomieu, 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)

Related Items (3)

Interpreted synchronous extension of time Petri nets. Definition, semantics and formal analysis ⋮ Diagnosability analysis of patterns on bounded labeled prioritized Petri nets ⋮ Relevant timed schedules/clock vectors for constructing time Petri net reachability graphs

Uses Software

• TINA

Cites Work

• Unnamed Item
• CTL* model checking for time Petri nets
• Bridging the Gap Between Timed Automata and Bounded Time Petri Nets
• Model Checking Timed Automata with Priorities Using DBM Subtraction
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Formal Methods for Components and Objects
• Automated Technology for Verification and Analysis
• Formal Modeling and Analysis of Timed Systems

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