The sweep-line state space exploration method

TY - JOUR

T1 - The sweep-line state space exploration method

AU - Jensen, Kurt

AU - Kristensen, Lars M.

AU - Mailund, Thomas

PY - 2012

Y1 - 2012

N2 - The sweep-line method exploits intrinsic progress in concurrent systems to alleviate the state explosion problem in explicit state model checking. The concept of progress makes it possible to delete states from the memory during state space exploration and thereby reduce peak memory usage. The contribution of this paper is twofold. First, we provide a coherent presentation of the sweep-line theory and the many variants of the method that have been developed over the past 10 years since the basic idea of the method was conceived. Second, we survey a selection of case studies where the sweep-line method has been put into practical use for the verification of concurrent systems.

AB - The sweep-line method exploits intrinsic progress in concurrent systems to alleviate the state explosion problem in explicit state model checking. The concept of progress makes it possible to delete states from the memory during state space exploration and thereby reduce peak memory usage. The contribution of this paper is twofold. First, we provide a coherent presentation of the sweep-line theory and the many variants of the method that have been developed over the past 10 years since the basic idea of the method was conceived. Second, we survey a selection of case studies where the sweep-line method has been put into practical use for the verification of concurrent systems.

U2 - 10.1016/j.tcs.2011.12.036

DO - 10.1016/j.tcs.2011.12.036

M3 - Journal article

SN - 0304-3975

VL - 429

SP - 169

EP - 179

JO - Theoretical Computer Science

JF - Theoretical Computer Science

ER -