论文标题
模型检查带有Transits的Petri网上的分支特性（完整版）
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
论文作者
论文摘要
为了建模并发系统，很方便区分数据流和控件。在数据流的级别上指定了正确性，而系统是在控制级别上配置的。具有过渡和Flow-LTL的培养皿网是一种相应的形式主义。在Flow-LTL中，数据流的正确性和对控件的公平性和最大性的假设都在线性时间内表达。到目前为止，无法针对具有Transits的Petri网指定分支行为。在本文中，我们介绍Flow-CTL*，以表达数据流的预期分支行为，同时维持LTL以保持对控制的公平性和最大性假设。我们用策略更新编码物理访问控制，作为培养皿网，并提供流程-CTL*中的标准要求。对于模型检查，我们通过自动机构造对petr-ctl*的转运petri网的模型检查问题减少了对LTL Petri Nets的模型检查问题。因此，可以验证具有公平性假设下的策略更新的物理访问控制，可以验证无限数量的人。
To model check concurrent systems, it is convenient to distinguish between the data flow and the control. Correctness is specified on the level of data flow whereas the system is configured on the level of control. Petri nets with transits and Flow-LTL are a corresponding formalism. In Flow-LTL, both the correctness of the data flow and assumptions on fairness and maximality for the control are expressed in linear time. So far, branching behavior cannot be specified for Petri nets with transits. In this paper, we introduce Flow-CTL* to express the intended branching behavior of the data flow while maintaining LTL for fairness and maximality assumptions on the control. We encode physical access control with policy updates as Petri nets with transits and give standard requirements in Flow-CTL*. For model checking, we reduce the model checking problem of Petri nets with transits against Flow-CTL* via automata constructions to the model checking problem of Petri nets against LTL. Thereby, physical access control with policy updates under fairness assumptions for an unbounded number of people can be verified.
