Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Symbolic Model Checking using Intervals of Vectors

Damien Morard, Lucas Donati, Didier Buchs

TL;DR

The paper tackles state-space explosion in global CTL model checking for Petri nets by introducing symbolic vector sets that generalize interval representations to vectors. It develops a formal framework of symbolic vectors and symbolic vector sets, including a canonical form and homomorphic operations, enabling CTL formula evaluation directly in the symbolic domain. The authors define pre, pre_sv, and pre_svs operators and demonstrate CTL evaluation via fixed-point expressions, with saturation and clustering to mitigate combinatorial blow-up. Benchmarks on MCC 2022 models, particularly the Circadian Clock, show promising scalability and performance improvements, indicating practical viability and potential for integration with other symbolic methods.

Abstract

Model checking is a powerful technique for software verification. However, the approach notably suffers from the infamous state space explosion problem. To tackle this, in this paper, we introduce a novel symbolic method for encoding Petri net markings. It is based on the use of generalised intervals on vectors, as opposed to existing methods based on vectors of intervals such as Interval Decision Diagrams. We develop a formalisation of these intervals, show that they possess homomorphic operations for model checking CTL on Petri nets, and define a canonical form that provides good performance characteristics. Our structure facilitates the symbolic evaluation of CTL formulas in the realm of global model checking, which aims to identify every state that satisfies a formula. Tests on examples of the model checking contest (MCC 2022) show that our approach yields promising results. To achieve this, we implement efficient computations based on saturation and clustering principles derived from other symbolic model checking techniques.

Symbolic Model Checking using Intervals of Vectors

TL;DR

The paper tackles state-space explosion in global CTL model checking for Petri nets by introducing symbolic vector sets that generalize interval representations to vectors. It develops a formal framework of symbolic vectors and symbolic vector sets, including a canonical form and homomorphic operations, enabling CTL formula evaluation directly in the symbolic domain. The authors define pre, pre_sv, and pre_svs operators and demonstrate CTL evaluation via fixed-point expressions, with saturation and clustering to mitigate combinatorial blow-up. Benchmarks on MCC 2022 models, particularly the Circadian Clock, show promising scalability and performance improvements, indicating practical viability and potential for integration with other symbolic methods.

Abstract

Model checking is a powerful technique for software verification. However, the approach notably suffers from the infamous state space explosion problem. To tackle this, in this paper, we introduce a novel symbolic method for encoding Petri net markings. It is based on the use of generalised intervals on vectors, as opposed to existing methods based on vectors of intervals such as Interval Decision Diagrams. We develop a formalisation of these intervals, show that they possess homomorphic operations for model checking CTL on Petri nets, and define a canonical form that provides good performance characteristics. Our structure facilitates the symbolic evaluation of CTL formulas in the realm of global model checking, which aims to identify every state that satisfies a formula. Tests on examples of the model checking contest (MCC 2022) show that our approach yields promising results. To achieve this, we implement efficient computations based on saturation and clustering principles derived from other symbolic model checking techniques.
Paper Structure (18 sections, 27 theorems, 35 equations, 7 figures, 3 tables)

This paper contains 18 sections, 27 theorems, 35 equations, 7 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Informal presentation
  3. Symbolic structure for sets of vectors
  4. Symbolic vectors
  5. Symbolic vector sets
  6. Total order, mergeability and shareability of symbolic vector sets
  7. Canonicity of symbolic vector sets
  8. Canonical operations
  9. Petri net model checking using symbolic vector sets
  10. Encoding markings using symbolic vector sets
  11. Global model checking of Petri nets with symbolic vector sets
  12. Use case: Mutual exclusion
  13. Optimisation through saturation
  14. Optimization: clustering
  15. Benchmarks and results
  16. ...and 3 more sections

Key Result

Lemma 3.8

Let $sv, sv' \in \mathbb{SV}$, then $uf(sv \cap_{sv} sv') = uf(sv) \cap uf(sv')$.

Figures (7)

  • Figure 1: Petri net with two places and one transition
  • Figure 2: Visualisation of the symbolic vector $(\{(1,0), (0,1)\}, \varnothing)$.
  • Figure 3: Visualisation of the symbolic vector $(\{(1,0), (0,1)\}, \{(2,3), (4,1)\})$.
  • Figure 4: Two symbolic vector sets with the same underlying set of vectors.
  • Figure 5: Visualisation of the two symbolic vector sets.
  • ...and 2 more figures

Theorems & Definitions (78)

  • Definition 3.1: Non-strict partial order
  • Definition 3.2: Inclusion relation on vectors
  • Definition 3.3: Symbolic vector
  • Example 3.4
  • Remark 3.5
  • Definition 3.6: Underlying set of vectors
  • Definition 3.7: Intersection of two symbolic vectors
  • Lemma 3.8
  • Example 3.9
  • Definition 3.10: Join
  • ...and 68 more