2023/01/20 by Roberto Gorrieri, Gorrieri, Roberto
Computer Science · Business, Management and Accounting · Social Sciences · #Petri Nets in System Modeling #Business Process Modeling and Analysis #Access Control and Trust
paper · pdf · doi:10.48550/arxiv.2301.08570
Information flow security properties were defined some years ago (see, e.g., the surveys \citeFG01,Ry01) in terms of suitable equivalence checking problems. These definitions were provided by using sequential models of computations (e.g., labeled transition systems \citeGV15), and interleaving behavioral equivalences (e.g., bisimulation equivalence \citeMil89). More recently, the distributed model of Petri nets has been used to study non-interference in \citeBG03,BG09,BC15, but also in these papers an interleaving semantics was used. We argue that in order to capture all the relevant information flows, truly-concurrent behavioral equivalences must be used. In particular, we propose for Petri nets the distributed non-interference property, called DNI, based on \em branching place bisimilarity \citeGor23b, which is a sensible, decidable equivalence for finite Petri nets with silent moves. Then we focus our attention on the subclass of Petri nets called \em finite-state machines, which can be represented (up to isomorphism) by the simple process algebra CFM \citeGor17. DNI is very easily checkable on CFM processes, as it is compositional, so that it does does not suffer from the state-space explosion problem. Moreover, we show that DNI can be characterized syntactically on CFM by means of a type system.