用于群信息状态空间探测的HIVE工具
The HIVE Tool for Informed Swarm State Space Exploration
摘要：
群验证和并行随机深度优先搜索是在大状态空间中搜索错误的非常有效的并行技术。然而，如果没有错误，并行化的可扩展性就完全丧失了。在最近的工作中，我们提出了一种机制来通知工人探索状态空间的哪些部分。这种机制与任何基于动作的形式主义兼容，其中状态空间可以由标记的转换系统表示。通过这种扩展，每个工作者可以严格限制，每次只能探索状态空间的一小部分。在本文中，我们提出了HIVE工具连同两个搜索算法，这两个搜索算法被添加到LTSmin工具套件中，以执行预处理步骤，并执行有界工人搜索。新的工具是用来协调知情的群体探索，和两个新的LTSmin算法用于预处理模型和执行个人搜索。
英文摘要：
Swarm verification and parallel randomised depth-first search are very effective parallel techniques to hunt bugs in large state spaces. In case bugs are absent, however, scalability of the parallelisation is completely lost. In recent work, we proposed a mechanism to inform the workers which parts of the state space to explore. This mechanism is compatible with any action-based formalism, where a state space can be represented by a labelled transition system. With this extension, each worker can be strictly bounded to explore only a small fraction of the state space at a time. In this paper, we present the HIVE tool together with two search algorithms which were added to the LTSmin tool suite to both perform a preprocessing step, and execute a bounded worker search. The new tool is used to coordinate informed swarm explorations, and the two new LTSmin algorithms are employed for preprocessing a model and performing the individual searches.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
