# Distributed Non-Interference

Roberto Gorrieri
Università di Bologna, Dipartimento di Informatica — Scienza e Ingegneria
Mura A. Zamboni, 7, 40127 Bologna, Italy<EMAIL_ADDRESS>
###### Abstract

Information flow security properties were defined some years ago (see, e.g.,
the surveys [13, 36]) in terms of suitable equivalence checking problems.
These definitions were provided by using sequential models of computations
(e.g., labeled transition systems [18]), and interleaving behavioral
equivalences (e.g., bisimulation equivalence [32]). More recently, the
distributed model of Petri nets has been used to study non-interference in [6,
7, 2], 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 branching
place bisimilarity [26, 25], 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 finite-state machines, which can be represented
(up to isomorphism) by the simple process algebra CFM [19]. 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.

##  1 Introduction

Non-interference has been defined in the literature as an extensional property
based on some observational semantics: the high part (usually considered the
secret part) of a system does not interfere with the low part (i.e., the
public one) if whatever is done at the high level (i.e., by high-level users)
produces no visible effect on the low part of the system (i.e., it does not
change the observations made by low-level users); or, equivalently, if low-
users cannot infer the occurrence of those events that should be observable
only by high-users.

The original notion of non-interference in [17] was defined, using trace
semantics, for deterministic automata with outputs. Generalized notions of
non-interference were then designed for more general sequential models of
computation, such as (nondeterministic) labeled transition systems (LTSs, for
short), by exploiting also finer notions of observational semantics such as
bisimulation equivalence (see, e.g., [36, 12, 37, 13]). The security
properties studied in these papers are all based on the dynamics of systems,
as they are defined by means of one (or more) equivalence check(s). Therefore,
non-interference checking is as difficult as equivalence checking, a well-
studied hard problem in automata theory and concurrency theory (see, e.g.,
[30, 18]).

More recently, the distributed model of Petri nets [34, 35, 19] was used to
study non-interference in, e.g., [6, 7, 2], but also in these papers the
security properties of interest are based on interleaving (i.e., sequential)
behavioral semantics and the distributed model is used only to show that,
under some conditions, these (interleaving) information flows can be
characterized by the presence (or absence) of certain causal or conflict
structures in the net.

The thesis of this paper is that, for security analysis, it is necessary to
describe the behavior of distributed systems by means of a distributed model
of computation, such as a Petri net, but also to observe the distributed model
by means of some truly-concurrent behavioral semantics, i.e., a semantics that
can observe the parallelism of system components or, better, the causality
among the actions performed. There is a wide range of possible truly-
concurrent equivalences (see, e.g., [14, 16] for a partial overview) and it
may be not obvious to understand which is more suitable. Our intuition is
that, in order to capture all the possible information flows, it is necessary
that the observational semantics is very concrete, observing not only the
partial order of events that have occurred, as in fully-concurrent
bisimilarity [5], but also the structure of the distributed state, as in place
bisimilarity [1], a sensible behavioral equivalence, which was recently proved
decidable [24] for finite Petri nets.

The non-interference problem can be summarized as follows. Our aim is to
analyze systems that can perform two kinds of actions: high-level actions,
representing the interaction of the system with high-level users, and low-
level actions, representing the interaction with low-level users. We want to
verify whether the interplay between the high user and the high part of the
system can affect the view of the system as observed by a low user. We assume
that the low user knows the structure of the system, and we check whether, in
spite of this, (s)he is not able to infer the behavior of the high user by
observing the low view of the execution of the system. Hence, we assume that
the set of actions is partitioned into two subsets: the set $H$ of high-level
actions (or secret actions) and the set $L$ of low-level actions (or public
actions).

To explain our point of view, we use the process algebra CFM [19, 21],
extending finite-state CCS [32] with an operator of asynchronous (i.e.,
without communication capabilities) parallelism, that can be used at the top
level only. The net semantics of CFM [19, 21], described in Section 3.2,
associates a finite-state machine (a particular Petri net whose transitions
have singleton pre-set and singleton, or empty, post-set) $N_{p}$ to each CFM
process term $p$ and, conversely, for each finite-state machine $N$ we can
associate a CFM process term $p$ whose net semantics $N_{p}$ is isomorphic to
$N$; for this reason, we can work equivalently on CFM process terms or on
finite-state machines. Consider the CFM sequential process

$\begin{array}[]{rcllrcl}A&\doteq&l.A+h.B&&B&\doteq&l.B\end{array}$

where $A$ and $B$ are process constants, each one equipped with a defining
equation, and where $l$ is a low action and $h$ is a high one. The LTS
semantics for $A$ is outlined in Figure 1(a).

$a)\qquad$$A$$B$$h$$l$$l$$b)\;\;$$A\setminus h$$B\setminus
h$$l$$l$$c)\;\;$$C\mbox{$\,|\,$}B$$B\mbox{$\,|\,$}B$$h$$l$$l$ Figure 1: An
example of a secure process with never-ending behavior

Intuitively, this system is secure because the execution of the high-level
action $h$ does not add any information to a low-level observer: what such a
low observer can see is just a, possibly never-ending, sequence of low actions
$l$ in any case: before $h$ is performed as well as after $h$ has been
performed. The most restrictive non-interference property discussed in [12,
13, 7], called SBNDC (acronym of Strong Bisimulation Non-Deducibility on
Composition), requires that whenever the system under scrutiny performs a
high-level action, the states of the system before and after executing that
high-level action are indistinguishable for a low-level observer. In our
example, this means that $A$ is SBNDC if $A\setminus h$ is bisimilar to
$B\setminus h$, where $A\setminus h$ denotes the low observable part of the
system before $h$ is performed (i.e., process $A$ where the transition $h$ is
pruned), while $B\setminus h$ denotes the low observable part of the system
after $h$ is performed. By observing the LTSs in Figure 1(b), we conclude that
$A$ is SBNDC.

However, the LTS in Figure 1(a) is isomorphic to the LTS in 1(c), which is the
semantics of the parallel process $C\mbox{$\,|\,$}B$, where $C\doteq h.B$ and
$B\doteq l.B$. Therefore, we can conclude that also $C\mbox{$\,|\,$}B$ enjoys
the SBNDC non-interference property. Unfortunately, this parallel system is
not secure: if a low observer can realize that two occurrences of actions $l$
have been performed in parallel (which is a possible behavior of
$B\mbox{$\,|\,$}B$ only, but this behavior is not represented in the
interleaving LTS semantics), then (s)he is sure that the high-level action $h$
has been performed. This trivial example shows that SBNDC, based on
interleaving bisimulation equivalence, is unable to detect a real information
flow from high to low.

However, if we use a Petri net semantics for the process algebra CFM, as
described in Section 3.2, we have that the net semantics for
$C\mbox{$\,|\,$}B$, outlined in Figure 2(a), is such that the low-observable
system before the execution of $h$, i.e., $(C\mbox{$\,|\,$}B)\setminus h$
(whose net semantics is outlined in Figure 2(b)) is not “truly-concurrent”
equivalent to the low-observable system after $h$, i.e.,
$(B\mbox{$\,|\,$}B)\setminus h$ (whose net semantics is in Figure 2(c)). In
fact, it is now visible that the two tokens on place $B\setminus h$ in the net
in (c) can perform transition $l$ at the same time, and such a behavior is
impossible for the net in (b). This example calls for a truly-concurrent
semantics which is at least as discriminating as step bisimulation equivalence
[33, 19], which is able to observe the parallel execution of actions.

$a)\qquad$$C$$h\;$$B\;$$l\;$$b)\;\;$$C\setminus h$$B\setminus
h$$l\;$$c)\;\;$$B\setminus h$$\;l$ Figure 2: The Petri net for the process
$C\mbox{$\,|\,$}B$ in (a), of $(C\mbox{$\,|\,$}B)\setminus h$ in (b) and of
$(B\mbox{$\,|\,$}B)\setminus h$ in (c) $a)\qquad\quad$$A$$h$$a$$b$$a.\mbox{\bf
0}$$b.\mbox{\bf 0}$$a$$b$$b)\;\;$$A\setminus h$$a$$b$$b.\mbox{\bf 0}\setminus
h$$a.\mbox{\bf 0}\setminus h$$b$$a$$c)\;\;$$a.\mbox{\bf 0}\setminus
h$$b.\mbox{\bf 0}\setminus h$$a$$b$ Figure 3: An example of an insecure
process $a)\qquad\quad$$l.h.C$$l\;$$h.C$$h\;$$C$$b)\;\;$$l.h.\mbox{\bf
0}$$l$$h.\mbox{\bf 0}$$h$$c)\;\;$$h.l.\mbox{\bf 0}+l.C$$h$$l$$l.\mbox{\bf
0}$$C$$l$ Figure 4: By observing the state, further information flows can be
detectable

As a further example, consider the process term (not expressible in CFM,
rather in the slightly richer process algebra BPP [9, 18, 23]):

$\begin{array}[]{rcllrcl}A&\doteq&h.(a.\mbox{\bf 0}|b.\mbox{\bf
0})+a.b.\mbox{\bf 0}+b.a.\mbox{\bf 0}\end{array}$

where $a,b$ are low-level actions, whose net semantics is outlined in Figure
3(a). The two low-observable subnets before and after the execution of $h$
(depicted in Figure 3(b) and 3(c), respectively) generate different partial
orders: if an observer realizes that $a$ and $b$ are causally independent,
then (s)he infers that $h$ has been performed. Therefore, the observation of
causality is crucial for detecting potential information flows in a
distributed system; hence, our observational semantics should be at least as
discriminating as fully-concurrent bisimilarity [5] (or, equivalently,
history-preserving bisimilarity [38, 14, 10]), that is able to observe the
partial orders of performed events.

However, we want to argue that also the structure of the distributed system
(i.e, the size of the current marking, in Petri net terminology) is an
important feature, that cannot be ignored, as most truly-concurrent behavioral
equivalences do (notably fully-concurrent bisimilarity [5]). Consider the net
in Figure 4(a), which is the semantics of the CFM process $l.h.C$, with
$C\doteq\mbox{\bf 0}$. Since $h$ is not causing any low action, we conclude
that this net is secure. However, the very similar net in (b), which is the
semantics of $l.h.\mbox{\bf 0}$, is not secure: if the low observer realizes
that the token disappears in the end, then (s)he can infer that $h$ has been
performed. This simple observation is about the observability of the size of
the distributed system: if the execution of a high-level action modifies the
current number of tokens (i.e., the number of currently active sequential
subprocesses), then its execution has an observable effect that can be
recognized by a low observer. Indeed, also in the net in Figure 3 the
execution of the high-level transitions $h$ modifies the current number of
active components, because the marking before executing $h$ has size $1$,
while the marking after $h$ has size $2$, so that a low observer can realize
that $h$ has been performed. Similarly, the net in Figure 4(c), which is the
semantics of $h.l.\mbox{\bf 0}+l.C$ with $C\doteq\mbox{\bf 0}$, is such that,
before and after $h$, the same partial order of events can be performed, but
if the token disappears in the end, then the low observer knows that $h$ has
been performed. Therefore, it is necessary to use a truly-concurrent
behavioral equivalence slightly finer than fully-concurrent bisimilarity,
which is resource-sensitive, i.e., able to observe also the resources of the
distributed state (i.e., the number of sequential processes composing the
distributed system). Resource-sensitive truly-concurrent behavioral
equivalences include, e.g., place bisimilarity [1, 24] and structure-
preserving bisimilarity [16]. These equivalences coincide on CFM (i.e., on
finite-state machines) and, on this class of nets, they can be equivalently
characterized in a very simple and effective way as team bisimilarity [20,
23]. However, on finite Petri nets place bisimilarity is strictly finer than
structure-preserving bisimilarity, but the former is decidable [24], while
this is an open problem for the latter. (By the way, fully-concurrent
bisimilarity is undecidable for finite Petri nets [11].) So, our starting
point is to consider place bisimilarity as our candidate observational
semantics over finite Petri nets.

