Publication details
Accepting Predecessors are Better than Back Edges in Distributed LTL Model
-Checking.
| Basic information | |
|---|---|
| Original title: | Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. |
| Authors: | Luboš Brim, Ivana Černá, Pavel Moravec, Jiří Šimša |
| Further information | |
|---|---|
| Citation: | BRIM, Luboš - ČERNÁ, Ivana - MORAVEC, Pavel - ŠIMŠA, Jiří. Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In Formal Methods in Computer-Aided Design (FMCAD). Neuveden : Springer-Verlag, LNCS 3312, 2004. ISBN 3-540-23738-0, pp. 352-366. 2004, Austin, USA. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | distributed - memory LTL model checking; graph predecessors |
We present a new distributed-memory algorithm for enumerative LTL model-checking that is designed to be run on a cluster of workstations communicating via MPI. The detection of accepting cycles is based on computing maximal accepting predecessors and the subsequent decomposition of the graph into independent predecessor subgraphs induced by maximal accepting predecessors. Several optimizations of the basic algorithm are presented and the influence of the ordering on the algorithm performance is discussed. Experimental implementation of the algorithm shows promising results.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
