Formal Verification of Petri Nets with Names
Formal Verification of Petri Nets with Names
复制标题
Petri 网名称的形式化验证
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Andrey Rivkin
中科院分区：
文献类型：
--
作者：
M. Montali;Andrey Rivkin
最近引入了具有名称创建和管理的Petri网，以便使Petri网能够对配备有通道、密码密钥或计算边界的（分布式）系统的动态进行建模。虽然传统的形式属性，如有界性，可覆盖性和可达性，已经深入研究了这一类的Petri网，形式验证丰富的时间属性还没有调查到目前为止。在本文中，我们攻击这个验证问题。我们引入复杂的一阶（MU）演算的变种，以指定丰富的属性，同时考虑系统的动态和其状态中存在的名称。然后，我们分析（联合国）的可判定性边界的验证，这样的逻辑，考虑不同的概念有界性。值得注意的是，我们的可判定性的结果是通过翻译到以数据为中心的动态系统，最近设计的正式规范和验证的业务流程工作在关系数据库的约束框架。在这种情况下，我们的研究结果有助于迄今为止尚未广泛相关的领域之间的交叉施肥。
Petri nets with name creation and management have been recently introduced so as to make Petri nets able to model the dynamics of (distributed) systems equipped with channels, cyphering keys, or computing boundaries. While traditional formal properties such as boundedness, coverability, and reachability, have been thoroughly studied for this class of Petri nets, formal verification against rich temporal properties has not been investigated so far. In this paper, we attack this verification problem. We introduce sophisticated variants of first-order (mu )-calculus to specify rich properties that simultaneously account for the system dynamics and the names present in its states. We then analyse the (un)decidability boundaries for the verification of such logics, by considering different notions of boundedness. Notably, our decidability results are obtained via a translation to data-centric dynamic systems, a recently devised framework for the formal specification and verification of business processes working over relational database with constraints. In this light, our results contribute to the cross-fertilization between areas that have not been extensively related so far.