Model checking Petri nets with MSVL

DOI10.1016/j.ins.2016.01.036zbMath1427.68210OpenAlexW2275235874MaRDI QIDQ2279737

Ya Shi, Zhenhua Duan, Cong Tian, Meng Chu 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

Petri netstranslationmodel checkingMSVLPPTL

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 (1)

PPTL specification mining based on LNFG

Uses Software

• Workcraft
• TINA

Cites Work

• Unnamed Item
• Unnamed Item
• Recent advances in unfolding technique
• Maximally permissive liveness-enforcing supervisor with lowest implementation cost for flexible manufacturing systems
• Performance evaluation of Petri nets centralized implementation. The execution time controller
• A practical decision procedure for propositional projection temporal logic with infinite models
• Macro liveness graph and liveness of \(\omega\)-independent unbounded nets
• Observable liveness of Petri nets
• Operational semantics of Framed Tempura
• Expressiveness of propositional projection temporal logic with star
• New Search Strategies for the Petri Net CEGAR Approach
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• The complexity of propositional linear temporal logics
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Interval Abstraction Refinement for Model Checking of Timed-Arc Petri Nets

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