Publication details
Using Accepting Predecessors in Distributed LTL Model
-Checking
| Basic information | |
|---|---|
| Original title: | Using Accepting Predecessors in Distributed LTL Model-Checking |
| Author: | Pavel Moravec |
| Further information | |
|---|---|
| Citation: | MORAVEC, Pavel. Using Accepting Predecessors in Distributed LTL Model-Checking. In MOVEP'04: 6th school on MOdeling and VErifying parallel Processes. Bruxelles, Belgium : Universite Libre de Bruxelles, 2004. pp. 122-129. 2004, Universite Libre de Bruxelles. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | LTL model checking; distributed algorithm |
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. The influence of the ordering on the algorithm performance is open as future work.
Related projects:
- Automated Verification of Parallel and Distributed Systems
- Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
