Relaxed Visibility Enhances Partial Order Reduction |
| |
Authors: | Doron Peled Antti Valmari Ilkka Kokkarinen |
| |
Affiliation: | (1) Bell Laboratories, Lucent Technologies, 600 Mountain Ave., Murray Hill, NJ 07974, USA;(2) Department of Computer Science, Technion, Israel Institute of Technology, Haifa, 32000, Israel;(3) Software Systems Laboratory, Tampere University of Technology, PO Box 553, FIN-33101 Tampere, Finland |
| |
Abstract: | 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, in order to guarantee that the reduced state space preserves the correctness of the checked property, the 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, and thus achieving a better reduction. We demonstrate the benefits of our improved reduction with experimental results. |
| |
Keywords: | automatic verification model checking partial order reduction state space explosion |
本文献已被 SpringerLink 等数据库收录! |
|