State-space explosion is a central problem in the automatic verification (model-checking) of concurrent systems. Partial order reduction is a method that was developed to try to cope with the state-space explosion. Based on the observation that the order of execution of concurrent (independent) atomic actions is in many cases unimportant for the checked property, it allows reducing the state space by exploring fewer execution sequences. However, to be on the safe side, partial order reductions put constraints about commuting the order of atomic actions that may change the value of propositions appearing in the checked specification. In this paper we relax this constraint, allowing a weaker requirement to be imposed, achieving a better reduction. We demonstrate the benefits of our improved reduction with experimental results.
CITATION STYLE
Kokkarinen, I., Peled, D., & Valmari, A. (1997). Relaxed visibility enhances partial order reduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1254, pp. 328–339). Springer Verlag. https://doi.org/10.1007/3-540-63166-6_33
Mendeley helps you to discover research relevant for your work.