Model Checking Branching Properties on Petri Nets with Transits

被引：1

作者：

Finkbeiner, Bernd ^{[1
]}

Gieseking, Manuel ^{[2
]}

Hecking-Harbusch, Jesko ^{[1
]}

Olderog, Ernst-Rudiger ^{[2
]}

机构：

[1] CISPA Helmholtz Ctr Informat Secur, Saarbrucken, Germany

[2] Carl von Ossietzky Univ Oldenburg, Oldenburg, Germany

来源：

AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS (ATVA 2020) | 2020年 / 12302卷

基金：

欧洲研究理事会;

关键词：

AUTOMATA;

D O I：

10.1007/978-3-030-59152-6_22

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：394 / 410

页数：17

共 50 条

[1] Model checking Petri nets with MSVL
Shi, Ya
Tian, Cong
Duan, Zhenhua
Zhou, Mengchu
[J]. INFORMATION SCIENCES, 2016, 363 : 274 - 291
[2] MODEL CHECKING OF PERSISTENT PETRI NETS
BEST, E
ESPARZA, J
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 626 : 35 - 52
[3] Using Integer Time Steps for Checking Branching Time Properties of Time Petri Nets
Janowska, Agata
Penczek, Wojciech
Polrola, Agata
Zbrzezny, Andrzej
[J]. TRANSACTIONS ON PETRI NETS AND OTHER MODELS OF CONCURRENCY VIII, 2013, 8100 : 89 - 105
[4] ON SYMBOLIC MODEL CHECKING IN PETRI NETS
HIRAISHI, K
NAKANO, M
[J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (11) : 1479 - 1486
[5] Model Checking Reconfigurable Petri Nets with Maude
Padberg, Julia
Schulz, Alexander
[J]. GRAPH TRANSFORMATION, 2016, 9761 : 54 - 70
[6] TCTL Model Checking of Time Petri Nets
Boucheneb, Hanifa
Gardey, Guillaume
Roux, Olivier H.
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2009, 19 (06) : 1509 - 1540
[7] Petri nets, traces, and local model checking
Cheng, A
[J]. THEORETICAL COMPUTER SCIENCE, 1997, 183 (02) : 229 - 251
[8] LTL model checking for modular Petri nets
Latvala, T
Mäkelä, M
[J]. APPLICATIONS AND THEORY OF PETRI NETS 2004, PROCEEDINGS, 2004, 3099 : 298 - 311
[9] Petri Nets, traces, and local model checking
Cheng, A
[J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1995, 936 : 322 - 337
[10] Sequential and distributed model checking of Petri nets
Bell A.
Haverkort B.R.
[J]. International Journal on Software Tools for Technology Transfer, 2005, 7 (1) : 43 - 60

← 1 2 3 4 5 →