Affiliations: Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France. [email protected] | Department of Computing, Mathematics, and Physics, Bergen University College, Norway. [email protected]
Note: [] Address for correspondence: Université Paris 13, Sorbonne Paris Cité, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France
Abstract: The sweep-line method allows explicit state model checkers to delete states from memory on-the-fly during state space exploration, thereby lowering the memory demands of the verification procedure. The sweep-line method is based on a least-progress-first search order that prohibits the immediate use of standard on-the-fly Büchi automata-based model checking algorithms that rely on a depth-first search order in the search for an acceptance cycle. This paper proposes and experimentally evaluates an algorithm for Büchi automata-based model checking compatible with the search order and deletion of states prescribed by the sweep-line method.
