Design and Optimisation of the FlyFast Front-end for
Attribute-based Coordination
Diego Latella

Mieke Massink

Consiglio Nazionale delle Ricerche
Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”
Diego.Latella@isti.cnr.it, Mieke.Massink@isti.cnr.it

Collective Adaptive Systems (CAS) consist of a large number of interacting objects. The design
of such systems requires scalable analysis tools and methods, which have necessarily to rely on
some form of approximation of the system’s actual behaviour. Promising techniques are those based
on mean-field approximation. The FlyFast model-checker uses an on-the-fly algorithm for bounded
PCTL model-checking of selected individual(s) in the context of very large populations whose global
behaviour is approximated using deterministic limit mean-field techniques. Recently, a front-end
for FlyFast has been proposed which provides a modelling language, PiFF in the sequel, for the
Predicate-based Interaction for FlyFast. In this paper we present details of PiFF design and an
approach to state-space reduction based on probabilistic bisimulation for inhomogeneous DTMCs.

1

Introduction

Collective Adaptive Systems (CAS) consist of a large number of entities with decentralised control and
varying degrees of complex autonomous behaviour. They form the basis of many modern smart city
critical infrastructures. Consequently, their design requires support from formal methods and scalable
automatic tools based on solid mathematical foundations. In [29, 27], Latella et al. presented a scalable mean-field model-checking procedure for verifying bounded Probabilistic Computation Tree Logic
(PCTL, [19]) properties of an individual1 in the context of a system consisting of a large number of
interacting objects. The model-checking procedure is implemented in the tool FlyFast2 . The procedure
performs on-the-fly, mean-field, approximated model-checking based on the idea of fast simulation, as
introduced in [8]. More specifically, the behaviour of a generic agent with S states in a system with a
large number N of instances of the agent at given step (i.e. time) t is approximated by K(µ(t)) where
K(m) is the S × S probability transition matrix of an (inhomogeneous) DTMC and µ(t) is a vector of size
S approximating the mean behaviour of (the rest of) the system at t; each element of µ(t) is associated
with a distinct state of the agent, say C, and gives an approximation of the fraction of instances of the
agent that are in state C in the global system, at step t. Note that such an approximation is a deterministic
one, i.e. µ is a function of the step t (the exact behaviour of the rest of the system would instead be a
large DTMC in turn); note furthermore, that the above transition matrix does not depend on N [29, 27].
Recently, modelling and programming languages have been proposed specifically for autonomic
computing systems and CAS [12, 5]. Typically, in such frameworks, a system is composed of a set of
independent components where a component is a process equipped also with a set of attributes describing features of the component. The attributes of a component can be updated during its execution so
1 The

technique can be applied also to a finite selection of individuals; in addition, systems with several distinct types of
individuals can be dealt with; for the sake of simplicity, in the present paper we consider systems with many instances of a
single individual only and we focus in the model-checking a single individual in such a context.
2 http://j-sam.sourceforge.net/

De Vink and Wiklicky (Eds.): QAPL 2017
EPTCS 250, 2017, pp. 92–110, doi:10.4204/EPTCS.250.6

c D. Latella & M. Massink
This work is licensed under the
Creative Commons Attribution License.

D. Latella & M. Massink

93

that the association between attribute names and attribute values is maintained in the dynamic store of
the component. Attributes can be used in predicates appearing in language constructs for component
interaction. The latter is thus typically modelled using predicate-based output/input multicast, originally
proposed in [26], and playing a fundamental role in the interaction schemes of languages like SCEL [12]
and C ARMA [5]. In fact, predicate-based communication can be used by components to dynamically
organise themselves into ensembles and as a means to dynamically select partners for interaction. Furthermore, it provides a way for representing component features, like for instance component location in
space, which are fundamental for systems distributed in space, such as CAS [30].
In [9] we proposed a front-end modelling language for FlyFast that provides constructs for dealing
with components and predicate-based interaction; in the sequel, the language—which has been inspired
by C ARMA— will be referred to as PiFF, which stands for for Predicate-based Interaction for FlyFast.
Components interact via predicate-based communication. Each component consists of a behaviour, modelled as a DTMC-like agent, like in FlyFast, and a set of attributes. The attribute name-value correspondence is kept in the current store of the component. Actions are predicate based multi-cast output and
input primitives; predicates are defined over attributes. Associated to each action there is also an (atomic)
probabilistic store-update. For instance, assume components have an attribute named loc which takes values in the set of points of a space, thus recording the current location of the component. The following
action models a multi-cast via channel α to all components in the same location as the sender, making
it change location randomly: α ∗ [loc = my.loc]hiJump. Here Jump is assumed to randomly update the
store and, in particular attribute loc. The computational model is clock-synchronous, as in FlyFast, but
at the component level. In addition, each component is equipped with a local outbox. The effect of an
output action α ∗ [πr ]hiσ is to deliver output label αhi to the local outbox, together with the predicate πr ,
which (the store of) the receiver components will be required to satisfy, as well as the current store of
the component executing the action; the current store is updated according to update σ . Note that output
actions are non-blocking and that successive output actions of the same component overwrite its outbox.
An input action α ∗ [πs ]()σ by a component will be executed with a probability which is proportional to
the fraction of all those components whose outboxes currently contain the label αhi, a predicate πr which
is satisfied by the component, and a store which satisfies in turn predicate πs . If such a fraction is zero,
then the input action will not take place (input is blocking), otherwise the action takes place, the store of
the component is updated via σ , and its outbox cleared.
Related Work CAS are typically large systems, so that the formal analysis of models for such systems
hits invariantly the state-space explosion problem. In order to mitigate this problem, the so called ‘onthe-fly’ paradigm is often adopted (see e.g. [10, 4, 21, 16]).
In the context of probabilistic model-checking several on-the-fly approaches have been proposed,
among which [13], [28] and [18]. In [13], a probabilistic model-checker is shown for the time bounded
fragment of PCTL. An on-the-fly approach for full PCTL model-checking is proposed in [28] where,
actually, a specific instantiation is presented of an algorithm which is parametric with respect to the
specific probabilistic processes modelling language and logic, and their specific semantics. Finally,
in [18] an on-the-fly approach is used for detecting a maximal relevant search depth in an infinite state
space and then a global model-checking approach is used for verifying bounded Continuous Stochastic
Logic (CSL) [1, 2] formulas in a continuous time setting on the selected subset of states.
An on-the-fly approach by itself however, does not solve the challenging scalability problems that
arise in truly large parallel systems, such as CAS. To address this type of scalability challenges in probabilistic model-checking, recently, several approaches have been proposed. In [20, 17] approximate

94

Designing Attribute-based FlyFast

