A Finite Prefix for Analysing Information Flow Among Transitions of a Free-Choice Net

In distributed systems, the occurrence of an action can give information about the occurrence of other actions. This can be an unwanted situation when “high” actions of the system need to be kept secret, while allowing users to observe “low” actions. If it is possible to deduce information about occurrence of high actions by observing only low actions, then the system suffers from an unwanted information flow. “Reveals” and “excludes” relations were introduced for modelling and analysing such an information flow among actions of a distributed system that is modelled via Petri nets. In this paper, we provide a formal basis for computing reveals and excludes relations of 1-safe free-choice Petri nets. We introduce the “maximal-step computation tree” to represent the behaviour of a distributed system under maximal-step semantics. We define a finite prefix of the tree called “full prefix” and we show that it is adequate for analysing information flow by means of reveals and excludes relations.