PaperlayerView exact revision on arXiv

Source-linked AI summary

Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets

Lorenzo Capra

arXiv:2609.34891v1cs.SCcs.SE

TL;DR

Symbolic structural invariant verification for High-Level Petri Nets remains limited to restricted Symmetric Net subclasses. This paper applies the SNexpression calculus to ESN flows and sketches broader invariant verification; it reports validation of a wide range of symbolic flows and an initial study of deriving a semiflow basis.

  • Problem

    Symbolic (semi)flow verification is available only for restricted Symmetric Net subclasses, and existing flow-generation approaches impose stringent arc-function constraints.

    Source: §1 · p. 1, §6 · p. 11

  • Method

    The paper extends the SNexpression symbolic calculus to ESN, verifying flows and outlining inductive inference of rewriting rules for broader invariants.

    Source: §1 · pp. 1–2, §8 · p. 14

  • Results

    The authors report validating a wide range of symbolic (semi)flows for ESN and an initial study linking a semiflow basis to the ESN skeleton.

    Source: §9 · p. 16

  • Takeaways & Limitations

    The calculus is also proposed as a way to formally check structural-invariant categories beyond flows.

    Source: §9 · p. 16

    Validating candidate symbolic P-semiflows or colored flows uses a more involved, less streamlined procedure than the approaches in Sections 5 and 7.

    Source: §8 · p. 16

Abstract

from arXiv · show

Structural analysis is central to Petri Net (PN) research, complementing state-space methods while avoiding their combinatorial issues. It is well studied for classical PNs but much less for High-Level Petri Nets (HLPN). Symmetric Nets (SN), a common HLPN formalism, use compact annotations to encode behavioral symmetries, allowing symbolic reachability graphs and associated lumped Markov chains for stochastic SN. In the past two decades, specific structural techniques for SN have emerged, notably the SNexpression tool, which implements a calculus for symbolic structural relations such as conflict and causality. We propose using this calculus to semi-automatically verify symbolic structural invariants, currently possible only for restricted SN subclasses, for an extended SN formalism (ESN) closed under key functional operators. We focus on flows and outline, at least in theory, how to construct a flow-generating family. We also sketch a framework for formally verifying a wider range of invariant properties. Representative examples illustrate the main concepts.

1 Introduction And Related Work

High-Level Petri Nets offer structured models but symbolic structural analysis remains challenging, and established flow-generation techniques cover only restricted subclasses. This paper extends the SNexpression calculus to ESN, focusing on symbolic flows and outlining broader invariant verification.

1 Introduction And Related Work

  • HLPNs use structured tokens and typed nodes, while Symmetric Nets encode behavioral symmetries and support compact symbolic reachability graphs.For stochastic Symmetric Nets, the symbolic graph yields a lumped Markov chain.Source: §1 · p. 1
  • The paper uses SNexpression’s symbolic structural calculus to verify structural invariants, especially symbolic (semi)flows, in extended Symmetric Nets (ESN).The calculus already expresses and computes structural relations such as conflict, causal connection, and mutual exclusion.Source: §1 · p. 1
  • ESN arc functions are closed under key operators, including composition, and the authors know of no other method that verifies symbolic invariants without constraining SN color functions.This complements existing computation of structural dependencies.Source: §1 · p. 2
  • The paper considers symbolic flow verification, colored flows that ignore token multiplicities, a possible semiflow-generating basis, and a broader inductive approach to invariants.The broader approach would require extending the tool to dynamically introduce rewriting rules; most elementary steps for the first three methods were automated.Source: §1 · p. 2
  • Existing symbolic flow-generation results for High-Level Petri Nets cover restricted subclasses, often imposing syntactic constraints that exclude many models.The cited approaches include symbolic elimination procedures, while a method based on generalized inverses has not been automated because computing them is practically infeasible.Source: §1 · p. 2

2 (Extended) Symmetric Nets

