How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking
| Authors | |
|---|---|
| Year of publication | 2005 |
| Type | Article in Proceedings |
| Conference | 1st Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2005) |
| MU Faculty or unit | |
| Citation | |
| Web | http://www.fi.muni.cz/memics05/ |
| Field | Informatics |
| Keywords | model checking; partial order reduction; ample sets |
| Description | Partial order reduction tries to combat the state space explosion problem by reducing the size of the state space. It is based on exploring only a subset of all possible interleavings of independent concurrent processes. However, even in cases when the dependency among processes is small, the method often fails. The reason is that the heuristics actually used to compute the dependency relation are too rough. In this paper we propose a new method which often overcomes the described bottleneck of partial order reduction. |
| Related projects: |