Occam's razor applied to the Petri net coverability problem

DOI10.1016/j.tcs.2018.04.014zbMath1402.68134arXiv1607.05956OpenAlexW2885554111MaRDI QIDQ5915567

Grégoire Sutre, Jérôme Leroux, Thomas Geffroy

Publication date: 23 November 2018

Published in: Theoretical Computer Science, Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1607.05956

zbMATH Keywords

invariantmodel-checkingPetri netpre-processingcoverability problem

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

Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Linear equations for unordered data vectors in $[D^k\to{}Z^d$] ⋮ Unnamed Item ⋮ Directed reachability for infinite-state systems ⋮ Computing parameterized invariants of parameterized Petri nets

Uses Software

• z3
• mist

Cites Work

• Unnamed Item
• The covering and boundedness problems for vector addition systems
• Algorithmic analysis of programs with well quasi-ordered domains.
• Approaching the coverability problem continuously
• Parallel program schemata
• Complexity Analysis of Continuous Petri Nets
• An SMT-Based Approach to Coverability Analysis
• State equation, controllability, and maximal matchings of petri nets
• Reasoning about systems with many processes
• Well-structured transition systems everywhere!

This page was built for publication: Occam's razor applied to the Petri net coverability problem