probabilistic model-checking is introduced. This is a form of statistical model-checking that consists in
the generation of random executions of an a priori established maximal length [25]. On each execution
the property of interest is checked and statistics are performed over the outcomes. The number of executions required for a reliable result depends on the maximal error-margin of interest. The approach relies
on the analysis of individual execution traces rather than a full state space exploration and is therefore
memory-efficient. However, the number of execution traces that may be required to reach a desired accuracy may be large and therefore time-consuming. The approach works for general models, i.e. models
where stochastic behaviour can also be non Markovian and that do not necessarily model populations of
similar objects. On the other hand, the approach is not independent from the number of objects involved.
As recalled above, in [27] a scalable model-checking algorithm is presented that is based on mean-field
approximation, for the verification of time bounded PCTL properties of an individual in the context of
a system consisting of a large number of interacting objects. Correctness of the algorithm with respect
to exact probabilistic model-checking has been proven in [27] as well. Also this algorithm is actually an
instantiation of the above mentioned parametric algorithm for (exact) probabilistic model-checking [28],
but the algorithm is instantiated on (time bounded PCTL and) the approximate, mean-field, semantics of
a population process modelling language. It is worth pointing out that FlyFast allows users to perform
simulations of their system models and to analyse the latter using their exact probabilistic semantics and
exact PCTL model-checking. In addition, the tool provides approximate model-checking for bounded
PCTL, using the model semantics based on mean-field.
The work of Latella et al. [27] is based on mean-field approximation in the discrete time setting;
approximated mean-field model-checking in the continuous time setting has been presented in the literature as well, where the deterministic approximation of the global system behaviour is formalised as
an initial value problem using a set of differential equations. Preliminary ideas on the exploitation of
mean-field convergence in continuous time for model-checking were informally sketched in [23], but
no model-checking algorithms were presented. Follow-up work on the above mentioned approach can
be found in [24] which relies on earlier results on fluid model-checking by Bortolussi and Hillston [6],
later published in [7], where a global CSL model-checking procedure is proposed for the verification
of properties of a selection of individuals in a population, which relies on fast simulation results. This
work is perhaps closest related to [27, 29]; however their procedure exploits mean-field convergence
and fast simulation [11, 15] in a continuous time setting—using a set of differential equations—rather
than in a discrete time setting—where an inductive definition is used. Moreover, that approach is based
on an interleaving model of computation, rather than a clock-synchronous one; furthermore, a global
model-checking approach, rather than an on-the-fly approach is adopted; it is also worth noting that the
treatment of nested formulas, whose truth value may change over time, turns out to be much more difficult in the interleaving, continuous time, global model-checking approach than in the clock-synchronous,
discrete time, on-the-fly one.
PiFF has been originally proposed in [9], where the complete formal, exact probabilistic, semantics
of the language have been defined. The semantics definition consists of three transition rules—one for
transitions associated with output actions, one for those associated with input actions, and one for transitions to be fired with residual probability. The rules induce a transition relation among component states
and compute the relevant probabilities. From the component transition relation, a component one-step
transition probability matrix is derived, the elements of which may depend on the fractions of the components in the system which are in a certain state. The system-wide one-step transition probability matrix is
obtained by product—due to independence assumptions—using the above mentioned component probability matrix and the actual fractions in the current system global state. In [9] a translation of PiFF to the
model specification language of FlyFast has also been presented which makes PiFF an additional front-

D. Latella & M. Massink

95

end for FlyFast extending its applicability to models of systems based on predicate-based interaction. In
the above mentioned paper, correctness of the translation has been proved as well. In particular, it has
been shown that the probabilistic semantics of any PiFF model are isomorphic to those of the translation
of the model. In other words, the transition probability matrix of (the DTMCs of) the two models is the
same. A companion translation of bounded PCTL formulas is also defined [9] and proven correct.
The notion of the outbox used in PiFF is reminiscent of the notion of the ether in PALOMA [14]
in the sense that the collection of all outboxes together can be thought of as a kind of ether; but such a
collection is intrinsically distributed among the components so that it cannot represent a bottleneck in
the execution of the system neither a singularity point in the deterministic approximation.
We are not aware of other proposals, apart from [9], of probabilistic process languages, equipped
both with standard, DTMC-based, semantics and with mean-field ones, that provide a predicate-based
interaction framework, and that are fully supported by a tool for probabilistic simulation, exact and
mean-field model-checking.
We conclude this section recalling that mean-field/fluid procedures are based on approximations of
the global behaviour of a system. Consequently, the techniques should be considered as complementary
to other, possibly more accurate but often not as scalable, analysis techniques for CAS, primarily those
based on stochastic simulation, such as statistical model-checking.
In this paper we present some details of PiFF, a translation to FlyFast which simplifies that proposed in [9] and an approach to model reduction based on probabilistic bisimulation for Inhomogeneous
DTMCs. In Section 2 we briefly present the main ingredients of the PiFF syntax and informal semantics,
and we recall those features of FlyFast directly relevant for understanding the translation of PiFF to the
FlyFast input language proposed in [9]. A revised and simplified version of the translation is described
in Section 3. In Section 4 we introduce a simplified language for the definition of transition-probabilities
in PiFF that allows us to define in Section 5 a model reduction procedure of the translation result, based
on a notion of bisimulation for the kind of IDTMCs of interest, introduced in Section 5 as well. An
example of application of the procedure is presented in Section 6. Some conclusions are drawn in Section 7. A formal proof of decidability of the cumulative probability test for state-space reduction based
on bisimulation is provided in the Appendix.

2

Summary on PiFF and FlyFast

In the following we present the main ingredients of PiFF and the features of FlyFast relevant for the
present paper.

2.1

PiFF

A PiFF system model specification ϒ = (∆ϒ , Fϒ , Σ0 )(N) is a triple where Fϒ is the set of relevant function
definitions (e.g. store updates, auxiliary constants and functions), ∆ϒ is a set of state defining equations,
and Σ0 is the initial system state (an N-tuple of component states, each of which being a 3-tuple (C, γ, O)
of agent state C, store γ and outbox O). We describe the relevant details below referring to [9] for the
formal definition probabilistic semantics of the language.
The PiFF type system consists of floating point values and operations, as in FlyFast, plus simple enumeration types for attributes, declared according to the syntax attype < name > enum < id − list >.
< id − list > is a finite list of identifiers. Of course, attributes can also take floating point values.
In Figure 1 the attribute type Space is defined that consists of four values A, B, C, D modelling four

Designing Attribute-based FlyFast

96

attype Space enum A, B, C, D;
..
.
const H = 0.6;
const L = 1 − H;
const Hdiv2 = H/2;
const Ldiv2 = L/2;
..
.
attribute loc : Space;
..
.
func Hr(x : Space) : Space; x endfunc;
func N(x : Space) : Space; case x of A : A; B : B; C : B; D : A endfunc;
func S(x : Space) : Space; case x of A : D; B : C; C : C; D : D endfunc;
func E(x : Space) : Space; case x of A : A; B : A; C : D; D : D endfunc;
func W(x : Space) : Space; case x of A : B; B : B; C : C; D : C endfunc;
..
.
func pHr(x : Space) : float; case x of A : H; B : L; C : H; D : L endfunc;
func pN(x : Space) : float; case x of A : 0; B : 0; C : Ldiv2; D : Hdiv2 endfunc;
func pS(x : Space) : float; case x of A : Ldiv2; B : Hdiv2; C : 0; D : 0 endfunc;
func pE(x : Space) : float; case x of A : 0; B : Hdiv2; C : Ldiv2; D : 0 endfunc;
func pW(x : Space) : float; case x of A : Ldiv2; B : 0; C : 0; D : Hdiv2 endfunc;
..
.
update Jump
my.loc := Hr(my.loc) with pHr(my.loc);
my.loc := N(my.loc) with pN(my.loc);
my.loc := S(my.loc) with pS(my.loc);
my.loc := E(my.loc) with pE(my.loc);
my.loc := W(my.loc) with pW(my.loc)
endupdate

Figure 1: A fragment of FSI .

D. Latella & M. Massink

97

locations. Some auxiliary constants are defined, using the const construct inherited from FlyFast:
const < name > = < value >.
A PiFF store update definition has the following syntax3 :
update upd
my.a1 := e11 , . . . , my.ak := ek1 with p1 ;
..
.
my.a1 := e1n , . . . , my.ak := ekn with pn
endupdate

where upd is the update name (unique within the system model specification), a1 , . . . , ak are the attribute names of the component, e11 , . . . , ekn and p1 , . . . , pn are attribute/store-probability expressions
respectively, with syntax defined according to the grammars e ::= va | ca | my.a | f na (e1 , . . . , em ) and
p ::= v p | c p | f n p (e1 , . . . , em ). In the above definition of attribute expressions va is an attribute value
(drawn from finite set V of attribute values), ca is an attribute constant in V defined using the const;
a ∈ {a1 , . . . , ak } is an attribute name and f na is an attribute function defined by the user in Fϒ , which,
when applied to attribute expressions e1 , . . . , em returns an attribute value; the syntax for such function
definitions afd is given below:
afd ::= func f na (x1 : T 1, . . . , xm : T m) : T ; afb endfunc
afb ::= e |case (x1 , . . . , xm ) of(va11 , . . . , vam1 ) : e1 ; (va12 , . . . , vam2 ) : e2 ; . . . (va1k , . . . , vamk ) : ek

