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 LTL model checking algorithms that rely on a depth-first search order. This paper proposes and experimentally evaluates an algorithm for LTL model checking compatible with the search order prescribed by the sweep-line method. © 2012 Springer-Verlag.
CITATION STYLE
Evangelista, S., & Kristensen, L. M. (2012). Hybrid on-the-fly LTL model checking with the sweep-line method. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7347 LNCS, pp. 248–267). https://doi.org/10.1007/978-3-642-31131-4_14
Mendeley helps you to discover research relevant for your work.