Model checking Petri nets with MSVL

DOI10.1016/J.INS.2016.01.036MaRDI QIDQ2279737zbMATH OpenOpenAlexFDO

Authors Ya Shi, Cong Tian, Zhenhua Duan, MengChu Zhou

Publication date 13 December 2019

Published in Information Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ins.2016.01.036

zbMATH Keywords

model checkingPetri netstranslationMSVLPPTL

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 CTL* Model Checker for Petri Nets
• Model checking reconfigurable Petri nets with Maude
• scientific article; zbMATH DE number 408787
• Applications and Theory of Petri Nets 2004
• Sequential and distributed model checking of Petri net specifications
• scientific article; zbMATH DE number 7438162
• Petri nets, traces, and local model checking

Cites work

• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 1744959 (Why is no real title available?)
• A practical decision procedure for propositional projection temporal logic with infinite models
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Expressiveness of propositional projection temporal logic with star
• Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets
• Macro liveness graph and liveness of -independent unbounded nets
• Maximally permissive liveness-enforcing supervisor with lowest implementation cost for flexible manufacturing systems
• New search strategies for the Petri net CEGAR approach
• Observable liveness of Petri nets
• Operational semantics of Framed Tempura
• Performance evaluation of Petri nets centralized implementation. The execution time controller
• Recent advances in unfolding technique
• The complexity of propositional linear temporal logics
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets

Cited in

(5)

• Translating Xd-C programs to MSVL programs
• Model checking of synchronized domain-specific multi-formalism models using high-level Petri nets
• Exploring the properties of MSC documents by translating them into Petri nets
• A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
• PPTL specification mining based on LNFG

Describes a project that uses

Uses Software

• TINA
• Workcraft

This page was built for publication: Model checking Petri nets with MSVL

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