where f na is the name of the attribute function, x1 : T 1, . . . , xm : T m are its parameters and their relative
types, T is the type of the result of f na ; e, ei are attribute-expressions and vai j are attribute-values.
In Figure 1 attribute functions N, S, E, W are defined for North, South, East, and West, such that Space
models the Cartesian space with four quadrants: A = N(D) = E(B), B = N(C) = W(A), and so on, as shown
diagrammatically in Figure 2 right. Function Hr is the identity on Space.
In the definition of store-probability expressions v p ∈ (0, 1], c p is a store-probability constant in (0, 1]
defined using the FlyFast const construct, and f n p is a store-probability function defined by the user
in Fϒ , which, when applied to attribute expressions e1 , . . . , em returns a probability value.The syntax for
store-probability function definitions pfd is similar to that of attribute functions:
pfd ::= func f n p (x1 : T 1, . . . , xm : T m) : float; pfb endfunc
pfb ::= p |case (x1 , . . . , xm ) of(va11 , . . . , vam1 ) : p1 ; (va12 , . . . , vam2 ) : p2 ; . . . (va1k , . . . , vamk ) : pk

where f n p is the name of the store-probability function, the result type is float (actually the range [0, 1])
x1 : T 1, . . . , xm : T m are its parameters and their relative types, p, pi are store-probability expressions and
vai j are attribute-values. In any store update definition it must be guaranteed that the values of p1 . . . pn
sum up4 to 1. The informal meaning is clear. The store update will make attributes a1 , . . . , ak take the
values of e1i , . . . , eki respectively with probability equal to the value of pi .
In Figure 1 store-probability functions pHr, pN, pS, pE, pW are defined that give the probabilities of
not moving (pHr), or of jumping to North (pN), South (pS), East (pE), West (pW), as functions of the
3 In

[9] a slightly different syntax for store updates has been used.
this version of the translation we allow only flat updates, i.e. the specific probability of each combination of values
assigned to the attributes must be given explicitly. Other possibilities could be defined using combinations of (independent)
probability distributions.
4 In

Designing Attribute-based FlyFast

98

S

:=

frc (I) :: inf∗ [⊥]hiJump.I +
frc (S) :: nsc∗ [⊥]hiJump.S

I

:=

ii :: inf∗ [⊥]hiJump.I +
ir :: rec∗ [⊥]hiJump.S

Figure 2: SI, a behavioural model.
current location.
Example 1 A simplified version of the behaviour of the epidemic process discussed in [9] is shown in
Figure 2 left5 . In Figure 1 we show a fragment of FSI defining store update Jump together with the relevant
type, constant and function definitions as introduced above. The component has just one attribute, named
loc, with values in Space. The effect of Jump executed by a component in which loc is bound to quadrant
` is to leave the value of loc unchanged with probability pHr(`), change it to the quadrant North of ` with
probability pN(`), and so on. Note that H > L and this implies that higher probability is assigned to A and
C and low probability to B and D. This is represented in Figure 2 right where higher probability locations
are shown in green and lower probability ones are shown in red; moreover, the relevant probabilities are
represented as arrows (H/2, L/2) or self-loops (H, L). A susceptible (state S) component becomes infected
(state I) via an inf action which takes place with probability equal to the fraction of components in the
system which are currently infected (i.e. frc(I)); it remains in state S via the self-loop labelled by action
nsc, with probability frc(S) = 1 − frc(I). An infected node (state I) may recover, entering state S with
action rec and probability ir; while infected, it keeps executing action inf, with probability ii. Note
that, for the sake of simplicity, we use only internal actions, modelled by means of output actions with
predicate false (⊥). We assume that in the initial global state all outboxes are non-empty; each contains
the initial store of the specific component (i.e., its initial location), predicate ⊥ and the empty tuple hi).
A PiFF state defining equation has the following (abstract) form: C := ∑ j∈J [g j ]p j :: act j .C j where either
[g j ]p j is the keyword rest or:
• g j is a boolean expression b which may depend on the current store, but not on the current occupancy measure vector: b ::= > | ⊥ | e ./ e | ¬b | b ∧ b and e ::= va | ca |my.a where > (⊥) denotes
the constant true (false), ./ ∈ {≥, >, ≤, <}, va is an attribute value (drawn from finite set V of
attribute values), ca is an attribute constant in V defined using the FlyFast const construct, and a
is the name of an attribute of the component.
• p j is a transition probability expression p ::= v p | c p | frc (C) | frc (π) | ∏i∈I pi | ∑i∈I pi | 1 − p, for
finite I, where v p ∈ (0, 1], c p a constant in (0, 1] defined via the const construct, and π is defined as
b above, but where expressions e can also be attribute names a (i.e. e ::= va | ca | my.a | a); frc (C)
is the fraction of components currently in state C over the total number N; similarly, frc (π) is the
fraction of components the current store of which satisfies π, over the total number N. Note that it
must be guaranteed that ∏i∈I pi ≤ 1 and ∑i∈I pi ≤ 1.
5 We focus only on those features that are most relevant for the present paper. In [9] also other features are shown like, e.g.
the use of (predicate-based) input actions, which are not the main subject of this paper.

D. Latella & M. Massink

99

• act j can be an output action α ∗ [π]hiσ or an input action α ∗ [π]()σ , where π is as above and σ is
the name of a store update. Note that in the case of an input action, π refers to the store of the
partner component in the previous step of the computation.
If [g j ]p j = rest, then act j must be an output action α ∗ [π]hiσ , to be executed with the residual probability.

2.2

FlyFast

FlyFast accepts a specification h∆, A, C0 i(N) of a model of a system consisting of the clock-synchronous
product of N instances of a probabilistic agent. The states of the DTMC-like agent model are specified
by a set of state-defining equations ∆. The (abstract) form of a state defining equation is the following
C := ∑ri=1 ai .Ci where ai ∈ A—the set of FlyFast actions—C,Ci ∈ S—the set of FlyFast states—and,
for i, j = 1, . . . , r ai 6= a j if i 6= j; note that Ci = C j with i 6= j is allowed instead6 . Each action has a
probability assigned by means of an action probability function definition in A of the form a :: exp where
exp is an expression consisting of constants and frc (C) terms. Constants are floating point values or
names associated to such values using the construct const < name > = < value >; frc (C) denotes the
element associated to state C in the current occupancy measure vector7 . So, strictly speaking, ∆ and A
characterise an inhomogeneous DTMC whose probability matrix K(m) is a function of the occupancy
measure vector m such that for each pair of states C,C0 , the matrix element K(m)C,C0 is the probability of
jumping from C to C0 given the current occupancy measure vector m. Letting S∆ be the set of states of the
agent, with |S∆ | = S, and U S = {(m1 , . . . , mS )|m1 + . . . + mS = 1} denote the unit simplex of dimension
S, we have K : U S × S∆ × S∆ → [0, 1]. Matrix K is generated directly from the input specification
h∆, A, C0 i(N) ; the reader interested in the details of how to derive K is referred to [27, 29]. Auxiliary
function definitions can be specified in A. The initial state C0 is a vector of size N consisting of the initial
state of each individual object. Finally, note that in matrix K(m) the information on specific actions is
lost, which is common in PCTL/DTMC based approaches; furthermore, we note that, by construction,
K(m) does not depend on N (see [27, 29] for details).

3

A revised translation

As in [9], we define a translation such that, given a PiFF system specification ϒ = (∆ϒ , Fϒ , Σ0 )(N) , the
translation returns the FlyFast system specification h∆, A, C0 i(N) preserving probabilistic semantics. The
predicate-based FlyFast front-end is then completed with a simple translation at the PCTL level, for
which we refer to [9].
The system model specification translation consists of two phases. In the first phase, each action
in the input system model specification ϒ is annotated with an identifier which is unique within the
specification. We let ℵ(ϒ) denote the resulting specification. These annotations will make action names
unique specification-wide thus eliminating complications which may arise from multiple occurrences
of the same action, in particular when leading to the same state (see [9] for details). Of course, these
annotations are disregarded in the probabilistic semantics, when considering the interaction model of
components. In other words, an output action αhi in outbox (γ, π, αhi) must match with any input
6 The

concrete FlyFast syntax is: state C{a 1.C 1 + a 2.C 2 ...a r.C r}.

7 The occupancy measure vector is a vector with as many elements as the number of states of an individual agent; the element

associated to a specific state gives the fraction of the subpopulation currently in that state over the size of the overall population.
The occupancy measure vector is a compact representation of the system global state.

Designing Attribute-based FlyFast

100

