Doctoral thesis
Open access

Global Symbolic Model Checking based on Generalised Intervals

ContributorsMorard, Damienorcid
DirectorsBuchs, Didier
Number of pages181
Imprimatur date2024-04-29
Defense date2024

Nowadays, the complexity of systems continues to grow to the point where it is often impossible to analyse them in their entirety. Many of these systems govern our daily lives, from financial management to transportation, including the industries that surround us. A problem in one of these systems can have repercussions on the safety and lives of users.

In an effort to combat these errors, software modelling and verification have become increasingly popular over the decades. Modelling focusses on representing the problem we want to solve, while verification involves checking that the model behaves as expected. In reality, the task of verification is so complex that it becomes impossible to carry out.

To reduce the underlying complexity of model sizes, the symbolic approach is generally used. In our thesis, we developed an original symbolic method. This solution is based on the notion of encoding with internal operations, called homomorphisms. Just as integer intervals encode sets of integers and benefit from operations that work directly on these intervals instead of the sets, our new approach replicates this principle on intervals of vectors. These vectors encode the states of the systems to be verified.

Our new method has enabled the verification of properties on models that are still too complex even for the best tools, using the results of the Model Checking Contest 2022.

  • Global model checking
  • Symbolic model checking
  • CTL
  • Intervals of vectors
  • Generalised intervals
  • Canonicity
  • Petri nets
  • Saturation
  • Model checking contest
  • Symbolic vectors
  • Symbolic vector sets
Citation (ISO format)
MORARD, Damien. Global Symbolic Model Checking based on Generalised Intervals. 2024. doi: 10.13097/archive-ouverte/unige:177272
Main files (1)
Secondary files (1)

Technical informations

Creation05/22/2024 3:45:20 PM
First validation05/24/2024 12:23:44 PM
Update time05/24/2024 12:28:10 PM
Status update05/24/2024 12:28:10 PM
Last indexation05/24/2024 12:28:12 PM
All rights reserved by Archive ouverte UNIGE and the University of GenevaunigeBlack