arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 1409.8404cs.FLcs.LO
收藏

可重构Petri网到Maude的转换

Converting Reconfigurable Petri Nets to Maude

Alexander Schulz

摘要:

模型检验是理论计算机科学的一个重要研究方向。它可以验证具有一组属性(如活性,死锁或安全性)的模型。典型的建模技术之一是Petri网,它们被很好地理解并且可以用于模型检验。可重构Petri网是基于一组规则的Petri网。这些规则可以动态地用于改变网络。缺少的是验证可重构网络和死锁或活性等属性的可能性。本文介绍了一个转换可重构Petri网Maude,使我们能够填补空白。提出了一种基于Maude方程-重写逻辑和LTLR模型检验器的网变换方法。

英文摘要:

Model checking is an important aim of the theoretical computer science. It enables the verification of a model with a set of properties such as liveness, deadlock or safety. One of the typical modelling techniques are Petri nets they are well understood and can be used for a model checking. Reconfigurable Petri nets are based on a Petri nets with a set of rules. These rules can be used dynamically to change the net. Missing is the possibility to verify a reconfigurable net and properties such as deadlocks or liveness. This paper introduces a conversion from reconfigurable Petri net to Maude, that allows us to fill the gap. It presents a net transformation approach which is based on Maude's equation- and rewrite logic as well as the LTLR model checker.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