action α() even if αhi would actually correspond to (α, ι)∗ [π]hi and α() would actually correspond to
(α, η)∗ [π 0 ](). Apart from this detail, the probabilistic semantics as defined in [9] remain unchanged.
The second phase is defined by the translation algorithm defined in Figure 5, which is a revised and
simplified version of that presented in [9] and is applied to ℵ(ϒ). We let I (ℵ(ϒ)) denote the result of
the translation, namely the pure FlyFast system specification h∆, A, C0 i(N) .
We recall here some notation from [9]. We let S∆ϒ denote the set of states of ϒ; Γ∆ϒ is the set of
all stores defined over the attributes of ϒ—a store is a finite mapping from the attributes of the component to a finite set of values V , thus Γ∆ϒ is finite—and O∆ϒ the finite set of all outboxes of ϒ. A
ϒ component-state is a triple (C, γ, O) ∈ S∆ϒ × Γ∆ϒ × O∆ϒ = Ω∆ϒ . If the component-state is the target of a transition modelling the execution of an output action, then O = (γ 0 , π, αhi), where γ 0 is the
store of the (component-state) source of the transition, π is the predicate used in the action—actualised
with γ 0 —and αhi the actual message sent by the action. If, instead, the component-state is the target
of a transition for an input action, then O = hi, i.e. the empty outbox. Note that the set of component
states of ℵ(ϒ) is identical to that of ϒ. Also the set of all stores of ℵ(ϒ) is the same as that of ϒ.
In the algorithm of Figure 5 by t ∗ t 0 we mean the syntactical term representing the product of terms
t and t 0 ; the notation is extended to PROD{t|cond(t)}, denoting the syntactical product t1 ∗ . . . ∗ tn if
{t|cond(t) = tt} = {t1 , . . . ,tn } 6= 0/ and 1 otherwise. Similarly, SUM{t|cond(t)} denotes the syntactical
sum t1 + . . . + tn if {t|cond(t) = tt} = {t1 , . . . ,tn } 6= 0/ and 0 otherwise. The translation algorithm uses a
few auxiliary functions which we briefly discuss below:
• IS : Ω∆ϒ → S is a total injection which maps every component state of ℵ(ϒ) to a distinct state
of I (ℵ(ϒ)); we recall that S denotes the set of state names of FlyFast models.
• IA : (S∆ϒ × Γ∆ϒ ) × (Λ∆ϒ × Iℵ ) × Ω∆ϒ → A is a total injection where, as in [9], Λ∆ϒ is the set of
action labels of ϒ and Iℵ is the set of unique identifiers used in the first phase of the translation.
We recall that A is the set of action names of FlyFast. The mapping of actions is a bit more
delicate because we have to respect FlyFast static constraints and, in particular, we have to avoid
multiple probability function definitions for the same action. A first source of potential violations
(i.e. multiple syntactical occurrences of the same action) has been removed by action annotation in
the first phase of the translation. A second source is the fact that the same action can take place in
different contexts (for example with different stores) or leading to different target component states
(maybe with different probabilities). To that purpose, we could distinguish different occurrences
of the same action in different transitions, each characterised by its source component-state and its
target component-state in Ω∆ϒ . In practice, since an action of a component cannot be influenced
by the current outbox of the component, it is sufficient to restrict the first component of the domain
from Ω∆ϒ to (S∆ϒ × Γ∆ϒ ).
• The interpretation functions defined in Figure 3, namely those depending on stores only (and not
on occupancy measure vectors); we assume EL [[·]]γ extended to EL [[ f n]]γ for defined function f n,
in the standard way. In Figure 3 βϒ denotes the constant to value bindings generated by the const
construct in the input model specification ϒ, whereas store update upd is defined as above.
• The translation function IP for transition probability expressions p j , defined in Figure 4.
Output actions are dealt with in step 1 of the algorithm of Figure 5. Let us consider, for example,
(inf, 1)∗ [⊥]hiJump in the definition of state S in Figure 2 (assuming annotations are integer values and
the action has been annotated with 1). We know that the possible values for locations are A,B,C,D,
so that the set of all stores is {loc} → {A,B,C,D}. The algorithm generates 12 actions8 . Let us focus
8 Diagonal

jumps are not contemplated in the model; technically this comes from the actual probability values used in the

D. Latella & M. Massink

101

EL [[>]]γ
= tt
EL [[⊥]]γ
= ff
EL [[e1 ./ e2 ]]γ
= EL [[e1 ]]γ ./ EL [[e2 ]]γ
EL [[¬b]]γ
= ¬EL [[b]]γ
EL [[b1 ∧ b2 ]]γ = EL [[b1 ]]γ ∧ EL [[b2 ]]γ
EL [[va ]]γ
= va
EL [[ca ]]γ
= βϒ (ca )
EL [[v p ]]γ
= vp
EL [[c p ]]γ
= βϒ (c p )
EL [[a]]γ
= a
EL [[my.a]]γ
= γ(a)
EL [[ f na (e1 , . . . , em )]]γ = EL [[ f na ]]γ (EL [[e1 ]]γ , . . . , EL [[em ]]γ )
EL [[ f n p (e1 , . . . , em )]]γ = EL [[ f n p ]]γ (EL [[e1 ]]γ , . . . , EL [[em ]]γ )
EU [[upd]]γ

= λ γ 0 .dom(γ 0 ) 6= {a1 , . . . , ak } → 0;
γ 0 (a1 ) = EL [[e11 ]]γ ∧ . . . ∧ γ 0 (ak ) = EL [[ek1 ]]γ → EL [[p1 ]]γ ;
..
.

ER [[>]]γ
ER [[⊥]]γ
ER [[e1 ./ e2 ]]γ
ER [[¬b]]γ
ER [[b1 ∧ b2 ]]γ
ER [[va ]]γ
ER [[ca ]]γ
ER [[a]]γ

=
=
=
=
=
=
=
=

γ 0 (a1 ) = EL [[e1n ]]γ ∧ . . . ∧ γ 0 (ak ) = EL [[ekn ]]γ → EL [[pn ]]γ ;
otherwise → 0
tt
ff
ER [[e1 ]]γ ./ ER [[e2 ]]γ
¬ER [[b]]γ
ER [[b1 ]]γ ∧ ER [[b2 ]]γ
va
βϒ (ca )
γ(a)
Figure 3: Interpretation functions relevant for the translation

on the action ξ associated to local position A (i.e. γ = [loc 7→ A]) and possible next position B (i.e.
γ 0 = [loc 7→ B]); the algorithm will generate the FlyFast probability function definition ξ :: pW(A) ∗
(frc (I1) + . . . + frc (In))9 as well as a transition leading to (a state which is the encoding, via IS , of)
the component state with I as (proper) state, store γ 0 , and outbox (γ, ⊥, infhi). Since the action is not
depending on the current outbox, in practice a copy of such a transition is generated for each component
state sharing the same proper state S and the same store γ. The translation scheme for input actions
is defined in case 2 and is similar, except that one has also to consider the sum of the fractions of the
possible partners. The translation of the rest case is straightforward. Note that for every ζ :: r ∗ q ∈ Aγ ,
r is a probability value associated to a store update; since any store update characterizes a probability
distribution over stores, assuming the range of such a distribution is {r1 , . . . , rn } if ζi :: ri ∗ q ∈ Aγ , then
also ζ j :: r j ∗ q ∈ Aγ for all j = 1, . . . , n, j 6= i with ∑ni=1 r j = 1. Thus the remaining probability is
qγ = (1 − SUM{q|ζ :: r ∗ q ∈ Aγ }), where q is either a term IP (p j )γ , with p j occurring in a summand of
the state defining equation (see step 1), or a term IP (p j )γ ∗ SUM{frc (IS (Σ))| . . .} (see step 2). It worth
definition of Jump.
9 Here we assume that I ({(C, γ, O) ∈ Ω |C = I}) = {I1, . . . , In} ⊂ S .
∆ϒ
S

Designing Attribute-based FlyFast

102
IP (v p )γ
IP (c p )γ
IP (frc (C))γ
IP (frc (π))γ
IP (∏i∈I pi )γ
IP (∑i∈I pi )γ

=
=
=
=
=
=

vp
βϒ (c p )
SUM{frc (IS ((C0 , γ 0 , O0 ))) | (C0 , γ 0 , O0 ) ∈ Ω∆ϒ and C0 = C}
SUM{frc (IS ((C0 , γ 0 , O0 ))) | (C0 , γ 0 , O0 ) ∈ Ω∆ϒ and ER [[EL [[π]]γ ]]γ 0 = tt}
PROD{IP (pi )γ | i ∈ I}
SUM{IP (pi )γ | i ∈ I}

