Computing Parameterized Invariants of Parameterized Petri Nets

DOI10.3233/FI-222137MaRDI QIDQ5044400zbMATH OpenOpenAlexFDO

Authors Javier Esparza, Mikhail Raskin, Christoph Welzel

Publication date 31 October 2022

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-222137

zbMATH Keywords

first-orderlogicparameterized systemstheorem provingWS1S

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Computing parameterized invariants of parameterized Petri nets
• scientific article; zbMATH DE number 1755152
• Abduction of trap invariants in parameterized systems
• Petri net analysis using invariant generation
• Automatic verification of parameterized networks of processes

Cites work

• An SMT-based approach to coverability analysis
• Analyzing guarded protocols: better cutoffs, more systems, more expressivity
• Approaching the coverability problem continuously
• Checking qualitative liveness properties of replicated systems with stochastic scheduling
• Computing parameterized invariants of parameterized Petri nets
• CONCUR 2004 - Concurrency Theory
• Decidability of parameterized verification
• scientific article; zbMATH DE number 1614699 (Why is no real title available?)
• scientific article; zbMATH DE number 1670768 (Why is no real title available?)
• scientific article; zbMATH DE number 5914356 (Why is no real title available?)
• scientific article; zbMATH DE number 996442 (Why is no real title available?)
• scientific article; zbMATH DE number 1302047 (Why is no real title available?)
• scientific article; zbMATH DE number 1538040 (Why is no real title available?)
• scientific article; zbMATH DE number 2086524 (Why is no real title available?)
• Minimal coverability tree construction made complete and efficient
• Model checking parameterized systems
• On the computation of the minimal coverability set of Petri nets
• Reasoning about networks with many identical finite state processes
• Reasoning about systems with many processes
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Structural Invariants for the Verification of Systems with Parameterized Architectures
• Symbolic model checking with rich assertional languages
• Tight cutoffs for guarded protocols with fairness
• Unbounded-thread program verification using thread-state equations
• Understanding Petri Nets
• Well-structured transition systems everywhere!

Cited in

(4)

• S-invariant analysis of general recursive Petri boxes
• Lifted structural invariant analysis of Petri net product lines
• scientific article; zbMATH DE number 4127001 (Why is no real title available?)
• Abduction of trap invariants in parameterized systems

Describes a project that uses

Uses Software

• MONA
• Potassco
• VAMPIRE
• CVC4
• D-Finder

This page was built for publication: Computing Parameterized Invariants of Parameterized Petri Nets

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