并行LSC验证下的POSA分解优化与模型检查

本文主要探讨了"并行LSC验证下的偏序符号自动机"这一主题，其核心在于利用理论计算机科学中的偏序符号自动机（POSA）来提供一种可视化的语义基础，特别是在实时序列图（LSC）的上下文中。LSC是一种表达对象间交互的图形工具，对于系统设计中的模块间通信建模尤其重要。POSA因其在LSC中的应用，其验证过程中的复杂性问题与模型的规模密切相关，特别是当考虑到LSC的并发性，如元素观察顺序的放宽，这会直接影响模型检查的时间效率。 文章关注的是POSA与确定性状态的关系，尤其是那些具有不相交注释传出转换的状态分解特性。研究者设计了一种程序，该程序能够将一个POSA分解为多个确定性状态的POSA的交集，结果表明，这种分解不仅保持了原POSA语言的不变性，而且在主导态分解的情况下，生成的POSA具有更小的规模。这个发现对于LSC的模型检查具有重要意义，因为大部分在处理LSC时得到的POSA状态通常都是确定性和支配性的，这意味着模型检查可以有效地分布执行，从而显著提高验证的效率。 此外，本文的工作还得到了德国研究委员会（DFG）的支持，分别在SFB/TR14AVACS跨区域合作研究中心和项目USE（DA206/7-3）的优先计划SPP1064中展开。作者提供了他们的联系方式以便进一步交流。 总结来说，这篇论文深入研究了如何通过并行方法和POSA的特性来优化LSC的模型验证过程，这对于实际系统设计中的模块化和并发性管理具有实用价值。同时，它还展示了理论研究与实际应用的结合，促进了自动化工具的发展，有助于提升系统设计和验证的效率。