CTL Model Checking with the Sweep-line State Space Exploration Method
Abstract
Model checking is a powerful approach to verification of distributed systems. The sweep-line method alleviates the inherent state explosion problem in model checking by exploiting progress in the system being verified. Verification with the sweep-line method has until now been restricted to verification of safety and linear-time properties. The contribution of this paper is a new model checking algorithm that enables verification of two common branching time properties. The basic idea is to combine the sweep-line method with on-the-fly computation and inspection of strongly connected components. We experimentally evaluate our algorithm on a communication protocol.
Downloads
Download data is not yet available.
Downloads
Published
2017-11-23
Issue
Section
Articles
License
Creative Commons Attribution 4.0 International Public License
https://creativecommons.org/licenses/by/4.0/legalcode.txt