转移系统分解为同步状态机集合
形式语言与自动机理论
2022-05-05 v3 硬件体系结构
系统与控制
系统与控制
摘要
转移系统(TS)和Petri网(PN)是形式化方法中普遍用于对系统建模的重要计算模型。一个重要问题是如何从给定TS中提取一个PN,其可达图与原始TS等价(采用合适的等价概念)。本文研究将转移系统分解为同步状态机(SMs),SMs是一类Petri网,其中每个变迁有一条入弧和一条出弧,且所有标识恰含一个令牌。这是从TS提取PN这一一般问题的重要情形。该分解基于区域理论,并证明区域的称为激发闭包的性质是保证原始TS与SMs分解之间等价的充分条件。给出了一种高效算法,通过将关键步骤归约到最大独立集问题(计算最小无冗余SMs集)或归约到可满足性(合并SMs)来求解该问题。我们报告的实验结果显示了结果质量与计算时间之间的良好权衡。
引用
@article{arxiv.2106.13852,
title = {Decomposition of transition systems into sets of synchronizing state machines},
author = {Viktor Teren and Jordi Cortadella and Tiziano Villa},
journal= {arXiv preprint arXiv:2106.13852},
year = {2022}
}