Sequential and parallel implementation of lazy abstraction strategies

Abstract

Verifying timed systems is essential in safety-critical applications and poses significant challenges due to the huge number of possible behaviors. Model checking is a powerful tool of verification exploring the possible behaviors of systems, but it struggles with industrial applications, particularly when time is involved. Abstraction-based techniques are often used for the model checking of complex systems, as they can simplify the representation of the state space. Lazy abstraction is such a technique that incrementally adjusts (refines) abstractions only as needed, thus offering a promising solution by balancing precision and efficiency.

This paper explores both sequential and parallel implementations of lazy abstraction strategies for timed systems. The sequential approach generalizes former implementations, while parallel implementations aim to leverage modern multi-core architectures for improved scalability and efficiency. Through empirical evaluation of benchmark systems, the research compares the various approaches, identifying key factors influencing parallelization effectiveness. The findings offer insights into lazy abstraction and opens new directions to further enhance the verification of complex timed systems.