Source-linked AI summary
Structural Analysis of Hybrid-Trace Nets: An Optimization Approach
Nguyen Cong Nhat Le, Claire N. Bonial, John G. Rogers, Neil T. Dantam
TL;DR
HTrN reachability is computationally challenging because its state spaces can be exponentially large. The paper develops a reachability relaxation and uses it to extract invariants. In tested problems, the approach proves more unreachabilities and generates more invariants faster than the baselines.
Problem
HTrN reachability is computationally challenging because the nets induce exponentially large state spaces.
Source: §I · p. 1Method
The paper develops a reachability relaxation for hybrid trace nets and uses relaxation-based methods to generate affine invariants.
Source: §I · p. 1, §VI · p. 4Results
The approach proves 1.5× more unreachabilities and produces up to 2.5× more invariants, running up to 2 orders of magnitude faster than, in tested problems.
Source: §VII · p. 6Takeaways & Limitations
The relaxation provides a polynomial-time route to invariant generation and fast unreachability verification in hybrid trace nets.
Source: §VIII · p. 7The polynomial-time construction of maximal 1-cardinality invariants is incomplete, so its resulting invariants may not be maximal.
Source: A. Polynomial-time Extraction · p. 4
Abstract
from arXiv · showhide
Fault and error detection is crucial for ensuring the correctness of safety-critical systems. Safety verification often addresses reachability of bad system states, where exhaustive state inspection may be intractable due to the large state spaces of complex systems. We propose a reachability relaxation for hybrid trace nets, a useful mathematical model for analyzing concurrent event systems, to efficiently verify system safety. We further use our relaxation to effectively identify invariants, expressions that hold in all reachable states, allowing state-space reduction for efficient verification. Empirically, our approach proves unsafe states unreachable in 1.5x more instances, generates 2.5x more invariants with up to 2 orders of magnitude faster generation times than the baselines in the tested problems.
I. INTRODUCTION
Hybrid trace nets combine integer, real, and Boolean state for event-driven systems, but their reachability is challenging and their analysis less developed. This work introduces a reachability relaxation and relaxation-based invariant extraction for that setting.
I. INTRODUCTION
- The approach targets HTrN reachability, whose exponentially large state spaces make deciding reachability computationally challenging.The paper proposes a reachability relaxation and effective invariant extraction to address this challenge.Source: §I · p. 1
B. Reachability Analysis
- Existing TN reachability methods include state enumeration, incremental checking, and incomplete routines, while the paper proposes a sound, incomplete polynomial-time linear-relaxation procedure.The cited approaches can be computationally hard in the worst case, and incomplete routines in fail on trace nets.Source: B. Reachability Analysis · p. 1
A. PN Formalisms
- Hybrid trace nets combine ordinary, continuous, and capacity formalisms, extending analysis to a hybrid setting that has received less study.Prior hybrid formalisms reason about ordinary and continuous PNs without TNs, while prior hybrid-TN analyses are limited in finite systems.Source: B. Reachability Analysis · p. 1, A. PN Formalisms · p. 1
C. Invariant Analysis
- Invariants are expressions holding in all reachable states; this work extracts GMECs and P-invariants in original nets rather than synthesizing controlled nets.Prior invariant methods can be impractical or fail to handle all TN transition rules and TN-specific information; relaxation-based analysis requires an over-approximation and can ignore event ordering.Source: C. Invariant Analysis · pp. 1–2
A. Petri Nets
Petri nets model event systems through places, transitions, and token flows; trace nets add Boolean places and specialized flow relations. Hybrid trace nets combine integer, real, and Boolean places with ordinary, continuous, and trace-net flows, and can impose box constraints.
A. Petri Nets
- Ordinary PNs represent event systems with token-bearing places and weighted arcs; continuous PNs allow real-valued token flows, while TNs use Boolean places and specialized flow relations.TN relations include input, output, set, reset, used, free, and nop.Source: A. Petri Nets · p. 2, Table I · p. 2
B. Mixed Integer Linear Programming (MILP)
- A MILP optimizes linear constraints over continuous and discrete variables, with branch-and-bound relaxing integrality to obtain optimistic solutions and prune weak branches.Branch-and-bound maintains bounds from relaxed solutions and the best incumbent.Source: B. Mixed Integer Linear Programming… · p. 2
IV. HYBRID TRACE NETS
- HTrNs combine ordinary, continuous, and trace-net flow relations across integer, real, and Boolean places, and allow box constraints on markings.Box constraints support bounded-state modeling and efficient optimization.Source: §IV · p. 2
A. HTrN Definition
- HTrN places have integer, real, or Boolean token counts, with Boolean counts restricted to 0 or 1; place-type distinctions affect decision and optimization complexity.Places may also have predetermined lower and upper bounds on their token counts.Source: A. HTrN Definition · p. 2
B. HTrN Dynamics
HTrN dynamics map a marking and transition firing to a successive marking. Numeric-place updates use linear equations, while Boolean-place updates use propositional logic to represent their distinct flow relations.
B. HTrN Dynamics
- Numeric places gain tokens from incoming transitions and lose tokens to outgoing transitions, with firing quantities for continuous and discrete transitions.Place bounds must hold before, during, and after a transition firing.Source: B. HTrN Dynamics · p. 3
- Boolean-place token counts update according to TN flow relations, encoded using binary firings for set, output, and used relations, with analogous opposite-polarity encodings for reset, input, and free.The Boolean and numeric place groups use propositional logic and linear equations, respectively.Source: B. HTrN Dynamics · p. 3
- Continuous used and free firings range from 0 to 1, but other TN flow relations cannot be continuous because they change Boolean token counts.Continuous relations must keep Boolean token counts unchanged to preserve integrality.Source: B. HTrN Dynamics · p. 3
V. HTRN REACHABILITY RELAXATION
The HTrN reachability relaxation approximates reachable markings by combining token flows across multiple steps into one step and extending the model to represent set and reset relations.
V. HTRN REACHABILITY RELAXATION
- The extension applies Petri-net linear relaxation to HTrNs by handling set and reset relations that existing relaxations do not capture.The relaxation is also applied to find invariants.Source: §V · p. 3
- The relaxation combines token flows across multiple steps into one step, neglecting transition ordering, to optimistically approximate reachable markings.It uses the incidence matrix and the sum of firing vectors across steps, subject to box constraints.Source: §V · p. 3
- Set and reset transitions require slack variables because their effects rebind Boolean-place counts rather than accumulate linearly.The added non-negative variables adjust relaxed counts so all reachable markings remain included.Source: §V · p. 3
VI. INVARIANT SYNTHESIS
The paper uses reachability relaxation to find affine invariants over places, including mutual-exclusion and token-count forms. Its invariant analysis incorporates TN constraints and offers both a polynomial-time procedure for a class of affine invariants and MILP extraction.
VI. INVARIANT SYNTHESIS
- Invariants are affine constraints over places that hold in all reachable markings, including generalized mutual-exclusion constraints and P-invariants.For Boolean places with 0-1 coefficients, the inequality and equality forms include k-cardinality and k-hot invariants, respectively.Source: §VI · p. 3
- The analysis uses relaxation to incorporate linear constraints inherent in TNs and provides a polynomial-time procedure for a class of affine invariants.It extends relaxation-based analysis to TNs, unlike prior approaches described as computationally hard and applicable only to ordinary PNs.Source: §VI · p. 4
- The paper constructs 1-cardinality and 1-hot invariants in polynomial time, then extracts k-cardinality and k-hot invariants with MILP.The paper relates k-cardinality invariants to optimization-solver clique and cover cuts, and k-hot invariants to compact state-space encodings.Source: §VI · pp. 3–4
A. Polynomial-time Extraction
The polynomial-time method builds cardinality and, under specific transition conditions, 1-hot invariants from pairwise mutexes; a separate MILP method extracts maximal k-cardinality and k-hot invariants using a tightened relaxation.
A. Polynomial-time Extraction
- The polynomial-time method identifies pairwise mutexes, combines them into 1-cardinality invariants, and may convert these into 1-hot invariants.Two Boolean places are mutex when they cannot both be true; pairwise mutexes can produce a quadratic number of expensive constraints.Source: A. Polynomial-time Extraction · p. 4
- A greedy procedure grows each 1-cardinality invariant from one place by adding mutually exclusive places in descending order of shared mutex count.Constructing maximal 1-cardinality constraints is PSPACE-complete, and the greedy procedure can produce non-maximal invariants.Source: A. Polynomial-time Extraction · p. 4
- A 1-cardinality group can yield a 1-hot invariant when one place is initially true and every transition disabling a group place enables another group place.The polynomial-time construction is incomplete, whereas the paper later gives a sound and complete method for maximal k-cardinality invariants from the relaxation.Source: A. Polynomial-time Extraction · p. 4
B. MILP Extraction
- The MILP method constructs constraints, tightens the relaxation with traps, then enumerates maximal k-cardinality invariants; opposite signs on w and d yield k-hot invariants.It uses MILP because invariant enumeration may be exponential.Source: B. MILP Extraction · p. 4
1) Constructing Invariant Constraints:
The method translates the relaxation into affine inequalities and applies Farkas’ lemma to characterize invariant coefficients; it then transforms the resulting constraints, while noting that relaxation alone may miss invariants.
1) Constructing Invariant Constraints:
- The affine system encodes bounds on m⟨h⟩ and nonnegativity of z, while its variables and constants define the vectors and matrix used in the lemma.The invariant coefficients in c apply to m⟨h⟩; coefficients for z are set to zero because the invariant is over places.Source: 1) Constructing Invariant Constraints · pp. 4–5
- Farkas’ lemma converts the condition that an affine inequality holds for every feasible solution into constraints on its coefficients.The paper applies the lemma to the affine system representing the relaxation and inequality (9).Source: 1) Constructing Invariant Constraints · p. 4
- The lemma-derived constraints are transformed by eliminating λE1, λE2, and λN, leaving linear constraints to solve for w and d.A feasible assignment to w, d, λL, and λU yields an inequality invariant of form (9).Source: 1) Constructing Invariant Constraints · p. 5
- The relaxation may miss invariants because it over-approximates reachable markings, so trap constraints are used to tighten it.Traps denote positive token sums over places [31].Source: 1) Constructing Invariant Constraints · p. 5
2) Tightenting Relaxtion with Traps:
The method uses traps to tighten the reachability relaxation for invariant finding, with a trap encoding that accounts for hybrid trace-net flow relations. Minimal traps are then incorporated into the invariant constraints.
2) Tightenting Relaxtion with Traps:
- A trap is a set of places that, once marked, remains marked in every subsequent step; initially marked traps tighten the invariant-finding relaxation.This extends ordinary Petri-net trap reasoning to hybrid trace nets, whose reset and output relations can reverse ordinary token-flow behavior.Source: 2) Tightenting Relaxtion with Traps · p. 5
- The minimal-trap constraints are combined with the relaxation to constrain invariant coefficients and extract invariants.The traps are stacked into a matrix, incorporated into the relaxation, and used in the resulting invariant-extraction constraints.Source: 2) Tightenting Relaxtion with Traps · p. 5
- Trap constraints require an initially marked place and preserve a marked place after any transition that requires one to fire.The encoding uses Boolean-place variables and transition-specific precondition and effect sets.Source: 2) Tightenting Relaxtion with Traps · p. 5
- The method finds minimal traps by repeatedly minimizing the number of selected places and adding constraints to diversify subsequent solutions.Minimality means that removing any place makes the remaining set cease to be a trap; enumeration can be exponentially large in the worst case.Source: 2) Tightenting Relaxtion with Traps · p. 5
3) Enumerating Invariants:
The enumeration procedure uses constraints from the relaxation and traps to generate maximal k-cardinality and k-hot invariants over Boolean places. A MILP searches for unique solutions until no further solution is feasible.
3) Enumerating Invariants:
- The procedure enumerates maximal k-cardinality and k-hot invariants over Boolean places, excluding redundant k-cardinality invariants.A k-cardinality invariant is maximal when flipping any zero coefficient makes it cease to be a k-cardinality invariant.Source: 3) Enumerating Invariants · p. 5
- A MILP repeatedly finds a maximal k-cardinality invariant and converts it to a k-hot invariant when possible, adding constraints to ensure subsequent solutions are unique.The enumeration ends when the MILP becomes infeasible.Source: 3) Enumerating Invariants · pp. 5–6
- For fixed k, a lexicographic objective maximizes Boolean-place coverage, then favors k-hot form; allowing d and d′ to round toward k can yield more invariants.The constraints link invariant coefficients to the relaxation and traps and restrict generated invariants to Boolean places.Source: 3) Enumerating Invariants · p. 6
- After each solve, an added constraint requires the next invariant to include at least one place absent from the previous solution.This prevents subsequent place sets from being subsets of already found solutions.Source: 3) Enumerating Invariants · p. 6
VII. EXPERIMENTS AND DISCUSSION
The experiments compare the relaxation with ITS-tools for safety verification and compare invariant-generation approaches with induction baselines. Across the tested problems, the relaxation and invariant methods outperform the baselines on the reported aggregate measures.
VII. EXPERIMENTS AND DISCUSSION
- The safety-verification time figure covers four trace-net families, with net size increasing from left to right and failures marking timeouts or memory-limit hits.The table captions describe ordinary-PN unreachability counts and invariant counts and generation times across baselines and the two proposed extraction methods.Source: Figure 1 · p. 6, Table II · p. 6, Table III · p. 7
- 1.5× more unreachabilities are proved, while invariant generation produces 2.5× more invariants and runs up to 2 orders of magnitude faster than the baselines in tested problems.The evaluation compares safety verification with ITS-tools and invariant generation with StInG and.Source: §VII · p. 6
- Benchmarks come from MCC and IPC competitions or are self-generated, and experiments use one core of an AMD Ryzen 9 7950X3D under Debian 12.IPC problems include Boolean- and numeric-valued state variables that map to hybrid trace nets.Source: §VII · p. 6
A. Safety Verification
The relaxation improves trace-net safety verification in the tested problems, while invariant-generation methods trade runtime against the number of invariants found. The conclusion reports broader gains over the tested baselines.
A. Safety Verification
- 38 of 40 trace-net instances are proved unreachable by TMKit, versus 25 solved by ITS-tools; performance is comparable on ordinary PNs.TMKit scales better as problem size increases, while ITS-tools verifies approximately the same number of unreachabilities on ordinary PNs.Source: A. Safety Verification · p. 7
- TMKit’s sound, incomplete relaxation uses linear programs for trace nets, whereas ITS-tools relies on expensive state-space computation because its incomplete techniques do not support them.For ordinary PNs, ITS-tools’ complete procedure and support techniques guarantee it finds more unreachabilities than TMKit’s incomplete relaxation.Source: A. Safety Verification · p. 7
B. Invariant Generation
- The polynomial-time method matches or exceeds baselines on 1-cardinality invariants, usually finds more 1-hot invariants, and has the lowest runtime; MILP finds the most invariants but runs slightly longer.The reported tests use four trace nets modeling IPC problems; nontrivial invariants are counted, with 1-hot invariants included as 1-cardinality invariants.Source: B. Invariant Generation · p. 7
- Traps tighten the relaxation and help MILP find more invariants, while the polynomial-time method’s greedy construction keeps runtime lowest.StInG finds fewer invariants and scales poorly; method finds fewer than the proposed approaches because its rigid formulation cannot use information such as box constraints and traps.Source: B. Invariant Generation · p. 7
VIII. CONCLUSIONS
- 1.5× more unreachabilities are proved, with better scaling, and invariant generation produces 2.5× more invariants and runs up to 2 orders of magnitude faster in tested problems.The conclusion attributes the verification result to the linear relaxation and reports the invariant-generation gains against baselines.Source: §VIII · p. 7