Figure 4: Transition probability expressions translation function definition
For each state equation C := ∑ j∈J [g j ]p j :: act j .C j in ∆ϒ :
1. For each output action (α, ι)∗ [π]hiσ = actk with k ∈ J and [gk ]pk 6= rest,
for each γ ∈ Γ∆ϒ s.t. EL [[gk ]]γ = tt and (C, γ, O) ∈ Ω∆ϒ for some O ∈ O∆ϒ , for each γ 0 ∈ Γ∆ϒ s.t. (Ck , γ 0 , (γ, EL [[π]]γ , αhi)) ∈ Ω∆ϒ and
EU [[σ ]]γ (γ 0 ) > 0, let ξ = IA ((C, γ), (αhi, ι), (Ck , γ 0 , (γ, EL [[π]]γ , αhi))) be a fresh new action in the FlyFast model specification
I (ℵ(ϒ)) = h∆, A, C0 i(N) and add the following action probability function definition in A: ξ :: EU [[σ ]]γ (γ 0 ) ∗ IP (pk )γ .
Moreover, for each outbox O ∈ O∆ϒ s.t. (C, γ, O) ∈ Ω∆ϒ , the following summand is added to the equation in ∆ for state
IS ((C, γ, O)): ξ . IS ((Ck , γ 0 , (γ, EL [[π]]γ , αhi)));
2. For each input action (α, ι)∗ [π]()σ = actk , with k ∈ J and [gk ]pk 6= rest,
for each γ ∈ Γ∆ϒ s.t. EL [[gk ]]γ = tt and (C, γ, O) ∈ Ω∆ϒ for some O ∈ O∆ϒ , for each γ 0 ∈ Γ∆ϒ s.t. (Ck , γ 0 , hi) ∈ Ω∆ϒ and
EU [[σ ]]γ (γ 0 ) > 0,
let ξ = IA ((C, γ), (α(), ι), (Ck , γ 0 , hi)), be a fresh new action in the FlyFast model specification I (ℵ(ϒ)) = h∆, A, C0 i(N) and
add the following action probability function definition in A:
ξ :: EU [[σ ]]γ (γ 0 ) ∗ IP (pk )γ ∗
∗SUM{frc (IS (Σ))|Σ = (C00 , γ 00 , (γ, π, αhi)) ∈ Ω∆ϒ ∧
∧ ER [[π]]γ = ER [[EL [[π]]γ ]]γ = tt}.
Moreover, for each outbox O ∈ O∆ϒ s.t. (C, γ, O) ∈ Ω∆ϒ , the following summand is added to the equation in ∆ for state
IS ((C, γ, O)): ξ . IS ((Ck , γ 0 , hi));
3. If there exists k ∈ J s.t. [gk ]pk = rest, and actk = (α, ι)∗ [π]hiσ , for each γ ∈ Γ∆ϒ s.t. (C, γ, O) ∈ Ω∆ϒ for some O ∈
O∆ϒ , let Aγ be the set of probability function definitions which has been constructed in steps (1) and (2) above. Let
qγ be defined by qγ = (1 − SUM{q|ζ :: r ∗ q ∈ Aγ }). For all γ 0 ∈ Γ∆ϒ s.t. (Ck , γ 0 , (γ, EL [[π]]γ , αhi)) ∈ Ω∆ϒ , let ξ =
IA ((C, γ), (α, ι)hi, (Ck , γ 0 , (γ, EL [[π]]γ , αhi))) ∈ Ω∆ϒ , be a fresh new action in the FlyFast model specification I (ℵ(ϒ)) =
h∆, A, C0 i(N) and add the following action probability function definition in A: ξ :: EU [[σ ]]γ (γ 0 ) ∗ qγ .
Moreover, for each outbox O ∈ O∆ϒ s.t. (C, γ, O) ∈ Ω∆ϒ , the following summand is added to the equation in ∆ for state
IS ((C, γ, O)): ξ . IS ((Ck , γ 0 , (γ, EL [[π]]γ , αhi)));
4. No other action probability function definition and transition is included and the initial state C0 of I (ϒ) is defined as C0 =
IS (Σ0 ).

Figure 5: The translation algorithm
pointing out here that the translation of Figure 5 is essentially the same as that presented in [9], when the
latter is applied to the sublanguage of PiFF where one requires that each action occurs at most once. The
annotations performed in the first phase of the translation ensure that this requirement is fulfilled; as we
noted above, these annotations are purely syntactical and are disregarded at the semantics level. We also
recall that in probabilistic, pure DTMC process language semantics, actions are in the end dropped and,
for each pair of states, the cumulative probability of such actions is assigned to the single transition from
one of the states to the other one. Consequently, correctness of the translation, proved in [9], is preserved
by the simplified version presented in this paper.
We note that in the algorithm sets Ω∆ϒ , Γ∆ϒ and O∆ϒ are used. Of course, an alternative approach
could be one which considers only the set Ω∆ϒ of component states which are reachable from a given
initial component state and, consequently, the sets Γ∆ϒ and O∆ϒ of used stores and outboxes. In this way,
the size of the resulting FlyFast model specification would be smaller (for example in terms of number of

D. Latella & M. Massink

103

states). On the other hand, this approach might require recompilation for each model-checking session
starting from a different initial component state.

4

A simplified language for Bisimulation-based optimisation

In this section we consider a simplified language for transition probability expressions appearing in
state defining equations that will allow us to perform bisimulation based optimisation of the result
h∆, A, C0 i(N) . The restricted syntax for transition probability expressions p we use in this section is
the following: p ::= e p | e p · frc (C) | e p · frc (π) and e p ::= v p | c p where v p and c p and π are defined as in
Section 2.
By inspection of the FlyFast translation as defined in Section 3, and recalling that the set S∆ of the
states of the resulting FlyFast model, ranged over by z, zi , . . ., has cardinality S, it is easy to see that the
probability action definition in the result of a translation of a generic output action is either of the form
ξ :: k, or it is of the form ξ :: k ∗ SUM{frc (zi )|i ∈ I} where k is a FlyFast constant. Moreover, if p was
of the form e p · frc (C), then index set I ⊆ {1, . . . , S} identifies those states in S∆ that represent (via IS )
component states with proper local state C; if instead, p was of the form e p · frc (π), then I ⊆ {1, . . . , S}
identifies those states in S∆ that represent (via IS ) component states with a store satisfying π in the
relevant store. At the FlyFast semantics level, recalling that frc (zi ) is exactly the i-th component mi of the
occupancy measure vector m = (m1 , . . . , mS ) of the model, we can rewrite10 the above as k or k · ∑i∈I mi .
Similarly, the probability action definition in the result of a translation of a generic
 input action
∗
0
0
(α, ι) [π ]() (executed in local store γ ) will necessarily be of the form k · ∑ j∈I 0 m j or of the form
k · ∑ j∈I m j · ∑ j∈I 0 m j , for index sets I as above and I 0 as follows:
I 0 = {i ∈ {1, . . . , S}|∃C, γ, γ, π, s.t.
zi = IS ((C, γ, (γ, π, αhi))) ∧ ER [[π]]γ 0 = ER [[EL [[π 0 ]]γ 0 ]]γ = tt}
An immediate consequence of using the above mentioned restricted syntax for the probability function definitions is that, letting K : U S ×S ×S → [0, 1] be the transition probability matrix for the FlyFast
translation of a model specification, we have that K(m1 , . . . , mS )z,z0 is a polynomial function of degree at
most 2 in variables m1 , . . . , mS .

5

Bisimilarity and State-space Reduction

The following definition generalises standard probabilistic bisimilarity for state labelled DTMCs to the
case in which transition probabilities are functions instead of constant values.
Definition 1 For finite set of states S, with |S| = S, let K : U S × S × S → [0, 1] and, for z ∈ S and
Q ⊆ S, write K(m)z,Q for ∑z0 ∈Q K(m)z,z0 . Let furthermore L : S → 2AP be a state-labelling function,
for a given set AP of atomic propositions. An equivalence relation R ⊆ S × S is called a bisimulation
relation if and only if z1 R z2 implies: (i) L (z1 ) = L (z2 ) and (ii) K(m)z1 ,Q = K(m)z2 ,Q , for all m ∈ U S
and Q ∈ S/R. The bisimulation equivalence on S is the largest bisimulation relation R ⊆ S × S.
We point out that the notion of bisimilarity does not introduce any approximation, and consequently error,
in a model and related analyses. Bisimilarity is only a way for abstracting from details that are irrelevant
10 With

