通用时态属性的骨架抽象
摘要：均匀着色的Petri网可以被抽象为它们的骨架，即将着色标记转换为黑色标记的状态/变迁网。彩色网和它的骨架通过一个网映射相关联。在模型检验过程中应用骨架作为抽象方法，我们需要在两个网的状态空间之间建立一种模拟关系。然后，普适时态性质（$ACTL^*$逻辑的性质）将被保留。由网映射引起的抽象关系不一定是模拟关系，这是由于与死锁相关的微妙问题。我们讨论了几种情况，其中由网映射引起的抽象关系也是模拟关系，从而保留了 $ACTL^*$ 特性。我们进一步提出了一种分区细化算法，将一个状态/变迁网折叠为彩色网。这样，骨架抽象方法可以用于给定为状态/变迁网的模型。实验证明了所提出技术的能力。使用骨架抽象，我们能够解决在模型检验竞赛中以前未解决的问题。
作者：Sophie Wallner and Karsten Wolf
论文ID：2112.08884
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22