When considering Petri nets with silent transitions (i.e., transitions labeled
by the invisible action $\tau$), we have the problem to understand which kind
of generalization of place bisimulation equivalence to consider. We have at
least two possible alternatives, inspired to weak bisimilarity [32] or to
branching bisimilarity [15], originally proposed for LTSs [18]. In order to
understand the problem, consider the CFM process constants

$\begin{array}[]{rcllrcl}C&\doteq&h.(a.D+a.b.\mbox{\bf
0})+a.D&&D&\doteq&\tau.b.\mbox{\bf 0}+c.\mbox{\bf 0}\end{array}$

where $a,b,c$ are low-level actions and $h$ is a high-level action, whose net
semantics is outlined in Figure 5(a). Of course, the low-observable system
before executing $h$ is $p=C\setminus h$, whose net is outlined in Figure
5(b), while the low-observable system after $h$ is $q=(a.D+a.b.\mbox{\bf
0})\setminus h$, depicted in Figure 5(c).

$a)\qquad\quad$$C$$h$$a$$a.D+a.b.\mbox{\bf 0}$$a$$a$$D$$c$$\tau$$b.\mbox{\bf
0}$$b$$b)\;\;$$p=C\setminus h$$a$$D\setminus h$$c$$\tau$$b.\mbox{\bf
0}\setminus h$$b$$c)\;\;$$q=(a.D+a.b.\mbox{\bf 0})\setminus
h$$a$$a$$D\setminus h$$c$$\tau$$b.\mbox{\bf 0}\setminus h$$b$ Figure 5: By
observing the timing of choice, further information flows can be detected

According to weak bisimilarity, $p$ and $q$ are equivalent; in particular, to
the transition $q{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}b.\mbox{\bf 0}\setminus h$, process $p$ can reply
with the sequence $p{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}D\setminus
h{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}b.\mbox{\bf
0}\setminus h$. Therefore, if we use weak bisimilarity, then the system would
be considered secure. However, note that, by replying to the transition
$q{\mbox{${\>\stackrel{{\scriptstyle a}}{{\longrightarrow}}\>}$}}b.\mbox{\bf
0}\setminus h$, the process $p$ passes through state $D\setminus h$, that is
capable of performing $c$, a behavior that is impossible for $b.\mbox{\bf
0}\setminus h$. Hence, if a low user realizes that, after performing the low
action $a$, the low action $c$ is never available (i.e., it is able to realize
that the user is executing the computation due to summand $a.b.\mbox{\bf 0}$
as in $q{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}b.\mbox{\bf 0}\setminus h$), then (s)he is sure
that $h$ has been performed; hence, $C$ cannot be considered as secure.

As a matter of fact, branching bisimilarity, which is strictly finer than weak
bisimilarity, does not consider $p$ and $q$ as equivalent, as only $q$ has the
possibility of discarding $c$ immediately by performing $a$. In fact, this
crucial property is enjoyed by branching bisimilarity (but not by weak
bisimilarity): when in the branching bisimulation game a transition
$q_{1}{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}q_{1}^{\prime}$
is matched by a computation, say,
$q_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}q_{2}^{\prime}{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}q_{2}^{\prime\prime}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}q_{2}^{\prime\prime\prime}$,
all the states traversed by the silent computation from $q_{2}$ to
$q_{2}^{\prime}$ are branching bisimilar, so that they all belong to the same
equivalence class; and, similarly, all the states traversed by the silent
computation from $q_{2}^{\prime\prime}$ to $q_{2}^{\prime\prime\prime}$ are
branching bisimilar (in the example above, the states $D\setminus h$ and
$b.\mbox{\bf 0}\setminus h$ are not equivalent, as only the former can perform
$c$). This ensures that branching bisimilarity does fully respect the timing
of choices.

Indeed, this example reinforces the observation that the timing of choices is
a crucial aspect for security, as already observed on LTSs in [12, 13] where
it is argued that it is better to use branching-time behavioral equivalences
(such as bisimulation equivalence [32]) rather than linear-time behavioral
equivalences (such as trace equivalence).

Summarizing, the behavioral equivalence that we advocate is branching place
bisimilarity [26, 25], a sensible behavioral equivalence, which is decidable
in exponential time on finite Petri nets and that specializes to the very
efficiently decidable branching team equivalence on finite-state machines
[21].

So, we are now ready to propose the property DNI (acronym of Distributed Non-
Interference) as follows. Given a finite Petri net $N$, we denote by
$N\setminus H$ the net obtained from $N$ by pruning all the high-labeled
transitions and by denoting each place $s$ of $N$ by $s\setminus H$, as we did
in the previous examples.

> The initial marking $m_{0}$ of $N$ is DNI if for each reachable markings
> $m_{1},m_{2}$ and for each $h\in H$ such that
> $m_{1}{\mbox{${\>\stackrel{{\scriptstyle h}}{{\longrightarrow}}\>}$}}m_{2}$,
> we have that $m_{1}\setminus H\approx_{p}m_{2}\setminus H$, where
> $\approx_{p}$ denotes branching place bisimilarity and, for $i=1,2$,
> $m_{i}\setminus H$ denotes the marking of the net $N\setminus H$
> corresponding to $m_{i}$ in $N$.

On the one hand, DNI is clearly decidable in exponential time for bounded nets
(i.e., nets with a finite number of reachable markings), because we have to
make a finite number of branching place bisimulation checks, each one
decidable in exponential time [25]. On the other hand, it is an open problem
to see whether DNI is decidable for general unbounded Petri nets.

After this general introduction, in the rest of the paper, we focus our
attention only on the special class of Petri nets called finite-state
machines, on the corresponding process algebra CFM that truly represents such
nets, up to isomorphism [19], and on branching team equivalence [21], which is
the specialization of branching place bisimilarity on such nets. Hence, the
definition of DNI above can be specialized for this subcase in the obvious
way.

On the class of finite-state machines, which are bounded, DNI is very easily
checkable. As a matter of fact, given a CFM parallel process
$p=p_{1}\mbox{$\,|\,$}p_{2}\mbox{$\,|\,$}\ldots\mbox{$\,|\,$}p_{n}$, we prove
that $p$ is DNI if and only if each $p_{i}$ is DNI, for $i=1,\ldots,n$. Hence,
instead of inspecting the state space of $p$, we can simply inspect the state
spaces for $p_{1}$, $p_{2}$, …$p_{n}$. If the state space of each $p_{i}$ is
composed of 10 states, then the state space of $p$ is composed of $10^{n}$
states, so that a direct check of DNI on the state space of $p$ is impossible
for large values of $n$. However, the distributed analysis on each $p_{i}$ can
be done in linear time w.r.t. $n$, hence also for very large values of $n$, so
that the state-space explosion problem can be kept under control.

Moreover, a structural characterization of DNI can be provided by inspecting
directly the finite-state machine under scrutiny, which offers a very
efficient, polynomial algorithm to check DNI.

Finally, a slight enhancement of DNI (called DNI as well, with abuse of
notation), based on the slightly finer rooted branching team equivalence [21]
(which is the coarsest congruence for all the operators of CFM contained in
branching team equivalence), is characterized syntactically on CFM by means of
a typing system: we prove that a CFM process $p$ is DNI if and only if $p$ (or
a slight variant of it) is typed. The typing system is based on a finite,
sound and complete, axiomatization of rooted branching team equivalence [21].

The paper is organized as follows. Section 2 introduces the basic definitions
about finite-state machines, together with the definition of (rooted)
branching team equivalence. Section 3 defines the syntax of the process
algebra CFM, hints its net semantics and recalls the finite axiomatization of
rooted branching team equivalence from [21]. Section 4 introduces the
distributed non-interference property DNI on CFM processes, proving that it
can be really checked in a distributed manner, and also describes the typing
system for (the slightly finer variant of) DNI (based on the rooted variant of
branching team bisimulation). Finally, Section 5 comments on related work.

##  2 Finite-State Machines and Branching Team Equivalence

By finite-state machine (FSM, for short) we mean a simple type of finite Petri
net [34, 35, 19] whose transitions have singleton pre-set and singleton, or
empty, post-set. The name originates from the fact that an unmarked net of
this kind is essentially isomorphic to a nondeterministic finite automaton
[30] (NFA, for short), usually called a finite-state machine as well. However,
semantically, our FSMs are richer than NFAs because, as their initial marking
may be not a singleton, these nets can also exhibit concurrent behavior, while
NFAs are strictly sequential.

###### Definition 1

(Multiset) Let ${\mathbb{N}}$ be the set of natural numbers. Given a finite
set $S$, a multiset over $S$ is a function $m:S\rightarrow{\mathbb{N}}$. Its
support set $dom(m)$ is $\\{s\in S\;\big{|}\;m(s)\neq 0\\}$. The set of all
multisets over $S$ is ${\mathcal{M}}(S)$, ranged over by $m$. We write $s\in
m$ if $m(s)>0$. The multiplicity of $s$ in $m$ is the number $m(s)$. The size
of $m$, denoted by $|m|$, is $\sum_{s\in S}m(s)$, i.e., the total number of
its elements. A multiset $m$ such that $dom(m)=\emptyset$ is called empty and
is denoted by $\theta$. We write $m\subseteq m^{\prime}$ if $m(s)\leq
m^{\prime}(s)$ for all $s\in S$. Multiset union $\\_\oplus\\_$ is defined as
follows: $(m\oplus m^{\prime})(s)$ $=m(s)+m^{\prime}(s)$. Multiset difference
$\\_\ominus\\_$ is defined as follows: $(m_{1}\ominus
m_{2})(s)=max\\{m_{1}(s)-m_{2}(s),0\\}$. The scalar product of a number $j$
with $m$ is the multiset $j\cdot m$ defined as $(j\cdot m)(s)=j\cdot(m(s))$.
By $s_{i}$ we also denote the multiset with $s_{i}$ as its only element.
Hence, a multiset $m$ over $S=\\{s_{1},\ldots,s_{n}\\}$ can be represented as
$k_{1}\cdot s_{1}\oplus k_{2}\cdot s_{2}\oplus\ldots\oplus k_{n}\cdot s_{n}$,
where $k_{j}=m(s_{j})\geq 0$ for $j=1,\ldots,n$.  $\Box$

###### Definition 2

(Finite-state machine) A labeled finite-state machine (FSM, for short) is a
tuple $N=(S,A,T)$, where

  * $\bullet$

$S$ is the finite set of places, ranged over by $s$ (possibly indexed),

  * $\bullet$

$A$ is the finite set of labels, ranged over by $\ell$ (possibly indexed),
which contains the silent label $\tau$, and

  * $\bullet$

$T\subseteq S\times A\times(S\cup\\{\theta\\})$ is the finite set of
transitions, ranged over by $t$.

Given a transition $t=(s,\ell,m)$, we use the notation ${}^{\bullet}t$ to
denote its pre-set $s$ (which is a single place), i.e., one token on place $s$
to be consumed; $l(t)$ for its label $\ell$, and $t^{\bullet}$ to denote its
post-set $m$ (which is a place or the empty multiset $\theta$), i.e., the
token, if any, to be produced. Hence, transition $t$ can be also represented
as ${}^{\bullet}t$${\>\stackrel{{\scriptstyle
l(t)}}{{\longrightarrow}}\>}$$t^{\bullet}$.  $\Box$

