arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2609.34891

Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets

Lorenzo Capra
View original source ↗Read source document ↗Export metadata ↓

Abstract

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.

Explore related subjects

cs.SCcs.SE

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Lorenzo Capra. 2026-09-28. Semi-automated Verification of Symbolic Invariants In Extended Symmetric Nets. https://doi.org/10.4204/eptcs.452.12

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

A Practical Approach To Verifying Structural Invariants In Colored Petri Nets

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.

cs.SC↗
arXiv2026

Fast Deterministic Normal Bases and Circulant Polynomial Determinants

Let $\mathsf{E}=\mathbb{F}_q[x]/(Γ)$ describe an algebraic extension of a finite field $\mathbb{F}_q$, where $q$ is a prime power and $Γ\in\mathbb{F}_q[x]$ is monic and irreducible of degree $n$. We give a deterministic algorithm that finds $β\in \mathsf{E}$ whose conjugates $β,β^q,\ldots,β^{q^{n-1}}$ form an $\mathbb{F}_q$-basis of $\mathsf{E}/\mathbb{F}_q$, a normal basis, using $O_ε((n^2\log q)^{1+ε})+{O\tilde{}}(n\log^2 q)$ bit operations for any $ε>0$. For $n>1$, let $θ=x\bmodΓ$, so $\mathsf{E}=\mathbb{F}_q[θ]$. A variant of a construction of Artin shows that $β_t=(θ-t)^{-1}$ is normal for all but at most $n(n-1)$ parameters $t\in\mathbb{F}_q$. We present an algorithm to construct an $n\times n$ circulant matrix over $\mathbb{F}_q[\mathcal T]$, for an indeterminate $\mathcal T$, whose determinant at $\mathcal T=t$ is non-zero precisely when $β_t$ is normal, and show this algorithm requires ${O\tilde{}}(n^2+n\log q)$ operations in $\mathbb{F}_q$. Then, as a primary subroutine, using triangular-set power projection and modular composition, we show how to compute the determinant of any $n\times n$ circulant over $\mathbb{F}_q[\mathcal T]$, given by its first row of polynomials of degree at most $m\geq1$, using $O_ε((nm\log q)^{1+ε})$ bit operations. For $q\leq n(n-1)$, we show how to embed our problem into a sufficiently large field extension, construct a normal basis there, and descend to the ground field, within the same stated cost.

cs.SC↗
arXiv2026

The Moment Method for Computing Real Points of Sparse Polynomial Systems

One of the most important problems in computational algebra is the computation of real solutions of a polynomial system. Lasserre, Laurent, and Rostalski introduced a numerical method to compute the real radical of an ideal defining a finite set of real points. Their method is based on moment matrices and reduces the problem to solving a semidefinite program. In this work, we build on this method and on the work of Laurent and Mourrain to exploit the sparsity of the input polynomials. For this purpose, we extend the theory of moment matrices to the setting of affine toric varieties. We prove that, for sparse polynomial systems, this approach allows us to recover real points on affine toric varieties. Moreover, we show that a projection of the spectrahedron associated with the semidefinite program is, in fact, a polytope, and we propose a variation of the method to compute only one real solution of the system.

cs.SC↗