Rethinking Partial-Order Methods

The goal of partial-order methods is to speed up explicit state exploration of concurrent systems. The state space of these systems grows exponentially with the number of components. Yet, explicit state exploration remains one of the main methods for checking safety properties, particularly in timed or probabilistic systems.

The initial idea of partial-order methods is quite natural. If two actions, say b and c, occur in different parts of a concurrent system, executing them in either order—bc or cb—produces the same result. Such permutations of independent actions create an equivalence relation on sequences. Since two equivalent sequences end in the same state, it is sufficient to explore just one representative of each equivalence class. The fewer equivalence classes, the greater the potential gain, and in an extreme case, there could be just one equivalence class.

The first partial-order methods were proposed about 35 years ago under the names of stubborn sets, persistent sets, or ample sets. Since then, there has been a steady flow of literature on the subject. In 2006, Flanagan and Godefroid introduced dynamic reductions, and in 2014, Abdulla proposed some notion of optimality that initiated a new cycle of works on the subject, mostly on so-called stateless exploration methods.

The goal of this talk is not to provide an overview of the existing literature, but rather to make three points. We will start by showing that an optimal stateless method can be directly obtained using so-called lexicographical explorations. Then, we will present a quite strong negative result showing that in most cases, having an optimal partial-order method is impossible. This result justifies looking at heuristics, so in the third part of the talk, we will present a viewpoint that allows for the development of new heuristics, as well as understanding existing ones.