One-sentence Summary

Phawade et al. from IIT Dharwad and NIT Calicut propose 2D-BMC, a novel bounded model checking algorithm that simultaneously bounds execution steps and token counts to verify unbounded Petri nets against LTL with linear integer arithmetic (LTL_LIA), enabling concurrent semantics and outperforming existing tools on complex properties.

Key Contributions

• We introduce 2D-BMC, a novel bounded model checking algorithm that simultaneously bounds execution length and token counts in unbounded Petri nets, enabling verification of LTL with linear integer arithmetic (LTL_LIA) properties under concurrent semantics.
• We provide SMT encodings for both interleaved and concurrent executions of unbounded Petri nets, allowing precise specification of token-based invariants and temporal properties that go beyond traditional reachability and coverability.
• We implement and evaluate DCModelChecker 2.0, demonstrating its ability to generate counterexamples on unbounded nets while preserving net structure, and showing competitive performance against tools like TAPAAL and ITS-Tools on selected benchmarks.

Introduction

The authors leverage bounded model checking (BMC) to verify unbounded Petri nets under concurrent semantics, addressing a gap in existing tools that mostly rely on interleaved execution and only check reachability or coverability. Prior approaches struggle to capture true concurrency and lack support for richer temporal properties like those expressible in LTL with linear integer arithmetic (LTL_LIA). Their main contribution is 2D-BMC—a novel BMC variant that bounds both execution length and token count simultaneously—and two tool versions (DCModelChecker 1.0 and 2.0) that implement this approach, enabling verification of LTL_LIA properties with either interleaved or concurrent semantics, while also generating counterexamples for debugging.

Method

The authors leverage a structured approach to model and verify unbounded Petri nets using SMT-based bounded model checking, with a focus on concurrent semantics and two-dimensional bounding. The core methodology integrates formal net semantics, SMT encoding, and a custom toolchain to handle temporal properties expressed in $LTL_{LIA}$LTLLIA​.

The modeling begins with the standard Petri net formalism: a tuple $N = (P, T, F)$N=(P,T,F), where $P$P is a set of places, $T$T a set of transitions, and $F$F a flow function defining directed arcs with optional weights. A marking $M: P \rightarrow \mathbb{N}_0$M:P→N0​ represents the state of the net, indicating token distribution across places. Transitions fire based on the enabledness rule: a transition $t$t is enabled at marking $M$M if $M(p) \geq \text{pre}_N(t, p)$M(p)≥preN​(t,p) for all $p \in P$p∈P. Upon firing, the successor marking $M'$M′ is computed as $M'(p) = M(p) - F(p, t) + F(t, p)$M′(p)=M(p)−F(p,t)+F(t,p) for all $p \in P$p∈P. The reachability graph captures all possible state transitions from an initial marking $M_0$M0​.

As shown in the figure below, the authors distinguish between interleaving and concurrent semantics. In interleaving semantics, only one transition fires per step. In contrast, concurrent semantics allows a subset $\tau' \subseteq \tau$τ′⊆τ of enabled transitions to fire simultaneously, provided the combined token consumption from pre-places does not exceed available tokens. The concurrent firing rule is defined as:

This rule enables a more compact and realistic representation of parallel system behavior.

To enable verification via SMT solvers like Z3, the authors construct a symbolic representation of the net. They define two key matrices: $Wt[m][l]$Wt[m][l] for net weight changes (outgoing minus incoming arcs) and $iWt[m][l]$iWt[m][l] for incident weights (incoming arcs only). The transition function $TF$TF is built by combining preconditions (ensuring sufficient tokens for firing) and postconditions (updating place markings). For concurrent semantics, $TF$TF does not enforce exactly one transition firing per step, unlike interleaving semantics.

