Cluster-Based LTL Model Checking of Large Systems

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BRIM Luboš ČERNÁ Ivana

Year of publication 2006
Type Article in Proceedings
Conference Formal Methods for Components and Objects
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords distributed LTL model checking
Description In recent years a bundle of parallel and distributed algorithms for verification of finite state systems has appeared. We survey distributed memory enumerative LTL model checking algorithms designed for networks of workstations communicating via MPI. The automata-based approach to LTL model checking reduces the model checking problem to the accepting cycle detection problem. Contrary to sequential algorithms, distributed algorithms cannot rely on depth-first search postorder which is essential for efficient cycle detection. Therefore, they have to employ diverse conditions that characterize the existence of cycles in a graph in order to come up with an efficient and practical solution. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be useful.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.