计算发生网中的揭示关系
计算机科学中的逻辑
2011-06-08 v1
摘要
Petri网展开是解决验证及相关任务中状态空间爆炸问题的有用工具。此外，其结构允许直接访问事件之间的因果优先、并发和冲突关系。本文进一步探索该数据结构，以确定以下关系：事件a揭示事件b当且仅当a的发生意味着b也必然发生，无论b是在a之前、之后还是与a同时发生。揭示关系的知识尤其有助于在诊断、测试或验证背景下分析部分可观测系统；它还可用于通过抽象生成更简洁的行为表示。揭示关系先前在故障诊断的背景下被引入，其中表明揭示关系是可判定的：对于安全Petri网N的展开U中的给定对(a,b)，U的有限前缀P足以判定a是否揭示b。在本文中，我们首先显著改进了|P|的界。然后，我们证明了存在一种高效算法用于计算给定前缀上的该关系。我们已实现该算法并报告了实验结果。
引用
@article{arxiv.1106.1230,
title = {Computing the Reveals Relation in Occurrence Nets},
author = {Stefan Haar and Christian Kern and Stefan Schwoon},
journal= {arXiv preprint arXiv:1106.1230},
year = {2011}
}
备注
In Proceedings GandALF 2011, arXiv:1106.0814