Publication details
Cluster
-Based LTL Model Checking of Large Systems
| Basic information | |
|---|---|
| Original title: | Cluster-Based LTL Model Checking of Large Systems |
| Authors: | Jiří Barnat, Luboš Brim, Ivana Černá |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří - BRIM, Luboš - ČERNÁ, Ivana. Cluster-Based LTL Model Checking of Large Systems. In Formal Methods for Components and Objects. Berlin : Springer, 2006. ISBN 978-3-540-36749-9, pp. 259-279. 2006, Amsterdam. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | distributed LTL model checking |
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:
- Integrated approach to education of PhD students in the area of parallel and distributed systems
- Techniques for automatic verification and validation of software nad hardware systems
- Institute for Theoretical Computer Science
- Highly Parallel and Distributed Computing Systems
- Automated software verification
