Symbolic Model Checking using Intervals of Vectors

TL;DR

This paper introduces a novel symbolic method using generalized intervals on vectors for Petri net model checking, aiming to mitigate state space explosion and improve performance in global model checking of CTL properties.

Contribution

It presents a new formalization of interval vectors with homomorphic operations and a canonical form, enabling efficient symbolic CTL evaluation on Petri nets.

Findings

Promising results on MCC 2022 examples

Efficient computations via saturation and clustering

Improved performance over existing interval 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.