How to Cope with Higher Dependency in Partial Order Reduction for LTL Model Checking

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

MORAVEC Pavel

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

Faculty of Informatics

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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info