a little notational abuse using k also as the actual value in [0, 1] of the FlyFast constant k.

Designing Attribute-based FlyFast

104
l

h

H

L

H
L

Figure 6: SI in two quadrants

for the specific analyses of interest. In particular, it is useful to remark that bisimilarity preserves also
state labels, which are directly related to the atomic propositions of logic formulas for which modelchecking is performed. Actually, it is well known that probabilistic bisimilarity coincides with PCTL
equivalence, i.e. the equivalence induced on system states by their satisfaction of PCTL formulas, for
finitely branching systems [3].
Note that K(m1 , . . . , mS )z1 ,Q = K(m1 , . . . , mS )z2 ,Q for all (m1 , . . . , mS ) ∈ U S is in general not decidable. If instead we consider only transition probability matrices as in Section 4, we see that each side
of the above equality is a polynomial function of degree at most 2 in variables m1 , . . . , mS and one can
define a normal form for the polynomial expressions in m1 , . . . , mS supported by an ordering relationon
the variable names (e.g. m1 ≺ . . . ≺ mS ) and get expressions of the general form ∑Si=1 ∑Sj≥i hi j · mi · m j +

hi j , hi , h. Actually, such expressions can always be rewritten in the form
∑Si=1 hi · mi + h for suitable

ui j · mi · m j + u for suitable ui j , u since, recalling that ∑Si=1 mi = 1, we get ∑Si=1 hi · mi =
∑Si=1 ∑Sj≥i


S
an expression of the following
∑Si=1 m
i · ∑i=1 hi · mi which,
 by simple algebraic manipulation, yields

S
S
S
S
0
form: ∑i=1 ∑ j≥i ui j · mi · m j ; finally, we get ∑i=1 ∑ j≥i ui j · mi · m j + u by letting ui j = hi j + u0i j and
u = h. The following proposition thus establishes decidability of K(m1 , . . . , mS )z1 ,Q = K(m1 , . . . , mS )z2 ,Q
for all (m1 , . . . , mS ) ∈ U S for transition probability matrices as in Section 4:

Proposition 1


Let A(m1 , . . . , mS ) = ∑Si=1 ∑Sj≥i ai j · mi · m j + a and B(m1 , . . . , mS ) = ∑Si=1 ∑Sj≥i bi j · mi · m j + b with
ai j , bi j , a, b ∈ R, where m1 , . . . , mS are variables taking values over R≥0 with ∑Si=1 mi = 1. The following
holds: (∀m1 , . . . , mS .A(m1 , . . . , mS ) = B(m1 , . . . , mS )) ⇔ ((∀i, j = 1, . . . , S with i ≤ j.ai j = bi j ) ∧ a = b).

The above results can be used for reduction of the state-space of the individual agent, i.e. the resulting
FlyFast model specification, after the application of the translation described in Section 3, by using for
instance the standard probabilistic relational coarsest set partition problem algorithm (see e.g. [22], page
227) with slight obvious modifications due to the presence of state-labels and the need of symbolic
computation capabilities required for checking (degree 2) polynomial expressions equality.11 It is worth
mentioning that state aggregation via bisimilarity is effective only if there is some sort of compatibility
between (i) state labelling—and, consequently, the specific PCTL atomic propositions one uses—and
(ii) the way probabilities are assigned to transitions—and, consequently, the cumulative probabilities to
equivalence classes. We will come back on this issue in the following section.

D. Latella & M. Massink

SA
SB
SC
SD
IA
IB
IC
ID

SA
HφS (m)
H
2 φS (m)
0
H
2 φS (m)
Hir
H
2 ir
0
H
2 ir

105
SB
L
2 φS (m)
LφS (m)
L
2 φS (m)

0
L
2 ir

Lir
L
2 ir
0

SC
0
H
2 φS (m)
HφS (m)
H
2 φS (m)
0
H
2 ir
Hir
H
2 ir

SD
L
2 φS (m)

0
L
2 φS (m)
LφS (m)
L
2 ir

0
L
2 ir

Lir

IA
HφI (m)
H
2 φI (m)
0
H
2 φI (m)
Hii
H
2 ii
0
H
2 ii

IB
L
2 φI (m)
LφI (m)
L
2 φI (m)

0
L
2 ii

Lii
L
2 ii
0

IC
0
H
2 φI (m)
HφI (m)
H
2 φI (m)
0
H
2 ii
Hii
H
2 ii

ID
L
2 φI (m)

0
L
2 φI (m)
LφI (m)
L
2 ii

0
L
2 ii

Lii

Figure 7: IDTMC transition probability matrix K(m), for m in U 8 .

6

Example

