Getting the Priorities Right: Saturation for Prioritised Petri Nets
Getting the Priorities Right: Saturation for Prioritised Petri Nets
复制标题
DOI：
10.1007/978-3-319-57861-3_14
复制
发表时间：
2017-06
期刊：
影响因子：
--
通讯作者：
Kristóf Marussy;V. Molnár;András Vörös;I. Majzik
中科院分区：
文献类型：
--
作者：
Kristóf Marussy;V. Molnár;András Vörös;I. Majzik
优先Petri网是一种功能强大的建模语言，通常构成更具表达力的建模语言（如GSPN）的核心。饱和状态空间遍历算法已被证明是有效的非优先并发模型。以前的工作表明，优先级可能会被编码到过渡关系，但这样做的主要思想的饱和破坏的过渡的局部性。本文提出了一种扩展的饱和度，本机处理优先级通过考虑优先级相关的启用转换分开，采用约束饱和的思想。为了对每个状态中启用的转换的最高优先级进行编码，我们引入了边值区间决策图。我们表明，在Petri网的情况下，这种数据结构可以离线构建。根据初步测量，所提出的解决方案比以前已知的基于矩阵决策树的方法更好地扩展，为GSPN的有效随机分析和优先模型的模型检查铺平了道路。
Prioritised Petri net is a powerful modelling language that often constitutes the core of even more expressive modelling languages such as GSPNs (Generalized Stochastic Petri nets). The saturation state space traversal algorithm has proved to be efficient for non-prioritised concurrent models. Previous works showed that priorities may be encoded into the transition relation, but doing so defeats the main idea of saturation by spoiling the locality of transitions. This paper presents an extension of saturation to natively handle priorities by considering the priority-related enabledness of transitions separately, adopting the idea of constrained saturation. To encode the highest priority of enabled transitions in every state we introduce edge-valued interval decision diagrams. We show that in case of Petri nets, this data structure can be constructed offline. According to preliminary measurements, the proposed solution scales better than previously known matrix decision diagram-based approaches, paving the way towards efficient stochastic analysis of GSPNs and the model checking of prioritised models.