Graphically, a place is represented by a circle, a transition by a box,
connected by a directed arc from the place in its pre-set and to the place in
its post-set, if any.

###### Definition 3

(Marking, FSM net system) A multiset over $S$ is called a marking. Given a
marking $m$ and a place $s$, we say that the place $s$ contains $m(s)$ tokens,
graphically represented by $m(s)$ bullets inside place $s$. An FSM net system
$N(m_{0})$ is a tuple $(S,A,T,$ $m_{0})$, where $(S,A,T)$ is an FSM and
$m_{0}$ is a marking over $S$, called the initial marking. We also say that
$N(m_{0})$ is a marked net. An FSM net system $N(m_{0})=(S,A,T,$ $m_{0})$ is
sequential if $m_{0}$ is a singleton, i.e., $|m_{0}|=1$; while it is
concurrent if $m_{0}$ is arbitrary.  $\Box$

###### Definition 4

(Firing sequence, reachable markings) Given an FSM $N=(S,A,T)$, a transition
$t$ is enabled at marking $m$, denoted by $m[t\rangle$, if
$\mbox{${}^{\bullet}t$}\subseteq m$. The execution (or firing) of $t$ enabled
at $m$ produces the marking
$m^{\prime}=(m\ominus\mbox{${}^{\bullet}t$})\oplus\mbox{$t^{\bullet}$}$. This
is written usually as $m[t\rangle m^{\prime}$, but also as
$m{\mbox{${\>\stackrel{{\scriptstyle
l(t)}}{{\longrightarrow}}\>}$}}m^{\prime}$. A firing sequence starting at $m$
is defined inductively as

  * $\bullet$

$m[\epsilon\rangle m$ is a firing sequence (where $\epsilon$ denotes an empty
sequence of transitions) and

  * $\bullet$

if $m[\sigma\rangle m^{\prime}$ is a firing sequence and $m^{\prime}[t\rangle
m^{\prime\prime}$, then $m[\sigma t\rangle m^{\prime\prime}$ is a firing
sequence.

If $\sigma=t_{1}\ldots t_{n}$ (for $n\geq 0$) and $m[\sigma\rangle m^{\prime}$
is a firing sequence, then there exist $m_{1},\ldots,m_{n+1}$ such that
$m=m_{1}[t_{1}\rangle m_{2}[t_{2}\rangle\ldots m_{n}[t_{n}\rangle
m_{n+1}=m^{\prime}$, and $\sigma=t_{1}\ldots t_{n}$ is called a transition
sequence starting at $m$ and ending at $m^{\prime}$. The set of reachable
markings from $m$ is
$reach(m)=\\{m^{\prime}\;\big{|}\;\exists\sigma.m[\sigma\rangle
m^{\prime}\\}$.  $\Box$

$s_{1}$$a\;$$\;c$$s_{2}\;$$b\;$$a)\qquad\qquad$$s_{3}$$s_{4}$$a\;$$\;b$$s_{5}$$b)\quad$
Figure 6: A sequential finite-state machine in (a), and a concurrent finite-
state machine in (b)

###### Example 1

By using the usual drawing convention for Petri nets, Figure 6 shows in (a) a
sequential FSM, which performs a sequence of $a$’s and $b$’s, until it
performs one $c$ and then stops successfully (the token disappears in the
end). A sequential FSM is such that any reachable marking is a singleton or
empty. Hence, a sequential FSM is safe (or $1$-bounded): each place in any
reachable marking can hold one token at most. In (b), a concurrent FSM is
depicted: it can perform $a$ forever, interleaved with two occurrences of $b$,
only: the two tokens in $s_{4}$ will eventually reach $s_{5}$, which is a
place representing unsuccessful termination (deadlock). A concurrent FSM is
$k$-bounded, where $k$ is the size of the initial marking: each place in any
reachable marking can hold $k$ tokens at most. Hence, the set $reach(m)$ is
finite for any $m$. As a final comment, note that for each FSM $N=(S,A,T)$ and
each place $s\in S$, the set $reach(s)$ is a subset of $S\cup\\{\theta\\}$.
$\Box$

###  2.1 Branching Bisimulation on Places

In order to adapt the definition of branching bisimulation on LTSs [15] for
unmarked FSMs, we need some auxiliary notation. We define relation
${\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}\subseteq
S\times(S\cup\\{\theta\\})$ as the reflexive and transitive closure of the
silent transition relation; formally, $\forall s\in S$,
$s{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}s$,
denoting that each place can silently reach itself with zero steps; moreover,
if
$s{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}s^{\prime}$
and
$s^{\prime}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}m$,
then
$s{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}m$,
where $m$ can be either the empty marking $\theta$ or a single place because
of the shape of FSMs transitions.

###### Definition 5

(Branching bisimulation on places) Let $N=(S,A,T)$ be an FSM. A branching
bisimulation is a relation $R\subseteq S\times S$ such that if
$(s_{1},s_{2})\in R$ then for all $\ell\in A$

  * $\bullet$

$\forall m_{1}$ such that
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$,

    * –

either $\ell=\tau$ and $\exists m_{2}$ such that
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}m_{2}$
with $(s_{1},m_{2})\in R$ and $(m_{1},m_{2})\in R$,

    * –

or $\exists s,m_{2}$ such that
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}s{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$
with $(s_{1},s)\in R$ and either $m_{1}=\theta=m_{2}$ or $(m_{1},m_{2})\in R$,

  * $\bullet$

and, symmetrically, $\forall m_{2}$ such that
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$.

Two places $s$ and $s^{\prime}$ are branching bisimilar (or branching
bisimulation equivalent), denoted by $s\approx s^{\prime}$, if there exists a
branching bisimulation $R$ such that $(s,s^{\prime})\in R$.  $\Box$

It is an easy exercise to check [21] that $(i)$ the identity relation
${\mathcal{I}}=\\{(s,s)\;\big{|}\;s\in S\\}$ is a branching bisimulation;
$(ii)$ the inverse relation
$R^{-1}=\\{(s^{\prime},s)\;\big{|}\;(s,s^{\prime})\in R\\}$ of a branching
bisimulation $R$ is a branching bisimulation; $(iii)$ the relational
composition $R_{1}\circ R_{2}=\\{(s,s^{\prime\prime})\;\big{|}\;\exists
s^{\prime}.(s,s^{\prime})\in R_{1}\wedge(s^{\prime},s^{\prime\prime})\in
R_{2}\\}$ of two branching bisimulations $R_{1}$ and $R_{2}$ is a branching
bisimulation; $(iv)$ the union $\bigcup_{i\in I}R_{i}$ of branching
bisimulations $R_{i}$ is a branching bisimulation. From these observations, it
follows that $\approx$ is an equivalence relation.

Remember that $s\approx s^{\prime}$ if there exists a branching bisimulation
containing the pair $(s,s^{\prime})$. This means that $\approx$ is the union
of all branching bisimulations, i.e.,

$\approx\;=\bigcup\\{R\subseteq S\times S\;\big{|}\;R\;\mbox{ is a branching
bisimulation}\\}.$

Hence, as the union of branching bisimulations is a branching bisimulation,
$\approx$ is also a branching bisimulation, hence the largest such relation.

###### Remark 1

(Stuttering Property) It is not difficult to prove that, given a
$\tau$-labeled path
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}s_{2}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}\ldots
s_{n}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}s_{n+1}$,
if $s_{1}\approx s_{n+1}$, then $s_{i}\approx s_{j}$ for all $i,j=1,\ldots
n+1$. This is sometimes called the stuttering property [15, 18].

This property justifies the following observation on the nature of branching
bisimilarity. As $\approx$ is a branching bisimulation, it satisfies the
conditions in Definition 5. Let us consider two branching bisimilar places
$s_{1}\approx s_{2}$. Then, suppose
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}m_{1}$
and that $s_{2}$ responds by performing
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}m_{2}$
with $s_{1}\approx m_{2}$ and $m_{1}\approx m_{2}$. By transitivity of
$\approx$, we have that also $s_{2}\approx m_{2}$. Hence, by the stuttering
property, $s_{1}$ is branching bisimilar to each place in the path from
$s_{2}$ to $m_{2}$, and so all the places traversed in the path from $s_{2}$
to $m_{2}$ are branching bisimilar. Similarly, assume
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$
(with $\ell$ that can be $\tau$) and that $s_{2}$ responds by performing
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}m{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$
with $s_{1}\approx m$ and $m_{1}\approx m_{2}$. By transitivity, $s_{2}\approx
m$, hence, by the stuttering property, $s_{1}$ is branching bisimilar to each
place in the path from $s_{2}$ to $m$. These constraints are not required by
weak bisimilarity [32, 21]: given $s_{1}$ weak bisimilar to $s_{2}$, when
matching a transition
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$
with
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}s_{2}^{\prime}{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}m_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}m_{2}^{\prime}$,
weak bisimilarity only requires that $m_{1}$ and $m_{2}^{\prime}$ are weak
bisimilar, but does not impose any condition on the intermediate states; in
particular, it is not required that $s_{1}$ is weak bisimilar to
$s_{2}^{\prime}$, or that $m_{1}$ is weak bisimilar to $m_{2}$.  $\Box$

Now we provide a couple of examples showing that branching bisimulation
equivalence is sensitive to the timing of choice and to the kind of
termination (i.e., to the size of the reachable marking).

###### Example 2

Consider Figure 7. It is not difficult to realize that $s_{1}\not\approx
s_{3}$. In fact, $s_{1}$ may reach $s_{2}$ by performing $a$; $s_{3}$ can
reply to this move in two different ways by reaching either $s_{4}$ or
$s_{5}$; however, while $s_{2}$ offers both $b$ and $c$, $s_{4}$ may perform
only $b$ and $s_{5}$ only $c$; hence, $s_{4}$ and $s_{5}$ are not branching
bisimilar to $s_{2}$ and so also $s_{1}$ is not branching bisimilar to
$s_{3}$. Moreover, also $s_{6}$ and $s_{8}$ are not branching bisimilar. In
fact, $s_{6}$ can reach $s_{7}$ by performing $a$, while $s_{8}$ can reply by
reaching the empty marking, but $\theta\not\approx s_{7}$. This example shows
that branching bisimilarity is sensitive to the kind of termination of a
process: even if $s_{7}$ is stuck, it is not equivalent to $\theta$ because
the latter is the marking of a properly terminated process, while $s_{7}$
denotes a deadlock situation.  $\Box$

$a)\qquad\qquad$$s_{1}$$a\;$$s_{2}\;$$b\;$$\;c$$b)\;\;$$s_{3}$$a\;$$\;a$$s_{4}\;$$b\;$$\;s_{5}$$\;c$$c)\;\;$$s_{6}$$\;a$$s_{7}$$s_{8}$$\;a$
Figure 7: Some non-branching bisimilar FSMs
$a)\quad$$s_{1}$$\tau\;$$\;b$$s_{2}\;$$a\;$$s_{3}\;$$b)\;\;$$s_{4}$$a\;$$\;b$$\;\tau$$\;s_{6}$$\;a$$s_{5}\;$$\;s_{7}$
Figure 8: Two non-branching bisimilar FSMs

###### Example 3