The verification target is $LTL_{LIA}$LTLLIA​, a linear temporal logic extended with integer arithmetic over place token counts. Formulas are built from atomic comparisons like $(\#p < \#q)$(#p<#q) and temporal operators (X, F, G, U). To apply bounded model checking, the authors introduce a two-dimensional bound $k = \lambda + \kappa$k=λ+κ, where $\lambda$λ bounds execution steps and $\kappa$κ bounds the total number of tokens. The bounded semantics restricts the state space to runs of length $\lambda$λ with at most $\kappa$κ tokens.

The 2D-BMC encoding $[\mathcal{M}, \psi]_{\langle \lambda, \kappa \rangle}$[M,ψ]⟨λ,κ⟩​ combines the SMT encoding of the net model $[\mathcal{M}]_{\langle \lambda, \kappa \rangle}$[M]⟨λ,κ⟩​ with the negated property $\psi = \neg \phi$ψ=¬ϕ encoded as $[\psi]_{\langle \lambda, \kappa \rangle}^0$[ψ]⟨λ,κ⟩0​ (for loop-free paths) or $l[\psi]_{\langle \lambda, \kappa \rangle}^0$l[ψ]⟨λ,κ⟩0​ (for paths with a loop back to state $l$l). The model encoding is built inductively: $[\mathcal{M}]_{\langle 0, \kappa \rangle}$[M]⟨0,κ⟩​ encodes the initial state with token bounds, and $[\mathcal{M}]_{\langle \lambda, \kappa \rangle}$[M]⟨λ,κ⟩​ extends this by adding the transition relation $T(s_{\lambda-1}, s_{\lambda})$T(sλ−1​,sλ​) and token bounds for the new state.

As shown in the figure below, the 2D-BMC algorithm explores the state space by incrementing $k$k and, for each $k$k, iterating over possible $(\lambda, \kappa)$(λ,κ) pairs. For each pair, it constructs and checks the SMT formula. If satisfiable, a counterexample trace is returned; if unsatisfiable, the bound is increased.

The tool architecture, depicted in the figure below, accepts a Petri net in PNML format and an $LTL_{LIA}$LTLLIA​ property. A pre-processing module, built using ANTLR, parses and validates both inputs, constructing internal data structures. The core model checker then applies the 2D-BMC algorithm, generating SMT constraints for Z3. The solver returns either UNSAT (property holds up to the bound) or SAT with a counterexample trace (property violated).

The workflow begins by negating the property $\phi$ϕ to $\psi$ψ and initializing the bound $k=0$k=0. For each $k$k, it iterates over $(\lambda, \kappa)$(λ,κ) pairs summing to $k$k, constructs the corresponding SMT formula, and queries Z3. The search continues until a counterexample is found or the external termination bound is reached. This systematic exploration ensures comprehensive verification within the bounded state space.

Experiment

• Validated correctness of DCModelChecker 2.0 against ITS-Tools on LTLFireability properties, achieving 90% tool confidence, with agreement on false properties confirming reliability.
• Demonstrated capability to verify FireabilityCardinality properties beyond MCC’s expressiveness, showing increased counterexample discovery with higher bounds.
• Successfully verified unbounded Petri nets where other tools (ITS-Tools, TAPAAL) only report falsity, while DCModelChecker 2.0 provides counterexample traces.
• Verified synthetic invariants in LTL_LIA, a capability absent in both MCC tools and DCModelChecker 1.0, expanding the scope of verifiable properties.
• Tool currently lags in performance versus state-of-the-art due to counterexample generation overhead, with future work targeting concurrent semantics and optimized encoding.

The authors use DCModelChecker 2.0 to verify unbounded Petri nets and compare its performance against DCModelChecker 1.0, ITS-Tools, and TAPAAL, showing that DCModelChecker 2.0 consistently returns false properties with counterexample traces while matching the outcomes of other tools. Results indicate that DCModelChecker 2.0 is slower than ITS-Tools and TAPAAL in execution time but provides additional diagnostic value through counterexample generation. The tool’s ability to handle unbounded nets and generate traces positions it as a complementary option despite current performance limitations.

The authors use DCModelChecker 2.0 to verify LTLFireability properties against ITS-Tools, achieving a tool confidence of 0.90 by comparing results where both tools agree on false properties or where DCModelChecker 2.0 returns counterexamples. Results show that DCModelChecker 2.0 correctly identifies false properties in most cases, though it produces some erroneous outputs when ITS-Tools reports true. The tool’s 2D-BMC strategy is not complete, as indicated by UNSAT results that may become false at higher bounds.