The section introduces ESN syntax and its multiset-function machinery, then defines the net components and their domains. Its examples illustrate how color classes, arc functions, guards, and ESN-specific functions describe model behavior.

2 (Extended) Symmetric Nets

  • The production-line example models N parallel lines, each with K interchangeable components, using color classes L and PL of sizes K and N.The places line, ass, and ok have domain PL×L; work moves a token between line and ass for a selected pair of colors.Source: §2 · p. 3

2.1 Multiset functions and operations

  • Multisets assign integer multiplicities to colors, and the section extends pointwise multiset operations to functions and defines function composition through linear extension.Prefix guards act as filters on functions.Source: §2.1 · pp. 3–4

2.2 Extended SN: formal definition

  • An ESN specifies places, transitions, color classes, node domains, input/output/inhibitor arc functions, transition guards, and an initial marking.Color classes can be partitioned or circularly ordered; place domains specify token shapes, transition domains specify instances, and guards restrict those instances.Source: §2.2 · p. 4
  • Arc functions map transition instances to place-domain multisets and are built from class functions and standard predicates, including equality, disequality, ordering, and subclass membership.Negative terms may occur in expressions, but the resulting arc functions must produce natural-multiplicity multisets.Source: §2.2 · p. 4
  • Inhibitor-arc functions are excluded from some CPN definitions and do not affect the flow computation described here.The approach for general invariants in Section 8 considers them.Source: §2.2 · p. 4
  • The ESN example uses an acknowledgment arc function that gathers expected acknowledgments and filters pairs of distinct nodes from a parametric product.Its type is {N → N2 × L}, which the passage says cannot be represented in original SN syntax; calculating its image size uses chromatic-polynomial techniques.Source: §2.2 · p. 5

3 Base Properties Of Arc Functions

The language L is closed under key operations used in symbolic structural analysis, and its set-valued variant supports structural dependencies while ignoring multiplicities. Invariant checking assumes constant-size arc functions, with transition splitting offered to meet that condition.

3 Base Properties Of Arc Functions

  • L is closed under composition, transposition, algebraic sum, difference, and intersection.Source: §3 · p. 5
  • The derived set-valued language retains these closure properties and expresses structural dependencies with natural coefficients and at most one difference symbol.Source: §3 · p. 5
  • Invariant checking assumes constant-size arc functions; transitions can be split so each resulting arc function has constant size.The transformation handles a transition with a size-dependent output.Source: §3 · p. 5
  • Any W in L can be expressed as guarded tuples with unit multiplicities, and equivalence is decidable by reducing both directional differences to 0.The coefficients also support codomain checks.Source: §3 · p. 6

4 Symbolic Flows: Basic Definitions And Properties

The section defines symbolic P- and T-flows through products with the incidence matrix and relates them to invariant markings and firing cycles. It also connects symbolic flows to ordinary flows of the ESN skeleton, reducing the symbolic search space.

4 Symbolic Flows: Basic Definitions And Properties

  • A symbolic P-flow is a non-null place-function vector whose product with H is null; a P-semiflow additionally has natural-multiplicity outputs.Source: §4 · p. 6
  • For every reachable marking, a P-semiflow's value on the marking equals its value on the initial marking.Source: §4 · p. 6
  • A T-semiflow satisfies H·IT ≡ 0 and represents a symbolic firing cycle that returns to the starting marking.Source: §4 · p. 6
  • Taking component sizes maps symbolic P-flows to conventional P-flows of the skeleton, and the analogous result holds for T-flows.Skeleton semiflows therefore provide necessary candidates and substantially reduce the symbolic search space.Source: §4 · p. 6
  • P-flow verification can use ordinary symbolic row-by-column products or the transposed matrix, relating P-flows to T-flows of the dual net.Source: §4 · p. 6

5 Semi-Flows Verification: A Few Examples

The examples use SNexpression to semi-automatically validate candidate symbolic flows and semiflows in ESN models. They show how verified flows describe conserved quantities, firing cycles, and structural boundedness across several model features.