Consider the nets in Figure 8. It is not difficult to see that $s_{1}$ and
$s_{4}$ are weakly bisimilar [32, 21]. However, $s_{1}\not\approx s_{4}$,
because to transition $s_{4}{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}s_{5}$, place $s_{1}$ can only try to respond with
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\>}$}}s_{2}{\mbox{${\>\stackrel{{\scriptstyle
a}}{{\longrightarrow}}\>}$}}s_{3}$, but not all the conditions required are
satisfied; in particular, $s_{2}\not\approx s_{4}$, because only $s_{4}$ can
do $b$. In fact, note that $s_{1}\not\approx s_{2}$. Indeed, branching
bisimulation equivalence ensures that, in response to the move
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$,
$s_{2}$ replies with
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\epsilon}}{{\Longrightarrow}}\>}$}}s{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$,
in such a way that all the places traversed in the silent path from $s_{2}$ to
$s$ are branching bisimilar.  $\Box$

###### Remark 2

(Complexity) If $m$ is the number of net transitions and $n$ of places,
checking whether two places of an FSM are branching bisimilar can be done in
$O(m\mbox{ log }n)$ time, by adapting the algorithm in [31] for branching
bisimulation on LTSs.  $\Box$

As branching bisimilarity is not a congruence for the CFM choice operator, we
need a slightly more concrete equivalence relation, which can be proved to be
the coarsest congruence, contained in $\approx$, for all the CFM operators.

###### Definition 6

(Rooted branching bisimulation on places) Let $N=(S,A,T)$ be an FSM. Two
places $s_{1}$ and $s_{2}$ are rooted branching bisimilar, denoted
$s_{1}\approx_{c}s_{2}$, if $\forall\ell\in A$

  * $\bullet$

for all $m_{1}$ such that
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$,
there exists $m_{2}$ such that
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$
and either $m_{1}=\theta=m_{2}$ or $m_{1}\approx m_{2}$,

  * $\bullet$

for all $m_{2}$ such that
$s_{2}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{2}$,
there exists $m_{1}$ such that
$s_{1}{\mbox{${\>\stackrel{{\scriptstyle\ell}}{{\longrightarrow}}\>}$}}m_{1}$
and either $m_{1}=\theta=m_{2}$ or $m_{1}\approx m_{2}$.

$\Box$

The peculiar feature of $\approx_{c}$ is that initial moves are matched as in
strong bisimulation [32], while subsequent moves are matched as for branching
bisimilarity. Therefore, rooted branching bisimilarity is a slightly finer
variant of branching bisimilarity.

###### Proposition 1

[21] For each FSM $N=(S,A,T)$ with silent moves, relations $\approx$ and
$\approx_{c}$ are equivalence relations.  $\Box$

###  2.2 (Rooted) Branching Team Equivalence

###### Definition 7

(Additive closure) Given an FSM net $N=(S,A,T)$ and a place relation
$R\subseteq S\times S$, we define a marking relation
$R^{\oplus}\,\subseteq\,{\mathcal{M}}(S)\times{\mathcal{M}}(S)$, called the
additive closure of $R$, as the least relation induced by the following axiom
and rule.

$\begin{array}[]{lllllllllll}\begin{array}[]{c}\\\ \hline\cr(\theta,\theta)\in
R^{\oplus}\end{array}&&\;\;\;\begin{array}[]{c}(s_{1},s_{2})\in
R\;\;\;(m_{1},m_{2})\in R^{\oplus}\\\ \hline\cr(s_{1}\oplus m_{1},s_{2}\oplus
m_{2})\in R^{\oplus}\end{array}\\\ \end{array}$
$\Box$

Note that, by definition, two markings are related by $R^{\oplus}$ only if
they have the same size. An alternative way to define that two markings
$m_{1}$ and $m_{2}$ are related by $R^{\oplus}$ is to state that $m_{1}$ can
be represented as $s_{1}\oplus s_{2}\oplus\ldots\oplus s_{k}$, $m_{2}$ can be
represented as $s_{1}^{\prime}\oplus s_{2}^{\prime}\oplus\ldots\oplus
s_{k}^{\prime}$ and $(s_{i},s_{i}^{\prime})\in R$ for $i=1,\ldots,k$.

###### Remark 3

(Additivity and subtractivity) The additive closure $R^{\oplus}$ of a place
relation $R$ is additive: if $(m_{1},m_{2})\in R^{\oplus}$ and
$(m_{1}^{\prime},m_{2}^{\prime})\in R^{\oplus}$, then $(m_{1}\oplus
m_{1}^{\prime},m_{2}\oplus m_{2}^{\prime})\in R^{\oplus}$. Moreover, if $R$ is
an equivalence relation, then $R^{\oplus}$ is subtractive: if $(m_{1}\oplus
m_{1}^{\prime},$ $m_{2}\oplus m_{2}^{\prime})\in R^{\oplus}$ and
$(m_{1},m_{2})\in R^{\oplus}$, then $(m_{1}^{\prime},m_{2}^{\prime})\in
R^{\oplus}$. (Proof in [20]).  $\Box$

###### Definition 8

(Rooted branching team equivalence) Given a finite-state machine $N=(S,A,T)$
and branching bisimulation equivalence $\approx$ and rooted branching
bisimulation equivalence ${\approx_{c}}$, we define branching team/rooted
branching team equivalences as the relations $\approx^{\oplus}$ and
$\approx_{c}^{\oplus}$, respectively.  $\Box$

Of course, (rooted) branching team equivalence relates markings of the same
size only; moreover, $\approx^{\oplus}$ and $\approx_{c}^{\oplus}$ are
equivalence relations by Proposition 1, as the additive closure of an
equivalence relation is also an equivalence relation.

Moreover, it is easy to prove that $\approx^{\oplus}$ enjoys a form of
stuttering property (cf. Remark 1), concerning sequential silent transition
sequences:

if $m_{0}[t_{1}\rangle m_{1}[t_{2}\rangle\ldots m_{n-1}[t_{n}\rangle m_{n}$,
$l(t_{i})=\tau$ for $i=1,\ldots,n$ (hence, the transition sequence
$t_{1}t_{2}\ldots t_{n}$ is silent), and
$\mbox{${}^{\bullet}t_{i}$}=\mbox{$t_{i-1}^{\bullet}$}$ for $i=2,\ldots,n$
(hence, the transition sequence $t_{1}t_{2}\ldots t_{n}$ is sequential), and,
moreover, $m_{0}\approx^{\oplus}m_{n}$, then $m_{i}\approx^{\oplus}m_{j}$ for
$i,j=1,\ldots,n$.

In [21] we proved that whenever $m_{1}\approx^{\oplus}m_{2}$, if
$m_{1}[t_{1}\rangle m_{1}^{\prime}$, then

  * –

either $l(t_{1})=\tau$ and

    * (i)

either $\exists\sigma_{2}$ nonempty, silent, sequential, such that
$\mbox{${}^{\bullet}t_{1}$}\approx\mbox{${}^{\bullet}\sigma_{2}$}$,
$\mbox{$t_{1}^{\bullet}$}\approx\mbox{$\sigma_{2}^{\bullet}$}$,
$\mbox{${}^{\bullet}t_{1}$}\approx\mbox{$\sigma_{2}^{\bullet}$}$,
$m_{2}[\sigma_{2}\rangle m_{2}^{\prime}$ with
$m_{1}\approx^{\oplus}m_{2}^{\prime}$ and
$m_{1}^{\prime}\approx^{\oplus}m_{2}^{\prime}$,

    * (ii)

or $\exists s_{2}\in m_{2}$ such that $\mbox{${}^{\bullet}t_{1}$}\approx
s_{2}$, $\mbox{$t_{1}^{\bullet}$}\approx s_{2}$, with
$m_{1}^{\prime}\approx^{\oplus}m_{2}$,

  * –

or $\exists\sigma,t_{2}$ such that $\sigma t_{2}$ is sequential, $\sigma$ is
silent, $l(t_{1})=l(t_{2})$,
$\mbox{${}^{\bullet}t_{1}$}\approx\mbox{${}^{\bullet}\sigma t_{2}$}$,
$\mbox{${}^{\bullet}t_{1}$}\approx\mbox{${}^{\bullet}t_{2}$}$,
$\mbox{$t_{1}^{\bullet}$}\approx^{\oplus}\mbox{$t_{2}^{\bullet}$}$,
$m_{2}[\sigma\rangle m[t_{2}\rangle m_{2}^{\prime}$ with
$m_{1}\approx^{\oplus}m$ and $m_{1}^{\prime}\approx^{\oplus}m_{2}^{\prime}$;

and, symmetrically, $\forall t_{2}$ such that $m_{2}[t_{2}\rangle
m_{2}^{\prime}$. In the either-(i)-case, we can easily prove that all the
markings in the path from $m_{2}$ to $m_{2}^{\prime}$ are branching team
bisimilar; similarly, in the or-case, all the markings in the path from
$m_{2}$ to $m$ are branching team bisimilar. Hence, branching team
bisimilarity $\approx^{\oplus}$ does fully respect the timing of choices.

###### Remark 4

(Complexity) Once the place relations $\approx$ and $\approx_{c}$ have been
computed once and for all for the given net in $O(m\cdot\mbox{ log }n)$ time,
the algorithm in [20] checks whether two markings $m_{1}$ and $m_{2}$ of equal
size $k$ are team equivalent in $O(k^{2})$ time.  $\Box$

##  3 CFM: Syntax, Semantics, Axiomatization

###  3.1 Syntax

Let $Act=H\cup L\cup\\{\tau\\}$ be a finite set of actions, ranged over by
$\mu$, composed of two disjoint subsets $L$ and $H$ of low-level actions and
high-level ones, respectively, and by the silent action $\tau$. Let
$\mathcal{C}$ be a finite set of constants, disjoint from $Act$, ranged over
by $A,B,C,\ldots$. The CFM terms (where CFM is the acronym of Concurrent
Finite-state Machines) are generated from actions and constants by the
following abstract syntax (with three syntactic categories):

$\begin{array}[]{lccccccccccl}s&::=&\mbox{\bf 0}&|&\mu.q&|&s+s&\hskip
28.45274pt\mbox{{\em guarded processes}}\\\ q&::=&s&|&C&&&\hskip
28.45274pt\mbox{{\em sequential processes}}\\\
p&::=&q&|&p\mbox{$\,|\,$}p&&&\hskip 28.45274pt\mbox{{\em parallel
processes}}\\\ \end{array}$

where 0 is the empty process, $\mu.q$ is a process where action $\mu$ prefixes
the residual $q$ ($\mu.-$ is the action prefixing operator), $s_{1}+s_{2}$
denotes the alternative composition of $s_{1}$ and $s_{2}$ ($-+-$ is the
choice operator), $p_{1}\mbox{$\,|\,$}p_{2}$ denotes the asynchronous parallel
composition of $p_{1}$ and $p_{2}$ and $C$ is a constant. A constant $C$ may
be equipped with a definition, but this must be a guarded process, i.e.,
$C\doteq s$. A term $p$ is a CFM process if each constant in Const$(p)$ (the
set of constants used by $p$; see [19] for details) is equipped with a
defining equation (in category $s$). The set of CFM processes is denoted by
$\mathcal{P}_{CFM}$, the set of its sequential processes, i.e., those in
syntactic category $q$, by $\mathcal{P}_{CFM}^{seq}$ and the set of its
guarded processes, i.e., those in syntactic category $s$, by
$\mathcal{P}_{CFM}^{grd}$. By $sort(p)\subseteq Act$ we denote the set of all
the actions occurring in $p$ and in the body of the constants in Const$(p)$.

$\begin{array}[]{lcllcl}\mbox{(Pref)}&\begin{array}[]{c}\\\
\hline\cr\mu.p{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p\end{array}&&\;\;\;\mbox{(Cons)}&\begin{array}[]{c}p{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\\\
\hline\cr
C{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\end{array}&C\doteq
p\\\
\mbox{(Sum${}_{1}$)}&\begin{array}[]{c}p{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\\\
\hline\cr
p+q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\end{array}&&\;\;\;\mbox{(Sum${}_{2}$)}&\begin{array}[]{c}q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}q^{\prime}\\\
\hline\cr
p+q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}q^{\prime}\end{array}\\\
\mbox{(Par${}_{1}$)}&\begin{array}[]{c}p{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\\\
\hline\cr
p\mbox{$\,|\,$}q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p^{\prime}\mbox{$\,|\,$}q\end{array}&&\;\;\;\mbox{(Par${}_{2}$)}&\begin{array}[]{c}q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}q^{\prime}\\\
\hline\cr
p\mbox{$\,|\,$}q{\mbox{${\>\stackrel{{\scriptstyle\mu}}{{\longrightarrow}}\>}$}}p\mbox{$\,|\,$}q^{\prime}\end{array}\\\\[-5.69046pt]
\end{array}$

Table 1: Structural operational LTS semantics for CFM

$\begin{array}[]{rcllrcllllll}\mbox{$dec$}(\mbox{\bf
0})&=&\theta&&\mbox{$dec$}(\mu.p)&=&\\{\mu.p\\}\\\
\mbox{$dec$}(p+p^{\prime})&=&\\{p+p^{\prime}\\}&&\mbox{$dec$}(C)&=&\\{C\\}\\\
\mbox{$dec$}(p\mbox{$\,|\,$}p^{\prime})&=&\mbox{$dec$}(p)\oplus\mbox{$dec$}(p^{\prime})\\\\[-5.69046pt]
\end{array}$

Table 2: Decomposition function

###  3.2 Semantics

The interleaving LTS semantics for CFM is given by the structural operational
rules in Table 1. Note that each state of the LTS is a CFM process. As an
example, the LTS for $C\mbox{$\,|\,$}B$, with $C\doteq h.B$ and $B\doteq l.B$,
is described in Figure 1(c). It is possible to prove that, for any $p$, the
set of states reachable from $p$ is finite [19].

The Petri net semantics for CFM is such that the set $S_{CFM}$ of places is
the set of the sequential CFM processes, without 0, i.e.,
$S_{CFM}={\mathcal{P}}_{CFM}^{seq}\setminus\\{\mbox{\bf 0}\\}$. The
decomposition function
$\mbox{$dec$}:{\mathcal{P}}_{CFM}\rightarrow{\mathcal{M}}(S_{CFM})$, mapping
process terms to markings, is defined in Table 2. An easy induction proves
that for any $p\in\mathcal{P}_{CFM}$, $\mbox{$dec$}(p)$ is a finite multiset
of sequential processes. Note that, if $C\doteq\mbox{\bf 0}$, then
$\theta=\mbox{$dec$}(\mbox{\bf 0})\neq\mbox{$dec$}(C)=\\{C\\}$. Note also that
$\theta=\mbox{$dec$}(\mbox{\bf 0})\neq\mbox{$dec$}(\mbox{\bf 0}+\mbox{\bf
0})=\\{\mbox{\bf 0}+\mbox{\bf 0}\\}$, which is a deadlock place.

$\begin{array}[]{rcllcllcl}\llbracket\mbox{\bf
0}\rrbracket_{I}&=&(\emptyset,\emptyset,\emptyset,\theta)&\\\
\llbracket\mu.p\rrbracket_{I}&=&(S,A,T,\\{\mu.p\\})&\mbox{ given }\llbracket
p\rrbracket_{I}=(S^{\prime},A^{\prime},T^{\prime},\mbox{$dec$}(p))\;\mbox{ and
where }\\\ &&&S=\\{\mu.p\\}\cup S^{\prime},\;A=\\{\mu\\}\cup
A^{\prime},\;T=\\{(\\{\mu.p\\},\mu,\mbox{$dec$}(p))\\}\cup T^{\prime}\\\
\llbracket p_{1}+p_{2}\rrbracket_{I}&=&(S,A,T,\\{p_{1}+p_{2}\\})&\mbox{ given
}\llbracket
p_{i}\rrbracket_{I}=(S_{i},A_{i},T_{i},\mbox{$dec$}(p_{i}))\;\mbox{ for
$i=1,2$, and where}\\\ &&&S=\\{p_{1}+p_{2}\\}\cup S_{1}^{\prime}\cup
S_{2}^{\prime},\mbox{ with, for $i=1,2$, }\\\
&&&S^{\prime}_{i}=\begin{cases}S_{i}&\\!\\!\mbox{$\exists t\in T_{i}$ such
that $\mbox{$t^{\bullet}$}(p_{i})>0$}\\\
S_{i}\setminus\\{p_{i}\\}&\\!\\!\mbox{otherwise}\\\ \end{cases}\\\
&&&A=A_{1}\cup A_{2},\;T=T^{\prime}\cup T^{\prime}_{1}\cup
T^{\prime}_{2},\mbox{ with, for $i=1,2$, }\\\
&&&T^{\prime}_{i}=\begin{cases}T_{i}&\\!\\!\mbox{$\exists t\in
T_{i}\,.\,\mbox{$t^{\bullet}$}(p_{i})>0$}\\\ T_{i}\setminus\\{t\in
T_{i}\;\big{|}\;\mbox{${}^{\bullet}t$}(p_{i})>0\\}&\\!\\!\mbox{otherwise}\\\
\end{cases}\\\
&&&T^{\prime}=\\{(\\{p_{1}+p_{2}\\},\mu,m)\;\big{|}\;(\\{p_{i}\\},\mu,m)\in
T_{i},i=1,2\\}\\\ \llbracket
C\rrbracket_{I}&=&(\\{C\\},\emptyset,\emptyset,\\{C\\})&\mbox{ if $C\in I$
}\\\ \llbracket C\rrbracket_{I}&=&(S,A,T,\\{C\\})&\mbox{ if $C\not\in I$,
given $C\doteq p$ and }\llbracket
p\rrbracket_{I\cup\\{C\\}}=(S^{\prime},A^{\prime},T^{\prime},\mbox{$dec$}(p))\\\
&&&A=A^{\prime},S=\\{C\\}\cup S^{\prime\prime},\mbox{ where }\\\
&&&S^{\prime\prime}=\begin{cases}S^{\prime}&\\!\\!\mbox{$\exists t\in
T^{\prime}\,.\,\mbox{$t^{\bullet}$}(p)>0$}\\\
S^{\prime}\setminus\\{p\\}&\\!\\!\mbox{otherwise}\\\ \end{cases}\\\
&&&T=\\{(\\{C\\},\mu,m)\;\big{|}\;(\\{p\\},\mu,m)\in T^{\prime}\\}\cup
T^{\prime\prime}\mbox{ where }\\\
&&&T^{\prime\prime}=\begin{cases}T^{\prime}&\\!\\!\mbox{$\exists t\in
T^{\prime}\,.\,\mbox{$t^{\bullet}$}(p)>0$}\\\ T^{\prime}\setminus\\{t\in
T^{\prime}\;\big{|}\;\mbox{${}^{\bullet}t$}(p)>0\\}&\\!\\!\mbox{otherwise}\\\
\end{cases}\\\ \llbracket
p_{1}\mbox{$\,|\,$}p_{2}\rrbracket_{I}&=&(S,A,T,m_{0})&\mbox{ given
}\llbracket p_{i}\rrbracket_{I}=(S_{i},A_{i},T_{i},m_{i})\;\mbox{ for $i=1,2$,
and where }\\\ &&&S=S_{1}\cup S_{2},\;A=A_{1}\cup A_{2},\;T=T_{1}\cup
T_{2},\;m_{0}=m_{1}\oplus m_{2}\\\\[-5.69046pt] \end{array}$

Table 3: Denotational net semantics

The net system $\llbracket p\rrbracket_{\emptyset}$ associated with process
$p$ is defined in a denotational style. The details of the construction are
outlined in Table 3. The mapping is parametrized by a set of constants that
have already been found while scanning $p$; such a set is initially empty and
it is used to avoid looping on recursive constants. The definition is syntax
driven and also the places of the constructed net are syntactic objects, i.e.,
CFM sequential process terms. E.g., the net system $\llbracket a.\mbox{\bf
0}\rrbracket_{\emptyset}$ is a net composed of one single marked place, namely
process $a.\mbox{\bf 0}$, and one single transition $(\\{a.\mbox{\bf
0}\\},a,\theta)$. A bit of care is needed in the rule for choice: in order to
include only strictly necessary places and transitions, the initial place
$p_{1}$ (or $p_{2}$) of the subnet $\llbracket p_{1}\rrbracket_{I}$ (or
$\llbracket p_{2}\rrbracket_{I}$) is to be kept in the net for $p_{1}+p_{2}$
only if there exists a transition reaching place $p_{1}$ (or $p_{2}$) in
$\llbracket p_{1}\rrbracket_{I}$ (or $\llbracket p_{2}\rrbracket_{I}$),
otherwise $p_{1}$ (or $p_{2}$) can be safely removed in the new net.
Similarly, for the rule for constants. Examples of the net construction for
some CFM terms can be found in [19, 21].

This net semantics has the following important properties:

  * $\bullet$

the semantics of a CFM process term $p$, i.e., the net $\llbracket
p\rrbracket_{\emptyset}$, is a finite-state machine, whose initial marking is
$\mbox{$dec$}(p)$; moreover,

  * $\bullet$

for any finite-state machine $N(m_{0})$ (whose places and transitions are all
reachable from $m_{0}$), there exists a CFM process term $p_{N(m_{0})}$ such
that its semantics $\llbracket p_{N(m_{0})}\rrbracket_{\emptyset}$ is a net
isomorphic to $N(m_{0})$ (Representability Theorem).

Therefore, thanks to these results (proved in [19]), we can conclude that the
CFM process algebra truly represents the class of finite-state machines, up to
isomorphism. Hence, we can transpose the definition of (rooted) branching team
equivalence from finite-state machines to CFM process terms in a simple way.

###### Definition 9

Two CFM processes $p$ and $q$ are (rooted) branching team equivalent, denoted
$p\approx^{\oplus}q$ and $p\approx_{c}^{\oplus}q$, respectively, if, by taking
the (union of the) nets $\llbracket p\rrbracket_{\emptyset}$ and $\llbracket
q\rrbracket_{\emptyset}$, we have that
$\mbox{$dec$}(p)\approx^{\oplus}\mbox{$dec$}(q)$ and
$\mbox{$dec$}(p)\approx_{c}^{\oplus}\mbox{$dec$}(q)$, respectively.  $\Box$

Of course, for sequential CFM processes, (rooted) branching team equivalence
$\approx^{\oplus}$ ($\approx_{c}^{\oplus}$) coincides with (rooted) branching
bisimilarity on places $\approx$ ($\approx_{c}$).

Finally, as we are going to use an auxiliary restriction operator over CFM
terms of the form $p\setminus H$, we define its net semantics as follows.

###### Definition 10

(Semantics of the auxiliary restriction operator) Given a CFM process $p$,
whose net semantics is $\llbracket
p\rrbracket_{\emptyset}=(S,A,T,\mbox{$dec$}(p))$, we define the net associated
to $p\setminus H$ as the net $\llbracket p\setminus
H\rrbracket_{\emptyset}=(S^{\prime},A^{\prime},T^{\prime},m)$ where

  * $\bullet$

$S^{\prime}=\\{s\setminus H\;\big{|}\;s\in S\\}$, i.e., each place is
decorated by the restriction operator;

  * $\bullet$

$A^{\prime}=A\setminus H$, i.e., $\\{\mu\;\big{|}\;\mu\in A,\mu\not\in H\\}$;

  * $\bullet$

$T^{\prime}=\\{(\mbox{${}^{\bullet}t$}\setminus
H,l(t),\mbox{$t^{\bullet}$}\setminus H)\;\big{|}\;t\in T,l(t)\not\in H\\}$;

  * $\bullet$

$m=\mbox{$dec$}(p)\setminus H$, where the restriction operator is applied
element-wise to the places, if any, of the marking $\mbox{$dec$}(p)$.

$\Box$

As an example, the net for $C\mbox{$\,|\,$}B$, with $C\doteq h.B$ and $B\doteq
l.B$, is outlined in Figure 2(a), while, assuming that $H$ is composed of the
single action $h$, the net for $(C\mbox{$\,|\,$}B)\setminus h$ is in Figure
2(b).

Branching team bisimilarity is a congruence for action prefixing, parallel
composition, recursion (via process constants) and restriction, but not for
the choice operator. For instance, $\tau.a.\mbox{\bf
0}\approx^{\oplus}a.\mbox{\bf 0}$, but $b.\mbox{\bf 0}+\tau.a.\mbox{\bf
0}\not\approx^{\oplus}b.\mbox{\bf 0}+a.\mbox{\bf 0}$. However, rooted
branching team bisimilarity $\approx_{c}^{\oplus}$ is a congruence also for
the choice operator, so that it can be axiomatized. (More details on
congruence properties and algebraic properties in [21].)

###  3.3 Axiomatization

In this section we recall the sound and complete, finite axiomatization of
rooted branching team equivalence $\approx_{c}^{\oplus}$ over CFM, outlined in
[21], where the reader can find more detail. For simplicity’s sake, the
syntactic definition of open CFM (i.e., CFM with variables) is given with only
one syntactic category, but each ground instantiation of an axiom must respect
the syntactic definition of CFM given (by means of three syntactic categories)
in Section 3.1; this means that we can write the axiom $x+(y+z)=(x+y)+z$, but
it is invalid to instantiate it to $C+(a.\mbox{\bf 0}+b.\mbox{\bf
0})=(C+a.\mbox{\bf 0})+b.\mbox{\bf 0}$ because these are not legal CFM
processes (the constant $C$ cannot be used as a summand).

$\begin{array}[]{llrcll}{\bf
A1}&\;\;\mbox{Associativity}&\;\;x+(y+z)&=&(x+y)+z&\\\ {\bf
A2}&\;\;\mbox{Commutativity}&\;\;x+y&=&y+x&\\\ {\bf
A3}&\;\;\mbox{Identity}&\;\;x+\mbox{\bf 0}&=&x&\quad\mbox{ if $x\neq\mbox{\bf
0}$}\\\ {\bf A4}&\;\;\mbox{Idempotence}&\;\;x+x&=&x&\quad\mbox{ if
$x\neq\mbox{\bf 0}$}\\\ \end{array}$

$\begin{array}[]{llrcll}{\bf
B}&\;\;\mbox{}&\;\;\mu.(\tau.(x+y)+x)&=&\mu.(x+y)&\\\ \end{array}$

$\begin{array}[]{llrcllll}{\bf R1}&\;\mbox{Stuck}&\mbox{if $C\doteq\mbox{\bf
0}$,}&\mbox{then}&\mbox{$C=\mbox{\bf 0}+\mbox{\bf 0}$}&\\\ {\bf
R2}&\;\mbox{Unfolding}&\mbox{if $C\doteq p\;\wedge\;p\neq\mbox{\bf
0}$,}&\mbox{then}&\mbox{$C=p$}&\\\ {\bf R3}&\;\mbox{Folding}&\mbox{if $C\doteq
p\\{C/x\\}\;\wedge\;og(p)\;\wedge\;q=p\\{q/x\\}$,}&\mbox{then}&\mbox{$C=q$}&\\\
\end{array}$

$\begin{array}[]{llrlllll}{\bf U1}&\;\mbox{if
$C\doteq(\tau.x+p)\\{C/x\\}\wedge D\doteq(\tau.(p+\mbox{\bf
0})+p)\\{D/x\\}$}&\mbox{then}&C=D&\\\ {\bf U2}&\;\mbox{if
$C\doteq(\tau.(\tau.x+p)+r)\\{C/x\\}\wedge
D\doteq(\tau.(p+r)+r)\\{D/x\\}$}&\mbox{then}&C=D&\\\ \end{array}$

$\begin{array}[]{llrcllll}{\bf U3}&\;\mbox{if
$C\doteq(\tau.(\tau.q+p)+r)\\{C/x\\}\wedge
D\doteq(\tau.(q+p)+r)\\{D/x\\}$,}\\\ &\mbox{ $x$ unguarded in
$q\in\mathcal{P}_{CFM}^{grd}$,}&\mbox{ then}&C=D\\\ {\bf U4}&\;\mbox{if
$C\doteq(\tau.(\tau.x+p)+\tau.(\tau.x+q)+r)\\{C/x\\}$}\\\
&\mbox{$\wedge\;D\doteq(\tau.(\tau.x+p+q)+r)\\{D/x\\}$}&\mbox{ then}&C=D\\\
\end{array}$

$\begin{array}[]{llrcll}{\bf
P1}&\;\;\mbox{Associativity}&\;\;x\mbox{$\,|\,$}(y\mbox{$\,|\,$}z)&=&(x\mbox{$\,|\,$}y)\mbox{$\,|\,$}z&\\\
{\bf P2}&\;\;\mbox{Commutativity}&\;\;x\mbox{$\,|\,$}y&=&y\mbox{$\,|\,$}x&\\\
{\bf P3}&\;\;\mbox{Identity}&\;\;x\mbox{$\,|\,$}\mbox{\bf
0}&=&x&\\\\[-8.5359pt] \end{array}$

Table 4: Axioms for rooted branching team equivalence

The set of axioms are outlined in Table 4. We call $E$ the set of axioms
$\\{$A1, A2, A3, A4, B, R1, R2, R3, U1, U2, U3, U4, P1, P2, P3$\\}$. By the
notation $E\vdash p=q$ we mean that there exists an equational deduction proof
of the equality $p=q$, by using the axioms in $E$. Besides the usual
equational deduction rules of reflexivity, symmetry, transitivity,
substitutivity and instantiation (see, e.g., [18]), in order to deal with
constants we need also the following recursion congruence rule:

$\frac{p=q\;\wedge\;A\doteq p\\{A/x\\}\;\wedge\;B\doteq q\\{B/x\\}}{A=B}$

where $p\\{A/x\\}$ denotes the open term $p$ where all occurrences of the
variable $x$ are replaced by $A$. The axioms A1-A4 are the usual axioms for
choice where, however, A3-A4 have the side condition $x\neq\mbox{\bf 0}$;
hence, it is not possible to prove $E\vdash\mbox{\bf 0}+\mbox{\bf 0}=\mbox{\bf
0}$, as expected, because these two terms have a completely different
semantics. Axiom B, originally in [15], is the axiom for rooted branching
bisimilarity. The conditional axioms R1-R3 are about process constants. Note
that R2 requires that $p$ is not (equal to) 0 (condition $p\neq\mbox{\bf 0}$).
Note also that these conditional axioms are actually a finite collection of
axioms, one for each constant definition: since the set $\mathcal{C}$ of
process constants is finite, the instances of R1-R3 are finitely many. Note
that axiom R3 requires that the body $p$ of the constant $C\doteq p\\{C/x\\}$
is observationally guarded (condition $og(p)$), meaning that
$C{\mbox{${\>\stackrel{{\scriptstyle\tau}}{{\nRightarrow}}\>}$}}C$. The axioms
$\\{$U1, U2, U3, U4$\\}$ are necessary to prove (soundness and) completeness
for the whole of CFM, hence including observationally unguarded (i.e.,
possibly silently divergent) processes. Finally, we have axioms P1-P3 for
parallel composition.

###### Theorem 3.1

[21](Sound and Complete) For every $p,q\in\mathcal{P}_{CFM}$, $E\vdash p=q$ if
and only if $p\approx_{c}^{\oplus}q$.  $\Box$

##  4 DNI: Distributed Non-Interference

###  4.1 Definition and Compositional Verification

###### Definition 11

(Distributed Non-Interference (DNI)) A CFM process $p$ enjoys the distributed
non-interference property (DNI, for short) if for each
$p^{\prime},p^{\prime\prime}$, reachable from $p$, and for each $h\in H$, such
that $p^{\prime}{\mbox{${\>\stackrel{{\scriptstyle
h}}{{\longrightarrow}}\>}$}}p^{\prime\prime}$, we have that
$p^{\prime}\setminus H\approx^{\oplus}p^{\prime\prime}\setminus H$ holds.
$\Box$

This intuitive and simple definition is somehow hybrid, because, on the one
hand, it refers to reachable states $p^{\prime}$ and $p^{\prime\prime}$ in the
LTS semantics, while, on the other hand, it requires that $p^{\prime}\setminus
H\approx^{\oplus}p^{\prime\prime}\setminus H$, a condition that can be checked
on the Petri net semantics. We can reformulate this definition in such a way
that it refers only to the Petri net semantics, a reformulation that will be
very useful in proving the following theorem.

###### Definition 12

(DNI on Petri nets) Given a CFM process $p$ and the FSM $\llbracket
p\rrbracket_{\emptyset}$ and its low-observable subnet $\llbracket p\setminus
H\rrbracket_{\emptyset}$, we say that $p$ satisfies DNI if for each
$m_{1},m_{2}$, reachable from $\mbox{$dec$}(p)$ in $\llbracket
p\rrbracket_{\emptyset}$, and for each $h\in H$, such that
$m_{1}{\mbox{${\>\stackrel{{\scriptstyle h}}{{\longrightarrow}}\>}$}}m_{2}$,
we have that the two markings $m_{1}\setminus H$ and $m_{2}\setminus H$ of
$\llbracket p\setminus H\rrbracket_{\emptyset}$ are branching team equivalent.
$\Box$

###### Theorem 4.1

A process $p$ is not DNI if and only if there exists $p_{i}\in\mbox{$dec$}(p)$
such that $p_{i}$ is not DNI.

###### Corollary 1

A CFM process $p$ is DNI if and only if each $p_{i}\in dom(\mbox{$dec$}(p))$
is DNI.

Hence, in order to check whether $p$ is DNI, we first compute
$\mbox{$dec$}(p)$ to single out its sequential components; then, we consider
only the elements of $dom(\mbox{$dec$}(p))$, because it is necessary to check
each sequential component only once. For instance, if
$p=(q_{1}\mbox{$\,|\,$}q_{2})\mbox{$\,|\,$}(q_{1}\mbox{$\,|\,$}q_{2})$, then,
assuming $q_{1}$ and $q_{2}$ sequential, $\mbox{$dec$}(p)=2\cdot q_{1}\oplus
2\cdot q_{2}$, so that $dom(\mbox{$dec$}(p))=\\{q_{1},q_{2}\\}$, and so we
have simply to check whether $q_{1}$ and $q_{2}$ are DNI.

###### Corollary 2

If $p\approx^{\oplus}q$ and $p$ is DNI, then also $q$ is DNI.

###  4.2 Efficient Verification Based on a Structural Characterization

Because of the shape of finite-state machines and because of additivity (and
subtractivity) of the behavioral relation $\approx^{\oplus}$ (cf. Remark 3), a
very efficient DNI verification can be done by the following polynomial
algorithm.

Given the CFM process $p$, first compute the nets $\llbracket
p\rrbracket_{\emptyset}=(S,A,T,\mbox{$dec$}(p))$ and the low-observable subnet
$\llbracket p\setminus H\rrbracket_{\emptyset}$. Then, compute branching
bisimilarity $\approx$ on the places of the net $\llbracket p\setminus
H\rrbracket_{\emptyset}$. Finally, for each $t\in T$ such that $l(t)\in H$,
check whether $\mbox{${}^{\bullet}t$}\setminus H$ and
$\mbox{$t^{\bullet}$}\setminus H$ are branching bisimilar in the net
$\llbracket p\setminus H\rrbracket_{\emptyset}$: if this is the case for all
the high-level transitions of $\llbracket p\rrbracket_{\emptyset}$, then $p$
is DNI; on the contrary, if for some $t$ the check fails (e.g., because
$\mbox{$t^{\bullet}$}=\theta$), then $p$ is not DNI.

The correctness of this polynomial algorithm follows by the fact that the net
$\llbracket p\rrbracket_{\emptyset}$ is dynamically reduced, i.e., all the
places and the transitions are reachable from the initial marking
$\mbox{$dec$}(p)$. Once $\llbracket p\rrbracket_{\emptyset}$ has been computed
by the polynomial algorithm described in Table 3, and $\llbracket p\setminus
H\rrbracket_{\emptyset}$ is computed by the simple algorithm in Definition 10,
the complexity of this procedure is essentially related to the problem of
computing $\approx$ (cf. Remark 2) for $\llbracket p\setminus
H\rrbracket_{\emptyset}$ and to give it a suitable adjacency matrix
representation in order to check easily, for each high-level transition $t\in
T$, whether the two relevant places $\mbox{${}^{\bullet}t$}\setminus H$ and
$\mbox{$t^{\bullet}$}\setminus H$ are related by $\approx$.

###  4.3 Typing System

In this section we provide a syntactic characterization on CFM of a slight
strengthening of DNI, which is based on rooted branching team equivalence
$\approx_{c}$, rather than on $\approx$. With abuse of notation, also this
property is called DNI: $p$ is DNI if for each $p^{\prime}$, reachable from
$p$, and for each $h\in H$, such that
$p^{\prime}{\mbox{${\>\stackrel{{\scriptstyle
h}}{{\longrightarrow}}\>}$}}p^{\prime\prime}$ for some $p^{\prime\prime}$, we
have that $p^{\prime}\setminus H\approx_{c}^{\oplus}p^{\prime\prime}\setminus
H$ holds.

This syntactic characterization is based on a typing proof system, which
exploits the axiomatization of rooted branching team equivalence
$\approx_{c}^{\oplus}$ in Table 4. Let us first define an auxiliary operator
$r(-)$, which takes in input a CFM process $p$ and returns a CFM process
$p^{\prime}$ obtained from $p$ by pruning its high-level actions, so that
$sort(p^{\prime})\subseteq L\cup\\{\tau\\}$. Its definition is outlined in
Table 5, where $r(h.p)=\mbox{\bf 0}+\mbox{\bf 0}$ because the pruning of $h.p$
is to be considered as a deadlock place. For instance, consider $C\doteq
h.l.C+l.C$; then $r(C)=C^{\prime}$, where $C^{\prime}\doteq\mbox{\bf
0}+\mbox{\bf 0}+l.C^{\prime}$. Similarly, if $D\doteq l.h.D$, then
$r(D)=D^{\prime}$ where $D^{\prime}\doteq l.(\mbox{\bf 0}+\mbox{\bf 0})$. It
is a trivial observation that the net semantics of $r(p)$ is isomorphic to the
(reachable part of the) net semantics of $p\setminus H$ for any CFM process
$p$. Moreover, we also define the set of initial actions of $p$, denoted by
$In(p)$, whose definition is outlined in Table 6.

$\begin{array}[]{rcllrclrrlll}r(\mbox{\bf 0})&=&\mbox{\bf
0}&&r(h.p)&=&\mbox{\bf 0}+\mbox{\bf 0}&&r(\mu.p)&=&\mu.r(p)\mbox{ if $\mu\in
L\cup\\{\tau\\}$}\\\
r(p+p^{\prime})&=&r(p)+r(p^{\prime})&&r(p\mbox{$\,|\,$}p^{\prime})&=&r(p)\mbox{$\,|\,$}r(p^{\prime})&&r(C)&=&C^{\prime}\;\mbox{with
$C^{\prime}\doteq r(p)$ if $C\doteq p$}\\\\[-5.69046pt] \end{array}$

Table 5: Restriction function

$\begin{array}[]{rcllrclrrlll}In(\mbox{\bf
0})&=&\emptyset&&In(\mu.p)&=&\\{\mu\\}&&In(p+p^{\prime})&=&In(p)\cup
In(p^{\prime})\\\ In(p\mbox{$\,|\,$}p^{\prime})&=&In(p)\cup
In(p^{\prime})&&In(C)&=&In(p)\;\mbox{ if $C\doteq p$}\\\\[-5.69046pt]
\end{array}$

Table 6: Function computing the initial actions

$\begin{array}[]{cccccccc}\begin{array}[]{c}\\\ \hline\cr(\mbox{\bf
0},I):dni\end{array}&&\begin{array}[]{c}(p,I):dni,(q,I):dni,In(p+q)\subseteq
L\cup\\{\tau\\}\\\ \hline\cr(p+q,I):dni\end{array}\\\
\begin{array}[]{c}(p,I):dni,(q,I):dni\\\
\hline\cr(p\mbox{$\,|\,$}q,I):dni\end{array}&&\begin{array}[]{c}(p,I):dni,p\neq\mbox{\bf
0},(q,I):dni,E\vdash r(p)=r(q)\\\ \hline\cr(h.p+q,I):dni\end{array}\\\
\end{array}$

$\begin{array}[]{cccccccc}\begin{array}[]{c}(p,I):dni\quad\mu\in
L\cup\\{\tau\\}\\\
\hline\cr(\mu.p,I):dni\end{array}&&\begin{array}[]{c}E\vdash p=\mbox{\bf
0}+\mbox{\bf 0}\\\
\hline\cr(h.p,I):dni\end{array}&&\begin{array}[]{c}\emptyset\neq
In(p)\subseteq H,(p,I):dni\\\ \hline\cr(h.p,I):dni\end{array}\\\ \end{array}$

$\begin{array}[]{cccccccc}\begin{array}[]{c}C\in I\\\
\hline\cr(C,I):dni\end{array}&&\begin{array}[]{c}C\not\in I,C\doteq p,\\{{\bf
A_{1}-A_{4}}\\}\vdash p=p^{\prime},(p^{\prime},I\cup\\{C\\}):dni\\\
\hline\cr(C,I):dni\end{array}\\\ \end{array}$

Table 7: Typing proof system

Then we define a typing system on CFM processes such that, if a process $p$ is
typed, then $p$ satisfies DNI and, moreover, if $p$ is DNI, then there exists
a process $p^{\prime}$, obtained by possibly reordering its summands via
axioms ${\bf A_{1}-A_{4}}$, which is typed.

The typing system is outlined in Table 7, where we are using a set $I$ of
already scanned constants as an additional parameter (in order to avoid
looping on recursively defined constants). A process $p$ is typed if
$(p,\emptyset):dni$ is derivable by the rules; this is often simply denoted by
$p:dni$. The need for the argument $I$ is clear in the two rules for the
constant $C$: if $C$ has been already scanned (i.e. $C\in I$), then $C$ is
typed; otherwise it is necessary to check that its body $p$ is typed (or
possibly a sequential process $p^{\prime}$ obtained by reordering its
summands, i.e., such that $\\{{\bf A_{1}-A_{4}}\\}\vdash p=p^{\prime}$), using
a set enriched by $C$ (condition $(p^{\prime},I\cup\\{C\\}):dni$).

We are implicitly assuming that the formation rules in this table respect the
syntax of CFM; this means that, for instance, the second rule and the fourth
one require also that $p$ and $q$ are actually guarded processes because this
is the case in $p+q$. Note that in the second rule we are requiring that
$In(p+q)$ is a subset of $L\cup\\{\tau\\}$, so that, as no high-level action
is executable by $p$ and $q$ as their first action, no DNI check is required
at this level of the syntax.

The interesting cases are the three rules about the action prefixing operator
and the rule about the choice operator when a summand starts with a high-level
action. The fifth rule in Table 7 states that if $p$ is typed, then also
$\mu.p$ is typed, for each $\mu\in L\cup\\{\tau\\}$. The sixth rule states
that if $p$ is a deadlock place (condition $E\vdash p=\mbox{\bf 0}+\mbox{\bf
0}$), then $h.p$ is typed, for each $h\in H$; note that $p$ cannot be 0,
because $h.\mbox{\bf 0}$ is not secure (the low-observable marking before
performing $h$ has size one, while that after $h$ has size zero). The seventh
rule states that if $p$ is a typed term that can perform at least one action,
but only high-level actions initially (condition $\emptyset\neq In(p)\subseteq
H$), then $h.p$ is typed. It is interesting to observe that $h.\tau.(\mbox{\bf
0}+\mbox{\bf 0})$, which is DNI according to Definition 12 based on branching
team bisimilarity $\approx^{\oplus}$, is not DNI according to the current
definition based on rooted branching team bisimilarity $\approx_{c}^{\oplus}$,
and indeed $h.\tau.(\mbox{\bf 0}+\mbox{\bf 0})$ cannot be typed.

The fourth rule in Table 7 about the choice operator states that if we prefix
a generic typed process $p$ with a high-level action $h$, then it is necessary
that an additional typed summand $q$ is present such that $p\setminus H$ and
$q\setminus H$ are rooted branching team equivalent; this semantic condition
is expressed syntactically by requiring that $E\vdash r(p)=r(q)$, thanks to
Theorem 3.1. Note that the condition $p\neq\mbox{\bf 0}$ is necessary, because
$h.\mbox{\bf 0}+\mbox{\bf 0}$ is not secure; on the contrary,
$h.\tau.\mbox{\bf 0}+\tau.\mbox{\bf 0}$ is typed because
$E\vdash\tau.\mbox{\bf 0}=\tau.\mbox{\bf 0}$. It is interesting to observe
that this rule about the choice operator covers also the case when many
summands start with high-level actions. For instance, $h.l.l.\mbox{\bf
0}+(h.l.(h.l.\mbox{\bf 0}+l.\mbox{\bf 0})+l.l.\mbox{\bf 0})$ is typed because
$l.l.\mbox{\bf 0}$ and $h.l.(h.l.\mbox{\bf 0}+l.\mbox{\bf 0})+l.l.\mbox{\bf
0}$ are typed and $E\vdash r(l.l.\mbox{\bf 0})=r(h.l.(h.l.\mbox{\bf
0}+l.\mbox{\bf 0})+l.l.\mbox{\bf 0})$. This strategy is intuitively correct
(i.e., it respects DNI) because, by checking that the subterm
$h.l.(h.l.\mbox{\bf 0}+l.\mbox{\bf 0})+l.l.\mbox{\bf 0}$ is typed/DNI, we can
safely ignore the other summand $h.l.l.\mbox{\bf 0}$, as it does not
contribute any initial low-visible behavior.

Now we want to prove that the typing system characterizes DNI correctly. To
get convinced of this result, let us consider a couple of paradigmatic
examples. The process constant $C\doteq h.l.C+l.C$ is DNI because, if
$C{\mbox{${\>\stackrel{{\scriptstyle h}}{{\longrightarrow}}\>}$}}l.C$, then
$C\setminus H\approx_{c}(l.C)\setminus H$, which is equivalent to say that
$r(C)\approx_{c}r(l.C)$. Not surprisingly, we can type it. $(C,\emptyset):dni$
holds, because $(h.l.C+l.C,\\{C\\}):dni$ holds, because, in turn,
$(l.C,\\{C\\}):dni$ and $E\vdash r(l.C)=r(l.C)$. On the contrary, $D\doteq
l.h.D$ is not DNI because if $h.D{\mbox{${\>\stackrel{{\scriptstyle
h}}{{\longrightarrow}}\>}$}}D$, then $h.D\setminus H\not\approx_{c}D\setminus
H$ as $h.D\setminus H$ is stuck, while $D\setminus H$ can perform $l$. As a
matter of fact, $D$ is not typed: to get $(D,\emptyset):dni$, we need
$(l.h.D,\\{D\\}):dni$, which would require $(h.D,\\{D\\}):dni$, which is
false, as no rule for high-level prefixing is applicable.

###### Proposition 2

For each CFM process $p$, if $p:dni$, then $p$ satisfies DNI.

Note that the converse implication is not alway true, because of the ordering
of summands. For instance, $l.\mbox{\bf 0}+h.l.\mbox{\bf 0}$, which is clearly
DNI, is not typed. However, $\\{{\bf A_{1}-A_{4}}\\}\vdash l.\mbox{\bf
0}+h.l.\mbox{\bf 0}=h.l.\mbox{\bf 0}+l.\mbox{\bf 0}$, where the process
$h.l.\mbox{\bf 0}+l.\mbox{\bf 0}$ is typed.

###### Proposition 3

For each CFM process $p$, if $p$ is DNI, then there exists $p^{\prime}$ such
that $\\{{\bf A_{1}-A_{4}}\\}\vdash p=p^{\prime}$ and $p^{\prime}:dni$.

##  5 Related Literature

The non-interference problem in a distributed model of computation was first
addressed in [6, 7]. There, the Petri net class of unlabeled elementary net
systems (i.e., safe, contact-free nets) was used to describe some information
flow security properties, notably BNDC (Bisimulation Non-Deducibility on
Composition) and SBNDC (Strong BNDC), based on interleaving bisimilarity.
These two properties do coincide on unlabeled elementary net systems, but
actually SBNDC is stronger on labeled FSMs; for instance, the CFM process
$l.h.l.\mbox{\bf 0}+l.\mbox{\bf 0}+l.l.\mbox{\bf 0}$ is BNDC [13], while it is
not SBNDC; this explains why we have chosen SBNDC as our starting point
towards the formulation of DNI.

In [7] it is shown that BNDC can be characterized as a structural property of
the elementary net concerning two special classes of places: causal places,
i.e., places for which there are an incoming high transition and an outgoing
low transition; and conflict places, i.e., places for which there are both
low-level and high-level outgoing transitions. The main theorem in [7] states
that if places of these types are not present or cannot be reached from the
initial marking, then the net is BNDC. Starting from [7], Baldan and Carraro
in [2] provide a causal characterization of BNDC on safe Petri nets (with
injective labeling), in terms of the unfolding semantics. Nonetheless, the
BNDC property is based on an interleaving semantics and the true-concurrency
semantics is used only to provide efficient algorithms to check the possible
presence of interferences. For unbounded partially observed finite P/T nets
(i.e., net with unobservable high transitions and injective labeling on low
transitions), Best et al. proved in [4] that SBNDC is decidable.

Another paper studying non-interference over a distributed model is [8].
Bérard et al. study a form of non-interference similar to SNNI [13] for High-
level Message Sequence Charts (HMSC), a scenario language for the description
of distributed systems, based on composition of partial orders. The model
allows for unbounded parallelism and the observable semantics they use is
interleaving and linear-time (i.e., language-based). They prove that non-
interference is undecidable in general, while it becomes decidable for regular
behaviors, or for weaker variants based on observing local behavior only. Also
in this case, however, the truly-concurrent semantics based on partial orders
is used mainly for algorithmic purpose; in fact, the authors shows that their
decidable properties are PSPACE-complete, with procedures that never compute
the interleaving semantics of the original HMSC.

On the contrary, Baldan et al. in [3] define security policies, intuitively
similar to non-interference, where causality is used as a first-class concept.
So, their notion of non-interference is more restrictive than those based on
interleaving semantics. However, their approach is linear-time, while non-
interference is usually defined on a branching-time semantics, i.e., on
various forms of bisimulation. Moreover, it seems overly restrictive; for
instance, the CFM process $h.l.\mbox{\bf 0}+l.\mbox{\bf 0}$, which is DNI and
so non-interferent according to our approach, would be considered insecure in
their approach.

Finally, Joshua Guttman and Paul Rowe proposed [27, 28] a model of distributed
computation, called frame (essentially a directed graph whose nodes are
sequential systems, described by LTSs, and whose arcs are directed
communication channels), onto which they define some form of intransitive non-
interference, defined by exploiting the partial order description of the
system executions. Hence, also their proposal advocates the use of truly-
concurrent semantic models for defining non-interference.

Acknowledgments: This paper is a revised continuation of the conference paper
[22], extending the approach to Petri nets with silent transitions.

## References

  * [1] C. Autant, Z. Belmesk, Ph. Schnoebelen,  Strong bisimilarity on nets revisited,  in Procs. PARLE’91, vol. II: Parallel Languages, LNCS 506, 295-312, Springer, 1991.
  * [2] P. Baldan, A. Carraro,  A causal view on non-intereference,  Funda. Infor. 140(1):1-38, 2015.
  * [3] P. Baldan, A. Beggiato, A. Lluch-Lafuente,  Many-to-many information flow policies,  19th IFIP WG 6.1 International Conference on Coordination Models and Languages, LNCS 10319, 159-177, Springer, 2017.
  * [4] E. Best, Ph. Darondeau, R. Gorrieri,  On the decidability of non-interference over unbounded Petri nets,  in Procs 8th International Workshop on Security Issues in Concurrency (SecCo 2010), EPTCS 51, 16-33, 2010.
  * [5] E. Best, R. Devillers, A. Kiehn, L. Pomello,  Concurrent bisimulations in Petri nets,  Acta Informatica 28(3): 231-264, 1991.
  * [6] N. Busi, R. Gorrieri,  A survey on non-interference with Petri nets,  Lectures on Concurrency and Petri Nets, LNCS 3098, 328-344, Springer, 2003.
  * [7] N. Busi, R. Gorrieri,  Structural non-interference in elementary and trace nets,  Mathematical Structures in Computer Science 19(6): 1065-1090, 2009.
  * [8] B. Bérard, L. Hélouët, J. Mullins,  Non-interference in partial order models,  in Procs ACSD’15, IEEE Computer Society, 80-89, 2015.
  * [9] S. Christensen,  Decidability and Decomposition in Process Algebra,  Ph.D. Thesis, University of Edinburgh (1993)
  * [10] P. Degano, R. De Nicola, U. Montanari,  Partial ordering descriptions and observations of nondeterministic concurrent systems,  in (J. W. de Bakker, W. P. de Roever, G. Rozenberg, Eds.)  Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, 438-466, Springer, 1989.
  * [11] J. Esparza,  Decidability and complexity of Petri net problems: An introduction,  Lectures on Petri Nets I: Basic Models,  LNCS1491, 374-428, Springer, 1998.
  * [12] R. Focardi, R. Gorrieri.  A classification of security properties.  Journal of Computer Security 3(1):5-33, 1995.
  * [13] R. Focardi, R. Gorrieri,  Classification of security properties (part I: Information flow),  in Foundations of Security Analysis and Design I, LNCS 2171, 331-396, Springer, 2001.
  * [14] R.J. van Glabbeek, U. Goltz,  Equivalence notions for concurrent systems and refinement of actions,  in Procs. MFCS’89, LNCS 379, 237-248, Springer, 1989.
  * [15] R.J. van Glabbeek, W.P. Weijland,  Branching time and abstraction in bisimulation semantics,  Journal of the ACM 43(3):555-600, 1996.
  * [16] R.J. van Glabbeek,  Structure preserving bisimilarity: supporting an operational Petri net semantics of CCSP,  in Correct System Design – Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, LNCS 9360, 99-130, Springer, 2015.
  * [17] J.A. Goguen, J. Meseguer.  Security policy and security models.  Proc. of Symposium on Security and Privacy (SSP’82), IEEE CS Press, pp. 11-20, 1982.
  * [18] R. Gorrieri, C. Versari, Introduction to Concurrency Theory: Transition Systems and CCS, EATCS Texts in Theoretical Computer Science, Springer, 2015.
  * [19] R. Gorrieri,  Process Algebras for Petri Nets: The Alphabetization of Distributed Systems,  EATCS Monographs in Theoretical Computer Science, Springer, 2017.
  * [20] R. Gorrieri,  Team bisimilarity, and its associated modal logic, for BPP nets,  Acta Informatica, 2020. DOI: 10.1007/s00236-020-00377-4
  * [21] R. Gorrieri,  Team equivalences for finite-state machines with silent moves,  Information and Computation 275:104603, 2020. DOI:10.1016/j.ic.2020.104603
  * [22] R. Gorrieri,  Interleaving vs true concurrency: some instructive security examples,  in Procs. Petri Nets 2020, LNCS 12152, 131-152, Springer, 2020.
  * [23] R. Gorrieri,  A study on team bisimulation and h-team bisimulation for BPP nets, Theoretical Computer Science 897:83-113, 2022.
  * [24] R. Gorrieri,  Place bisimilarity is decidable, indeed!,  arXiv:2104.01392, april 2021.
  * [25] R. Gorrieri,  Branching place bisimilarity: A decidable behavioral equivalence for finite Petri nets with silent moves,  in Procs. 41st Formal Techniques for Distributed Objects, Components, and Systems (FORTE’21), LNCS 12719, 80-99, Springer, 2021.
  * [26] R. Gorrieri,  Branching place bisimilarity,  CoRR abs/2305.04222, September 2023, https://arXiv.2305.04222
  * [27] Joshua D. Guttman, Paul D. Rowe,  A cut principle for information flow,  in Procs. IEEE Computer Security Foundations (CSF 2015), 107-121, IEEE Computer Society Press, 2015.
  * [28] Joshua D. Guttman,  Information flow, distributed systems, and refinement, by example,  Concurrency, Security, and Puzzles: Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday, LNCS 10160, 88-103, Springer, 2017.
  * [29] C.A.R. Hoare,  Communicating Sequential Processes,  Prentice-Hall International Series in Computer Science, 1985.
  * [30] J.E. Hopcroft, R. Motwani, J.D. Ullman,  Introduction to Automata Theory, Languages and Computation, 2nd ed.,  Addison-Wesley, 2001.
  * [31] D.N. Jansen, J.F. Groote, J.J.A. Keiren, A. Wijs. An $O(m\cdot log\,n)$ algorithm for branching bisimilarity on labelled transition systems, in Procs. TACAS’20, LNCS 12079, 3-20, Springer, 2020.
  * [32] R. Milner. Communication and Concurrency, Prentice-Hall, 1989.
  * [33] M. Nielsen, P.S. Thiagarajan,  Degrees of non-determinism and concurrency: A Petri net view,  in Procs. of the Fourth Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’84), LNCS 181, 89-117, Springer, 1984.
  * [34] J.L. Peterson,  Petri Net Theory and the Modeling of Systems, Prentice-Hall, 1981.
  * [35] W. Reisig,  Petri Nets: An Introduction,  EATCS Monographs in Theor. Comp. Science,  Springer, 1985.
  * [36] P. Ryan,  Mathematical models of computer security,  in Foundations of Security Analysis and Design I, LNCS 2171, 1-61, Springer, 2001.
  * [37] P. Ryan, S. Schneider. Process algebra and noninterference, in Proc. of 12th Computer Security Foundations Workshop (CSFW), 214-227, IEEE CS Press, 1999.
  * [38] A. Rabinovich, B.A. Trakhtenbrot,  Behavior structures and nets,  Fundamenta Informaticae 11(4):357-404, 1988.