Bounded parametric verification for distributed time Petri nets with discrete-time semantics

DOI10.3233/FI-2010-272MaRDI QIDQ3081898zbMATH OpenFDO

Authors Michał Knapik, Wojciech Penczek, MacIej Szreter, Agata Półrola

Publication date 9 March 2011

Full work available at URL https://doi.org/10.3233/FI-2010-272

zbMATH Keywords

bounded model checkingcomputation tree logic (CTL)distributed systemsPRTECTLverification

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

• SAT-based (parametric) reachability for a class of distributed time Petri nets
• Bounded parametric model checking for elementary net systems
• Bounded Model Checking for Parametric Timed Automata
• A method for parametric verification of the behavior of time Petri nets
• Parametric model-checking of stopwatch Petri nets

Cited in

(8)

• Interpreted synchronous extension of time Petri nets. Definition, semantics and formal analysis
• Using integer time steps for checking branching time properties of time Petri nets
• Bounded parametric model checking for elementary net systems
• SAT-based (parametric) reachability for a class of distributed time Petri nets
• Parametric model checking with VerICS
• Parametric model-checking of stopwatch Petri nets
• Bounded model checking distributed temporal logic
• Verification of bounded Petri nets using integer programming

This page was built for publication: Bounded parametric verification for distributed time Petri nets with discrete-time semantics

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