The sweep-line state space exploration method

详细信息	查看全文 | 推荐本文 |

• 作者：Kurt Jensen^a ; Lars M. Kristensen^b ; ^{Lars.Michael.Kristensen@hib.no} ; Thomas Mailund^c
• 关键词：Explicit state space exploration ; Model checking ; Concurrent systems ; Verification ; State explosion ; Sweep-line method ; Coloured Petri Nets
• 刊名：Theoretical Computer Science
• 出版年：2012
• 期刊代码：114_03043975
• 类别：cp
• 出版时间：20 April, 2012
• 卷：429
• 期：Complete
• 页码：169-179
• 文件大小：527 K

摘要

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.