The application of the translation to the specification of Example 1 generates an agent model with 8
states, say S∆ = {SA, SB, SC, SD, IA, IB, IC, ID}12 with associated IDTMC probability transition matrix
as shown in Figure 7 where mxy represents the fraction of objects currently in state xy for x ∈ {S, I} and
y ∈ {A, B,C, D}—i.e. the components in state x and with loc = y in the original specification of Fig 2—so
that m = (mSA , mSB , mSC , mSD , mIA , mIB , mIC , mID ) is the occupancy measure vector. In Figure 7, functions
φS and φI are used as abbreviations in the obvious way: φS (m) = mSA + mSB + mSC + mSD and φI (m) =
mIA + mIB + mIC + mID . Let us assume now that we are interested in checking PCTL formulas on the
model of Fig 2 which distinguish components located in A or C from those located in B or D, and
those in state S from those in state I, that is we consider atomic propositions Sh, Ih, Sl and Il and a
labelling L such that L (SA) = L (SC) = {Sh}, L (IA) = L (IC) = {Ih}, L (SB) = L (SD) = {Sl},
and L (IB) = L (ID) = {Il}.
Consider relation R on S∆ defined as R = IS∆ ∪ {(SA, SC), (SB, SD), (IA, IC), (IB, ID)} ∪ {(SC, SA),
(SD, SB), (IC, IA), (ID, IB)} where IS∆ is the identity relation on S∆ . It is very easy to show that R is
a bisimulation according to Definition 1. Clearly R is an equivalence relation and its quotient S∆ /R
is the set {QSh , QSl , QIh , QIl } with QSh = {SA, SC}, QSl = {SB, SD}, QIh = {IA, IC}, QIl = {IB, ID}. In
addition, for all z1 , z2 ∈ S∆ , whenever z1 R z2 , we have L (z1 ) = L (z2 ) and K(m)z1 ,Q = K(m)z2 ,Q for all
Q ∈ S∆ /R and for all m, as one can easily check; clearly, R is also the largest bisimulation relation on S∆ .
The relationship between the two occupancy measure vectors is: mQSh = mSA + mSC , mQSl = mSB + mSD ,
mQIh = mIA + mIC , and mQIl = mIB + mID . We can thus use the reduced IDTMC defined by matrix
b given
b Q , mQ , mQ , mQ ) shown in Figure 9. It corresponds to the FlyFast agent specification ∆
K(m
Sh
Sl
Ih
Il
in Figure 8. In a sense, the high probability locations A and C, in the new model, have collapsed into a
single one, namely h and the low probability ones (B and D) have collapsed into l, as shown in Figure 6.
We point out again the correspondence between the symmetry in the space jump probability on one side
and the definition of the state labelling function on the other side. Finally, note that a coarser labelling
like, e.g. L 0 (SA) = L 0 (SC) = L 0 (IA) = L 0 (IC) = {h}, L 0 (SB) = L 0 (SD) = L 0 (IB) = L 0 (ID) = {l}
would make the model collapse into one with only two states, Qh and Ql , with probabilities H : Qh →
Qh , H : Ql → Qh , L : Qh → Ql and L : Qh → Ql where only the location would be modelled whereas
11 For

instance, on page 227 of [22], line 12, v(x, S) = v(y, S) should be replaced with L(x) = L(y) ∧ v(x, S) = v(y, S) and in
line 13, v(x, S) 6= v(y, S) should be replaced with L(x) 6= L(y) ∨ v(x, S) 6= v(y, S), in order to take state labels into consideration
as well. Of course v(x, S) (L, respectively)is to be intended as K(m)z,Q (L , respectively), using the notation we introduced
above for Bisimilarity.
12 Actually the agent resulting from the translation of Figure 5 has a higher number of states due to the different possibilities
for outbox values. Many of these states are unreachable from the initial state since the agent has no input action and we assume
an initial unreachable state pruning has been performed.

Designing Attribute-based FlyFast

106
action
action
action
action

QSh_inf_QIh:
QSh_inf_QIl:
QSl_inf_QIh:
QSl_inf_QIl:

H*(frc(QIh)+frc(QIl));
L*(frc(QIh)+frc(QIl));
H*(frc(QIh)+frc(QIl));
L*(frc(QIh)+frc(QIl));

action
action
action
action

QSh_nsc_QSh:
QSh_nsc_QSl:
QSl_nsc_QSh:
QSl_nsc_QSl:

H*(frc(QSh)+frc(QSl));
L*(frc(QSh)+frc(QSl));
H*(frc(QSh)+frc(QSl));
L*(frc(QSh)+frc(QSl));

action
action
action
action

QIh_inf_QIh:
QIh_inf_QIl:
QIl_inf_QIh:
QIl_inf_QIl:

H*ii;
L*ii;
H*ii;
L*ii;

action
action
action
action

QIh_rec_QSh:
QIh_rec_QSl:
QIl_rec_QSh:
QIl_rec_QSl:

H*ir;
L*ir;
H*ir;
L*ir;

state
state
state
state

QSh{QSh_inf_QIh.QIh
QSl{QSl_inf_QIh.QIh
QIh{QIh_inf_QIh.QIh
QIl{QIl_inf_QIh.QIh

+
+
+
+

QSh_inf_QIl.QIl
QSl_inf_QIl.QIl
QIh_inf_QIl.QIl
QIl_inf_QIl.QIl

+
+
+
+

QSh_nsc_QSh.QSh
QSl_nsc_QSh.QSh
QIh_rec_QSh.QSh
QIl_rec_QSh.QSh

+ QSh_nsc_QSl.QSl}
+ QSl_nsc_QSl.QSl}
+ QIh_rec_QSl.QSl}
+QIl_rec_QSl.QSl}

b
Figure 8: Reduced agent specification ∆
QSh
QSl
QIh
QIl

QSh
H · (mQSh + mQSl )
H · (mQSh + mQSl )
H · ir
H · ir

QSl
L · (mQSh + mQSl )
L · (mQSh + mQSl )
L · ir
L · ir

QIh
H · (mQIh + mQIl )
H · (mQIh + mQIl )
H · ii
H · ii

QIl
L · (mQIh + mQIl )
L · (mQIh + mQIl )
L · ii
L · ii

b
Figure 9: IDTMC transition probability matrix function K(m),
for m in U 4 .
information on the infection status would be lost.

7

Conclusions

PiFF [9] is a language for a predicate-based front-end of FlyFast, an on-the-fly mean-field modelchecking tool. In this paper we presented a simplified version of the translation proposed in [9] together
with an approach for model reduction that can be applied to the result of the translation. The approach
is based on probabilistic bisimilarity for inhomogeneous DTMCs. An example of application of the procedure has been shown. The implementation of a compiler for PiFF mapping the language to FlyFast
is under development as an add-on of FlyFast. We plan to apply the resulting extended tool to more as
well as more complex models, in order to get concrete insights on the practical applicability of the framework and on the actual limitations imposed by the restrictions necessary for exploiting bisimilarity-based
state-space reduction. Investigating possible ways of relaxing some of such restrictions will also be an
interesting line of research.
Acknowledgments Research partially funded by EU Project n. 600708 A Quantitative Approach to Management and Design of Collective and Adaptive Behaviours (QUANTICOL).

References
[1] Adnan Aziz, Kumud Sanwal, Vigyan Singhal & Robert K. Brayton (2000): Model-checking continous-time
Markov chains. ACM Trans. Comput. Log. 1(1), pp. 162–170, doi:10.1145/343369.343402.
[2] Christel Baier, Boudewijn R. Haverkort, Holger Hermanns & Joost-Pieter Katoen (2003): Model-Checking
Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng. 29(6), pp. 524–541,
doi:10.1109/TSE.2003.1205180.

D. Latella & M. Massink

107

[3] Christel Baier & Joost-Pieter Katoen (2008): Principles of model checking. MIT Press.
[4] Girish Bhat, Rance Cleaveland & Orna Grumberg (1995): Efficient On-the-Fly Model Checking for CTL*.
In: Proceedings, 10th Annual IEEE Symposium on Logic in Computer Science, San Diego, California, USA,
June 26-29, 1995, IEEE Computer Society, pp. 388–397, doi:10.1109/LICS.1995.523273.
[5] L. Bortolussi, G. Cabri, G. Di Marzo Serugendo, V. Galpin, J. Hillston, R. Lanciani, M. Massink & D. Tribastone, M. Weyns (2015): Verification of CAS. In J. Hillston, J. Pitt, M. Wirsing & F. Zambonelli, editors: Collective Adaptive Systems: Qualitative and Quantitative Modelling and Analysis, Schloss Dagstuhl Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany, pp. 91–102. Dagstuhl Reports. Vol. 4, Issue
12. Report from Dagstuhl Seminar 14512. ISSN 2192-5283.
[6] Luca Bortolussi & Jane Hillston (2012): Fluid Model Checking. In Maciej Koutny & Irek Ulidowski, editors:
CONCUR 2012 - Concurrency Theory - 23rd International Conference, CONCUR 2012, Newcastle upon
Tyne, UK, September 4-7, 2012. Proceedings, Lecture Notes in Computer Science 7454, Springer, pp. 333–
347, doi:10.1007/978-3-642-32940-1 24.
[7] Luca Bortolussi & Jane Hillston (2015): Model checking single agent behaviours by fluid approximation. Inf.
Comput. 242, pp. 183–226, doi:10.1016/j.ic.2015.03.002.
[8] Jean-Yves Le Boudec, David D. McDonald & Jochen Mundinger (2007): A Generic Mean Field Convergence
Result for Systems of Interacting Objects. In: Fourth International Conference on the Quantitative Evaluaiton
of Systems (QEST 2007), 17-19 September 2007, Edinburgh, Scotland, UK, IEEE Computer Society, pp.
3–18, doi:10.1109/QEST.2007.8.
[9] Vincenzo Ciancia, Diego Latella & Mieke Massink (2016): On-the-Fly Mean-Field Model-Checking for
Attribute-Based Coordination. In Alberto Lluch-Lafuente & José Proença, editors: Coordination Models
and Languages - 18th IFIP WG 6.1 International Conference, COORDINATION 2016, Held as Part of the
11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Heraklion,
Crete, Greece, June 6-9, 2016, Proceedings, Lecture Notes in Computer Science 9686, Springer, pp. 67–83,
doi:10.1007/978-3-319-39519-7 5.
[10] Costas Courcoubetis, Moshe Y. Vardi, Pierre Wolper & Mihalis Yannakakis (1992): Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design 1(2/3), pp. 275–288,
doi:10.1007/BF00121128.
[11] R.W.R. Darling & J.R. Norris (2008): Differential equation approximations for Markov chains. Probability
Surveys 5, pp. 37–79, doi:10.1214/07-PS121.
[12] Rocco De Nicola, Diego Latella, Alberto Lluch-Lafuente, Michele Loreti, Andrea Margheri, Mieke Massink,
Andrea Morichetta, Rosario Pugliese, Francesco Tiezzi & Andrea Vandin (2015): The SCEL Language:
Design, Implementation, Verification. In Martin Wirsing, Matthias M. Hölzl, Nora Koch & Philip Mayer,
editors: Software Engineering for Collective Autonomic Systems - The ASCENS Approach, Lecture Notes
in Computer Science 8998, Springer, pp. 3–71, doi:10.1007/978-3-319-16310-9 1.
[13] Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci & Marisa Venturini Zilli (2004):
Bounded Probabilistic Model Checking with the Muralpha Verifier. In Alan J. Hu & Andrew K. Martin,
editors: Formal Methods in Computer-Aided Design, 5th International Conference, FMCAD 2004, Austin,
Texas, USA, November 15-17, 2004, Proceedings, Lecture Notes in Computer Science 3312, Springer, pp.
214–229, doi:10.1007/978-3-540-30494-4 16.
[14] Cheng Feng & Jane Hillston (2014): PALOMA: A Process Algebra for Located Markovian Agents. In Gethin
Norman & William H. Sanders, editors: Quantitative Evaluation of Systems - 11th International Conference,
QEST 2014, Florence, Italy, September 8-10, 2014. Proceedings, Lecture Notes in Computer Science 8657,
Springer, pp. 265–280, doi:10.1007/978-3-319-10696-0 22.
[15] Nicolas Gast & Bruno Gaujal (2010): A mean field model of work stealing in large-scale systems. In Vishal
Misra, Paul Barford & Mark S. Squillante, editors: SIGMETRICS 2010, Proceedings of the 2010 ACM
SIGMETRICS International Conference on Measurement and Modeling of Computer Systems, New York,
New York, USA, 14-18 June 2010, ACM, pp. 13–24, doi:10.1145/1811039.1811042.

108

Designing Attribute-based FlyFast

[16] Stefania Gnesi & Franco Mazzanti (2011): An Abstract, on the Fly Framework for the Verification of ServiceOriented Systems. In Martin Wirsing & Matthias M. Hölzl, editors: Rigorous Software Engineering for
Service-Oriented Systems - Results of the SENSORIA Project on Software Engineering for Service-Oriented
Computing, Lecture Notes in Computer Science 6582, Springer, pp. 390–407, doi:10.1007/978-3-642-204012 18.
[17] Guillaume Guirado, Thomas Hérault, Richard Lassaigne & Sylvain Peyronnet (2006): Distribution, Approximation and Probabilistic Model Checking. Electr. Notes Theor. Comput. Sci. 135(2), pp. 19–30,
doi:10.1016/j.entcs.2005.10.016.
[18] Ernst Moritz Hahn, Holger Hermanns, Björn Wachter & Lijun Zhang (2009): INFAMY: An Infinite-State
Markov Model Checker. In Ahmed Bouajjani & Oded Maler, editors: Computer Aided Verification, 21st
International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Lecture Notes
in Computer Science 5643, Springer, pp. 641–647, doi:10.1007/978-3-642-02658-4 49.
[19] Hans Hansson & Bengt Jonsson (1994): A Logic for Reasoning about Time and Reliability. Formal Asp.
Comput. 6(5), pp. 512–535, doi:10.1007/BF01211866.
[20] Thomas Hérault, Richard Lassaigne, Frédéric Magniette & Sylvain Peyronnet (2004): Approximate Probabilistic Model Checking. In Bernhard Steffen & Giorgio Levi, editors: Verification, Model Checking, and
Abstract Interpretation, 5th International Conference, VMCAI 2004, Venice, January 11-13, 2004, Proceedings, Lecture Notes in Computer Science 2937, Springer, pp. 73–84, doi:10.1007/978-3-540-24622-0 8.
[21] Gerard J. Holzmann (2004): The SPIN Model Checker - primer and reference manual. Addison-Wesley.
[22] D. Huynh & L. Tian (1992): On some equivalence relations for probabilistic processes. Fundamenta Informaticae 17, pp. 211–234.
[23] A. Kolesnichenko, A. Remke & P.-T. de Boer (2012): A logic for model-checking of mean-field models.
Technical Report TR-CTIT-12-11, http://doc.utwente.nl/80267/.
[24] Anna Kolesnichenko, Pieter-Tjerk de Boer, Anne Remke & Boudewijn R. Haverkort (2013): A logic for
model-checking mean-field models. In: 2013 43rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Budapest, Hungary, June 24-27, 2013, IEEE Computer Society, pp. 1–12,
doi:10.1109/DSN.2013.6575345.
[25] Kim G. Larsen & Axel Legay (2016): Statistical Model Checking: Past, Present, and Future. In Tiziana Margaria & Bernhard Steffen, editors: Leveraging Applications of Formal Methods, Verification and Validation:
Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October
10-14, 2016, Proceedings, Part I, Lecture Notes in Computer Science 9952, pp. 3–15, doi:10.1007/978-3319-47166-2 1.
[26] D. Latella (1983): Comunicazione basata su proprietà nei sistemi decentralizzati. [Property-based interprocess communication in decentralized systems] Graduation Thesis. Istituto di Scienze dell’Informazione.
Univ. of Pisa, Italy (in italian).
[27] Diego Latella, Michele Loreti & Mieke Massink (2013): On-the-fly Fast Mean-Field Model-Checking. In
Martı́n Abadi & Alberto Lluch-Lafuente, editors: Trustworthy Global Computing - 8th International Symposium, TGC 2013, Buenos Aires, Argentina, August 30-31, 2013, Revised Selected Papers, Lecture Notes in
Computer Science 8358, Springer, pp. 297–314, doi:10.1007/978-3-319-05119-2 17.
[28] Diego Latella, Michele Loreti & Mieke Massink (2014): On-the-fly Probabilistic Model Checking. In Ivan
Lanese, Alberto Lluch-Lafuente, Ana Sokolova & Hugo Torres Vieira, editors: Proceedings 7th Interaction and Concurrency Experience, ICE 2014, Berlin, Germany, 6th June 2014., EPTCS 166, pp. 45–59,
doi:10.4204/EPTCS.166.6.
[29] Diego Latella, Michele Loreti & Mieke Massink (2015): On-the-fly PCTL fast mean-field approximated model-checking for self-organising coordination.
Sci. Comput. Program. 110, pp. 23–50,
doi:10.1016/j.scico.2015.06.009.
[30] Michele Loreti & Jane Hillston (2016): Modelling and Analysis of Collective Adaptive Systems with CARMA
and its Tools. In Marco Bernardo, Rocco De Nicola & Jane Hillston, editors: Formal Methods for the

D. Latella & M. Massink

109

Quantitative Evaluation of Collective Adaptive Systems - 16th International School on Formal Methods for
the Design of Computer, Communication, and Software Systems, SFM 2016, Bertinoro, Italy, June 20-24,
2016, Advanced Lectures, Lecture Notes in Computer Science 9700, Springer, pp. 83–119, doi:10.1007/9783-319-34096-8 4.

Designing Attribute-based FlyFast

110

A

Appendix

Proof of Proposition 1
⇐: Trivial.
⇒:
We first prove that a = b:
∀m1 , . . . , mS .A(m1 , . . . , mS ) = B(m1 , . . . , mS )
⇒

{Logic}
A(0, . . . , 0) = B(0, . . . , 0)

⇒

{Def. of A(m1 , . . . , mS ) and B(m1 , . . . , mS )}
a=b

Now we prove that aii = bii for i = 1, . . . , S:
∀m1 , . . . , mS .A(m1 , . . . , mS ) = B(m1 , . . . , mS )
⇒

{Take the S − tuple (m̄1 , . . . , m̄S ) where m̄k = 1 if k = i and 0 otherwise}
A(m̄1 , . . . , m̄S ) = B(m̄1 , . . . , m̄S )

⇒

{Def. of A(m1 , . . . , mS ) and B(m1 , . . . , mS )}
aii + a = bii + b

⇒

{a = b (see above)}
aii = bii

Finally we prove that ai j = bi j , for i, j = 1, . . . , S, j > i:
∀m1 , . . . , mS .A(m1 , . . . , mS ) = B(m1 , . . . , mS )
⇒

{(m̃1 , . . . , m̃S ) where m̃k = 0.5 if k ∈ {i, j} and 0 otherwise}
A(m̃1 , . . . , m̃S ) = B(m̃1 , . . . , m̃S )

⇒

{Def. of A(m1 , . . . , mS ) and B(m1 , . . . , mS )}
0.25aii + 0.25ai j + 0.25a j j + a = 0.25bii + 0.25bi j + 0.25b j j + b

⇒

{a = b (see above)}
0.25aii + 0.25ai j + 0.25a j j = 0.25bii + 0.25bi j + 0.25b j j

⇒

{Algebra}
aii + ai j + a j j = bii + bi j + b j j

⇒

{aii = bii and a j j = b j j (see above)}
ai j = bi j

•

