  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.