Verification approach

  • The SNexpression-supported calculations validate candidate flows, although the current implementation does not natively support composition in the set-valued function language.The calculations use a simulation of that composition and take a few milliseconds on the reported machine.Source: §5 · pp. 6–7

Example 1

  • Figure 3 presents the distributed production-line incidence matrix alongside candidate P- and T-semiflows for validation.The model’s P-semiflow interpretation identifies conserved workpieces across distributed production lines.Source: §5 · p. 7, Figure 3 · p. 7
  • The distributed production-line model is structurally bounded because its places are covered by flows, and it is color-safe when its initial marking is color-safe.A P-semiflow expresses conservation of workpieces across the distributed production lines; another flow relates the ok and focc places.Source: §5 · p. 7
  • The production-line T-semiflow represents one load, K work occurrences, and one assembly, with no multiplicities in the incidence matrix or flow expressions.The symbolic T-semiflow corresponds to N conventional semiflows, one for each binding of pl.Source: §5 · pp. 7–8

Example 2

  • For the broadcast model, the symbolic calculus verifies the candidate T-semiflow by reducing expressions to normal form and checking that null expressions reduce to zero.The candidate is shown with the incidence matrix in Figure 5.Source: §5 · p. 8, Figure 5 · p. 9
  • The broadcast protocol’s symbolic T-semiflow verifies a complete cycle: one data broadcast, acknowledgments, deliveries, and a final completion event.The cycle’s row-by-column products are nullified; the ESN skeleton has no P-semiflows, while a conventional T-semiflow is given for K = |N|.Source: §5 · p. 8

Example 3

  • For the ordered-class SN, P-semiflows express color-multiset balances, while the T-semiflow describes a firing cycle returning to the starting marking.The example relates its symbolic semiflows to the underlying skeleton’s P- and T-semiflow vectors.Source: §5 · p. 10

Example 4

  • Arc functions with multiplicities greater than one pose no theoretical issue for the calculus, though they are forbidden in the cited approach.One P-semiflow equates the sum of colors in p1’s tuple components with the multiset of colors in p2.Source: §5 · p. 10

6 Generating A Semi-Flow Basis

The section outlines how a semiflow-generating family could be constructed for ESN under a constant-size assumption on arc functions. It demonstrates the reasoning on a simple example, but introduces no algorithm.

Construction approach

  • The proposed construction is a hybrid empirical–theoretical method that exploits Property 4.1 under the assumption that all arc functions have constant size.It uses properties of SN arc functions to reduce the difficulty of deriving a semiflow generative family.Source: §6 · p. 11

Enumeration

  • For a finite set Σ and fixed size k, the relevant set is finite and can be computed explicitly, though enumeration may become costly for large k or composite color domains.Property 4.2 may help with that enumeration problem.Source: §6 · p. 11

Arc-function representation

  • Each arc function can be expressed as a sum of natural-number multiples of tuples that produce unit-multiplicity multisets.The tuples may optionally include a filter.Source: §6 · pp. 11–12

Scope of demonstration

  • The paper demonstrates the construction on a simple example rather than introducing an algorithm, and notes that other examples pose more challenging cases.The example derives symbolic P-semiflows from the basis of the underlying skeleton and identifies a common subdomain for each flow’s places.Source: §6 · p. 12

Illustrative example

  • For the illustrated skeleton, the two P-semiflow basis vectors are [start : 1 line : 1 ass : 1] and [ok : 1 focc : 1].The corresponding common subdomains are L and PL, respectively.Source: §6 · p. 12

7 Colored Flows

Colored semiflows track invariant color types while ignoring token multiplicities, complementing symbolic flows that capture both qualitative and quantitative properties. The section defines their verification and illustrates both failure and success cases.

7 Colored Flows

  • Colored semiflows isolate qualitative invariants of colored markings, which can remain meaningful independently of token counts, including in unbounded models.The section calls these Csemiflows and distinguishes them from symbolic flows that can capture both color types and color number.Source: §7 · p. 12
  • A P-Csemiflow is a vector of set-valued functions whose products with H+ and H− are equivalent.The definition removes multiplicities from the positive and negative terms of the incidence functions.Source: §7 · pp. 12–13
  • The proposed I1 fails verification, while I2 is a Csemiflow preserving the colors in p3 and the first components of tuples in p1.The example derives H+ and H− by splitting a guarded self-loop's incidence function into disjoint positive and negative terms.Source: §7 · p. 13
  • The SNexpression calculus can validate Csemiflows parametrically across color-class cardinalities specified by linear constraints.The reported results hold irrespective of the cardinality of subclass C1; a detailed study of parametric analysis is outside the paper's scope.Source: §7 · p. 13

8 Verifying General Invariants

The section sketches symbolic verification of general structural invariants by proving the property initially and preserving it across symbolic transition firings. It illustrates the approach with constraints involving input and inhibitor arcs.

8 Verifying General Invariants

  • The SN structural calculus can verify properties beyond symbolic or colored semiflows, including properties for unbounded models and models with inhibitor arcs.The section illustrates the approach with an example involving disjointness between token components and colors in two places.Source: §8 · pp. 13–14
  • The proof strategy establishes the invariant in the initial marking, then shows it is preserved by every symbolic transition instance.The preservation step uses SNexpression to infer rewriting axioms, currently manually; automating that inference is planned.Source: §8 · pp. 13–14
  • Input and inhibitor arc constraints are encoded as rewrite rules and applied to the invariant expression during symbolic firing.The section describes substituting the encoded firing conditions and simplifying the resulting expression with composition rules.Source: §8 · pp. 15–16
  • Validating candidate symbolic P-semiflows or colored flows with this methodology is more involved and less streamlined than the approaches in Sections 5 and 7.The paper presents this as a possible use of the methodology, not as its most streamlined application.Source: §8 · p. 16

9 Conclusions

The paper concludes that the SN structural calculus can validate symbolic flows in ESN and sketches both semiflow-basis construction and broader invariant checking. It identifies tool enhancements and symbolic generalized inverses as future work.

9 Conclusions

  • The SN structural calculus implemented in SNexpression validates a wide range of symbolic semiflows and flows for ESN models.The paper also reports an initial study linking a semiflow basis to conventional semiflows of the ESN skeleton.Source: §9 · p. 16
  • The paper outlines applying the calculus to formally check more general categories of structural invariants.The conclusion presents this as an indicated approach, rather than a completed general verification procedure.Source: §9 · p. 16
  • Planned work includes multiset-function composition and interactive axiom inference in SNexpression, interoperability with GreatSPN, and symbolic representation of generalized inverses.The generalized-inverse investigation is intended to support a generative family of symbolic flows.Source: §9 · p. 16

Appendix: proofs, unfolding-skeletons, and conventional semiflows

The appendix proof connects symbolic ESN flows to conventional flows of the underlying skeleton. It also provides model unfoldings, skeleton figures, and a table of conventional semiflows.

Appendix: proofs, unfolding-skeletons, and conventional semiflows

  • The proof shows that the conventional row-by-column product of a symbolic P-flow yields a conventional flow of the ESN skeleton.It uses the constant-size property of the function linear extension.Source: Appendix: proofs, unfolding-skeletons,… · p. 18
  • Figure 13 shows an unfolding of the PL model for N = 2 and K = 2; Table 1 lists P- and T-semiflows for the Petri net shown in Figure 13.Source: Figure 13 · p. 18, Table 1 · p. 18
  • The appendix provides skeleton figures for the PL model and the broadcast model.The captions identify the models but do not describe their structure.Source: Figure 14 · p. 19, Figure 15 · p. 19
Loading 2609.34891v1…