面向目标的自动机网络化简

我们考虑由具有局部状态的有限状态机组成的网络，其局部转换受其他自动机当前状态的条件化。在本文中，我们描述了一种针对特定可达性属性的化简程序，即"从全局状态s出发，存在一序列转换导致到达一个自动机g处于局部状态T'的状态。通过对单个自动机内的转换进行因果分析，提出的化简程序在保留满足可达性属性的所有最小轨迹的同时删除局部转换。该程序的复杂度在总局部状态数和转换数之上为多项式，在单个自动机内的局部状态数之上为指数。应用于建模生物系统动态的自动机网络时，我们观察到化简显著缩小可达状态空间，显著提高了大型网络模型检验的可行性。