Structural Reductions Revisited
- 30 June 2020
- book chapter
- conference paper
- Published by Springer Science and Business Media LLC
- Vol. 12152, 303-323
- https://doi.org/10.1007/978-3-030-51831-8_15
Abstract
Structural reductions are a powerful class of techniques that reason on a specification with the goal to reduce it before attempting to explore its behaviors. In this paper we present new structural reduction rules for verification of deadlock freedom and safety properties of Petri nets. These new rules are presented together with a large body of rules found in diverse literature. For some rules we leverage an SMT solver to compute if application conditions are met. We use a CEGAR approach based on progressively refining the classical state equation with new constraints, and memory-less exploration to confirm counter-examples. Extensive experimentation demonstrates the usefulness of this structural verification approach.Keywords
This publication has 16 references indexed in Scilit:
- Counting Petri net markings from reduction equationsInternational Journal on Software Tools for Technology Transfer, 2019
- Stubborn versus structural reductions for Petri netsJournal of Logical and Algebraic Methods in Programming, 2019
- Simplification of CTL Formulae for Efficient Model Checking of Petri NetsPublished by Springer Science and Business Media LLC ,2018
- Analysis of Petri Nets and Transition SystemsElectronic Proceedings in Theoretical Computer Science, 2015
- New Efficient Petri Nets Reductions for Parallel Programs VerificationParallel Processing Letters, 2006
- Checking properties of nets using transformationsPublished by Springer Science and Business Media LLC ,2005
- Syntactical Colored Petri Nets ReductionsLecture Notes in Computer Science, 2005
- Counterexample-Guided Abstraction RefinementLecture Notes in Computer Science, 2000
- Verification of Safety Properties Using Integer Programming: Beyond the State EquationFormal Methods in System Design, 2000
- Concurrent system analysis using Petri nets: an optimized algorithm for finding net invariantsComputer Communications, 1988