Symbolic methods improve verification of colored petri net structures
A Practical Approach To Verifying Structural Invariants In Colored Petri Nets
Symbolic ComputationFormal Languages and Automata Theory
Summary
Checking that certain conditions always hold in complex systems can be difficult, especially when those systems have intricate behaviors. The authors focus on a type of model called Symmetric Nets, which are a form of High-Level Petri Nets that use compact notation to represent repeated patterns. They propose a way to semi-automatically verify important structural properties, called invariants, which help ensure the system behaves correctly. Their approach extends existing tools and theories to cover more types of properties than before, making it easier to analyze these complex models.
What this means in practice
- •For systems engineers: Verify safety-critical system models by checking structural invariants in Symmetric Nets to reduce state-space explosion problems.
- •For software architecture teams: Use symbolic structural analysis to ensure complex concurrent system designs adhere to desired consistency and dependency properties.
Authors
Lorenzo Capra
Abstract
Structural analysis is a core method in Petri Net (PN) research, offering a perspective complementary to state-space techniques while avoiding many of their limitations. It is well studied for classical PNs but far less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, enabling the construction of a symbolic reachability graph (and a lumped Markov chain in stochastic SN) and the execution of symbolic discrete-event simulations. During the past two decades, structural techniques tailored to SN have been developed, notably supported by the SNexpression tool. This tool implements a formal calculus designed for the computation of symbolic structural relations, including, but not limited to, conflict relations and causal dependencies. Here, we focus on using this calculus to verify semi-automatically symbolic structural invariants, a task currently feasible only for certain restricted SN subclasses. We focus specifically on (semi)flows and briefly discuss an approach through which a flow generative family can be generated, at least theoretically. We further briefly outline a framework for the formal verification of a broader class of invariant properties. An extended formulation of the SN formalism is employed, which demonstrably satisfies the closure property with respect to fundamental functional operators. The core concepts are elucidated by means of representative examples throughout the exposition.