Property directed reachability for generalized Petri nets

DOI10.1007/978-3-030-99524-9_28MaRDI QIDQ6535575zbMATHFDO

Authors Nicolas Amat, Silvano Dal Zilio, Thomas Hujsa

Publication date 23 January 2024

zbMATH Keywords

model checkingreachabilityPetri netsSMT solving

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

• Directed reachability for infinite-state systems
• A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
• Generalized property-directed reachability for hybrid systems
• Applications and Theory of Petri Nets 2004
• Compositional reachability in Petri nets

Cites work

• scientific article; zbMATH DE number 1302046 (Why is no real title available?)
• scientific article; zbMATH DE number 2102695 (Why is no real title available?)
• Abstraction-based incremental inductive coverability for Petri nets
• An SMT-based approach to coverability analysis
• Applying CEGAR to the Petri net state equation
• Commodification of accelerations for the Karp and Miller construction
• Directed reachability for infinite-state systems
• Generalized property directed reachability
• Infinite-state invariant checking with IC3 and predicate abstraction
• On the combination of polyhedral abstraction and SMT-based model checking for Petri nets
• Refinement of trace abstraction for real-time programs
• SAT-Based Model Checking without Unrolling
• Semigroups, Presburger formulas, and languages
• State equation, controllability, and maximal matchings of petri nets
• Structural reductions revisited
• TAPAAL 2.0: integrated development environment for timed-arc Petri nets
• The general vector addition system reachability problem by Presburger inductive invariants
• The reachability problem for Petri nets is not elementary
• The tool TINA – Construction of abstract state spaces for petri nets and time petri nets
• Understanding IC3

Cited in

(2)

• On the complexity of proving polyhedral reductions
• Automated polyhedral abstraction proving

This page was built for publication: Property directed reachability for generalized Petri nets

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