CISPA
Browse
cispa_all_3265.pdf (431.42 kB)

Model Checking Branching Properties on Petri Nets with Transits

Download (431.42 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Bernd FinkbeinerBernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog
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. %for the first time.

History

Preferred Citation

Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch and Ernst-Rüdiger Olderog. Model Checking Branching Properties on Petri Nets with Transits. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2020-10-19

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_3265, title = "Model Checking Branching Properties on Petri Nets with Transits", author = "Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-Rüdiger", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC