Improving Saturation Efficiency with Implicit Relations
Improving Saturation Efficiency with Implicit Relations
复制标题
利用隐式关系提高饱和效率
DOI：
10.1007/978-3-030-21571-2_17
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Miner, Andrew
中科院分区：
文献类型：
--
作者：
Biswal, Shruti;Miner, Andrew
决策图是一种成熟的数据结构，用于可达集生成和高级模型（如Petri网）的模型检查，这是由于其多功能性和有效算法的可用性。使用决策图来表示高级模型的每个事件的转移关系，饱和算法可以用于构造决策图，该决策图表示从初始状态集合经由零个或多个事件的发生可到达的所有状态。一个困难出现在实践中的模型，其状态变量的界限是未知的，因为过渡关系不能被构造之前的界限是已知的。以前，在飞行中的方法构建的过渡关系沿着与可达性设置在饱和过程中。这可能会影响性能，因为必须重新构建转换关系决策图，并且随着每个状态变量的大小增加，可能需要丢弃计算表条目。在本文中，我们介绍了一种不同的方法的基础上的隐式和不变的表示的过渡关系，从而避免了需要重建的过渡关系和丢弃的计算表条目。我们修改的饱和度算法使用这种新的表示，并证明了它的有效性与几个基准模型上的实验。
Decision diagrams are a well-established data structure for reachability set generation and model checking of high-level models such as Petri nets, due to their versatility and the availability of efficient algorithms for their construction. Using a decision diagram to represent the transition relation of each event of the high-level model, the saturation algorithm can be used to construct a decision diagram representing all states reachable from an initial set of states, via the occurrence of zero or more events. A difficulty arises in practice for models whose state variable bounds are unknown, as the transition relations cannot be constructed before the bounds are known. Previously, on-the-fly approaches have constructed the transition relations along with the reachability set during the saturation procedure. This can affect performance, as the transition relation decision diagrams must be rebuilt, and compute-table entries may need to be discarded, as the size of each state variable increases. In this paper, we introduce a different approach based on an implicit and unchanging representation for the transition relations, thereby avoiding the need to reconstruct the transition relations and discard compute-table entries. We modify the saturation algorithm to use this new representation, and demonstrate its effectiveness with experiments on several benchmark models.
登录
查看更多内容
使用可扩展决策图生成异步系统的符号状态空间
DOI：
10.1007/978-3-540-95891-8_52
发表时间：
2009
期刊：
2010 Seventh International Conference on the Quantitative Evaluation of Systems
影响因子：
--
作者：
Min Wan;Gianfranco Ciardo
通讯作者：
Gianfranco Ciardo
饱和度无限制
DOI：
10.1007/3-540-36577-x_27
发表时间：
2003
期刊：
Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078)
影响因子：
--
作者：
Gianfranco Ciardo;Robert M. Marmorstein;Radu I. Siminiceanu
通讯作者：
Radu I. Siminiceanu
DOI：
10.1007/11562436_32
发表时间：
2005
期刊：
Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078)
影响因子：
--
作者：
J. Couvreur;Y. Thierry
通讯作者：
Y. Thierry
使用决策图隐式 GSPN 可达集生成
DOI：
10.1016/j.peva.2003.07.005
发表时间：
2004
期刊：
Perform. Evaluation
影响因子：
--
作者：
Andrew S. Miner
通讯作者：
Andrew S. Miner
Petri网符号模型检验的区间图技术
DOI：
10.1145/307418.307452
发表时间：
1999
期刊：
Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078)
影响因子：
--
作者：
Karsten Strehl;L. Thiele
通讯作者：
L. Thiele