Verification of bounded Petri nets using integer programming

DOI10.1007/s10703-006-0022-1zbMath1112.68104OpenAlexW2041613450MaRDI QIDQ878111

Maciej Koutny, Victor Khomenko

Publication date: 26 April 2007

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-0022-1

zbMATH Keywords

Integer programmingPetri netsVerificationNet unfoldingsPartial order techniques

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

Verification of bounded Petri nets using integer programming, Failures: Their Definition, Modelling and Analysis, Occurrence Nets Then and Now: The Path to Structured Occurrence Nets

Uses Software

• CPLEX
• Smodels
• PEP

Cites Work

• Verification of bounded Petri nets using integer programming
• Branching processes of Petri nets
• Operational and denotational semantics for the box algebra
• An efficient incremental algorithm for solving systems of linear diophantine equations
• Model checking using net unfoldings
• Avoiding slack variables in the solving of linear diophantine equations and inequations
• An improvement of McMillan's unfolding algorithm
• Canonical prefixes of Petri net unfoldings
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item