In this short presentation we propose a formal framework based on a two-player game on Petri nets. We consider multi-agent systems in which a component, the controller, needs to guarantee a certain liveness property on the system behaviour, while keeping secret some of its actions to the other system components, and we discuss the basis for a uniform solution of this problem.
We propose a framework for the formal study of concurrent multi-agent systems, in which a component (the controller) needs to keep certain services active, and at the same time needs to keep secret some of its actions.
These two problems are often studied separately; a common way to check whether the
controller is able to guarantee a certain property consists in modelling the problem as a
twoplayer game, and verifying the existence of a winning strategy for the controller, namely a
selection of moves such that the property is always guaranteed in the system, regardless of
the behavior of the remaining part of the system. Typical goals for the controller consist in
avoiding a set of states [
To check whether a system satisfies some privacy requirements, several notions of
noninterference and opacity have been introduced [
Our goal is to put the basis for a unified analysis of these two problems. We define a
multiagent system as a 1-safe Petri net, where transitions are partitioned into controllable and
uncontrollable, and a subset of controllable transitions needs to remain secret. We define the
privacy requirement through the reveals relation [
This work builds on [8], where we define an algorithm to check the existence of a winning strategy when the goal of the controller is a LTL formula and the system is modelled as a 1-safe net, and on [9], where we propose an algorithm to verify the existence of reveals relations for a subclass of bounded P/T systems.
The main ideas of our approach are illustrated in the following, extremely simplified, example. Consider the Petri net in Fig. 1, where transitions in grey belong to the controller. Transition models the request of a service, which can be supplied in two distinct ways (either or ). The controller must guarantee that every request is sooner or later satisfied, so that the environment will reach place ; at the same time, the environment should not be able to deduce whether or was chosen. Suppose that the environment does not directly observe the grey transitions. If transition fires, then the environment can deduce that was chosen. Hence, a winning strategy for the controller consists in never firing .
In the following we assume the basic definitions of Petri net theory such as 1-safe net systems and their unfoldings ([10], [11]).
Let Σ = ( , , , ) be a 1-safe net system and unf(Σ) = ( , , , ) be its unfolding.
The set is partitioned into two disjoint subsets, , the set of controllable transitions, and , the set of uncontrollable transitions which belong to the environment.
In addition, T can be partitioned into high and low transitions, denoted ℎ and , respectively. We assume ℎ ⊆ , being ℎ the set of controllable transitions which must remain secret, i.e.: the set of transitions whose occurrence should not be deduced by the environment. By consequence, the events in the unfolding will be partitioned into , controllable, and , uncontrollable events, according to their labels; moreover, will contain the set ℎ of occurrence of secret transitions, the high events.
A run is a prefix = ( , , , ) of the unfolding of Σ , describing a particular history in which conflicts have been solved, i.e.: the underlying net ( , , ) is conflict-free. A cut in is a maximal set of pairwise concurrent elements of .
Let be a set of runs in unf(Σ) and 1, 2 ∈ ; we say 1 reveals 2 in , denoted 1 ◁ 2 , if each run in which contains an occurrence of 1 also contains at least one occurrence of 2.
Formally, 1 ◁ 2 if 1) ∀ ∈ 1 ∈ ( ) ⇒ 2 ∈ ( ), and 2) there is a run ∈ such that: 1 ∈ ( ).
We will say that the set of runs satisfies the non-interference property if and only if there is no pair of transitions ∈ , ℎ ∈ ℎ such that reveals ℎ in .
In this section we define a two-player asynchronous game.
Let Σ = ( , , , ) be a 1-safe net, the set of controllable transitions, = ∖ ; unf(Σ) = ( , , , ) its unfolding, with ⊂ the set of controllable events. A strategy is a function that returns a subset of controllable transitions, based on the current controller observation. In this work we assume that the controller can observe a subset of places in the system, and that has no memory, therefore its observations are subsets of markings.
The game we are defining is asynchronous, in the sense that players do not take turns; any player can decide to fire one of its transitions, when the transition is enabled, and we assume that the system is distributed in space. This implies that even if a place is observable by the controller, in general the controller cannot base its strategy on the information that the place is marked or unmarked, if a non controllable transition is enabled, and might change the marking of the place. Hence we introduce the concept of stable part of a marking. Let be a reachable marking. Its stable part is defined as the set of places in whose tokens cannot be consumed by any sequence of uncontrollable transitions enabled in . We assume that the controller can base his decisions only upon the observable and stable parts of markings. This is motivated by the fact that even if the value of a certain local state is not hidden to the controller, its information may arrive to the controller with a certain delay. By definition, if a place is not in the stable part of a marking, its value may change due to a transition that is out of the control of the controller, therefore the information about it may arrive outdated to the controller, that cannot count on it. If we denote with the set of reachable markings and with obs the function that for each marking associates its stable and observable part, we can formally define a strategy (abusing the notation) as : obs( ) → 2 .
We assume that the set of the environment transitions ⊆ has a progress constraint, that is, if a transition ∈ is constantly enabled, it will eventually fire. Let ⊆ be the set of events corresponding to the occurrence of transitions in . A play is a run of the unfolding, maximal with respect to , namely ′ obtained by extending with an ∈ cannot be a run.
A play is consistent with a strategy if (1) for each ∈ ∩ there is a cut such that ( ) = and ∈ (obs()), i.e. each controllable event was allowed by in the play; (2) no event belonging to the controller is finally postponed, namely there is no event ∈ enabled in but not present in , which is constantly selected by .
Given a play, to decide whether the controller wins it, we need to formally define its goal. As
stated in the introduction, we consider goals composed by two parts that need to be verified at
the same time. The first is the ability of the controller to eventually guarantee a certain service,
whenever it is required. Let req be the place denoting that the service has been requested and s
the place denoting the service. We express this part of the goal with an LTL formula, specifically
( → ), where and are, respectively, the globally and the eventually temporal
operators. In words, whenever a request is made, it will eventually be satisfied. The second is
the secrecy property, namely let ℎ ⊆ be the subset of high transitions and = ∖ ℎ the
subset of low transitions. The environment should not be able to discover the occurrence of a
high transition through the observation of low transitions. We model this property through
reveals, namely we require that there is no pair ℎ, , in the considered set of runs , such
that ◁ ℎ. In the literature [
1. could be the set of all the runs on the system maximal with respect to the set . This is the set of all the runs allowed by the game. This option works if the environment is not aware of the goal of the controller; if this is the case, it cannot restrict the behaviours of the system by computing a set of possible strategies, but has to consider that any possible run allowed in the game can occur. 2. is the set of all the runs on the system, maximal with respect to the set and where the LTL formula is satisfied. In this case we assume that the environment is aware of the ifrst goal of the controller, but it is still not able to compute a strategy that the controller could take. 3. is a set of runs such that for each ∈ there is a strategy such that is winning with respect to the LTL goal, and is a play consistent with . In this case we consider a partially rational environment, that is able to restrict the behaviours of the controller by knowing its goal and by computing which behaviours the controller could have in order to be sure to reach it. 4. is a set of runs such that for each ∈ there is a strategy as follows: • is winning for the LTL goal; • for each ∈ that can fire by following , there is no ℎ ∈ ℎ that fires by following such that ◁ ℎ in the runs allowed by .
This is the case in which the environment is not only able to compute a strategy for liveness, but also to compute which strategies should be avoided in order to let it deduce information about occurrences of high transitions.
When we pursue the last option, we only need to check whether is empty; if it is not, the controller has a winning strategy. In all the other cases we need to compute the reveals relation on the set .
We have described a framework, based on Petri nets, in which it is possible to combine two
types of problems, that we tackled in recent years: exploiting a kind of asynchronous game in
order to prove certain liveness properties, and studying a relation between events, useful in
formalizing non-interference in distributed systems. The next steps we plan to carry on relate to
the search for algorithms to decide whether a winning strategy for the controller exists. To this
aim, we plan to start from the algorithms that we developed for solving each of these problems
[9, 8], by adapting them to work in the combined case. This step is not trivial, since a strategy
tuned for one goal among liveness and non-interference may not satisfy the other. Longer term
goals include considering generalizations of the relation, using an relation [