Sciweavers

Share
FMCO
2005
Springer

Cluster-Based LTL Model Checking of Large Systems

10 years 7 months ago
Cluster-Based LTL Model Checking of Large Systems
Abstract. 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. In the automata-based approach to LTL model checking the problem is reduced to the accepting cycle detection problem in a graph. Distributed algorithms, in opposite to sequential ones, cannot rely on depth-first search postorder which is essential for efficient detection of accepting cycles. Therefore, diverse conditions that characterise the existence of cycles in a graph have to be employed in order to come up with efficient and practical distributed algorithms. We compare these algorithms both theoretically and experimentally and determine cases where particular algorithms can be successful.
Jiri Barnat, Lubos Brim, Ivana Cerná
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where FMCO
Authors Jiri Barnat, Lubos Brim, Ivana Cerná
Comments (0)
books