A language for populations

Population Language is used to model systems composed by N identical interacting processes or objects. At any point in time, each object can be in any of its finitely many states and the evolution of the system proceeds in a clock-synchronous fashion: at each clock tick each member
of the population must either execute one of the transitions that are enabled in its current state, or remain in such a state (see here for all the formal details).

To create a new Population Project go to File -> New -> Other… and select Population Project


After that provide a name for the new project:


After that a new project is created that contains a simple specification:


The provided model describes a network of computers that can be infected by a worm. Each node in the network can acquire infection from two sources, i.e. by the activity of a worm of an infected node (inf_sus) or by an external source (inf_ext). Once a computer is infected, the worm
remains latent for a while, and then activates (activate).


When the worm is active, it tries to propagate over the network by sending messages to other nodes.  After some time, an infected computer can be patched (patch), so that the infection is recovered. New versions of the worm can appear; for this reason, recovered computers can become susceptible to infection again, after a while (loss).

Simulation tools can be used to used to estimate system behaviour. Two kind of simulations are available: one based on standard probabilistic simulation (referred as individuals in the simulation panel) and one based on fast simulations. The latter uses a mean-field approximation to simulate the behaviour of a single object in the context of a large class of elements.

This plug-in also provides a specific model checking procedure, named FlyFast that can be used to verify large scaled systems. This procedure exploits mean field approximation in model-checking techniques to overcome scalability issues raised by the size of systems. Details on the procedure are available here.

By relying on FlyFast we can check if a given element satisfies or not a given property when it is located in an environment with a given structure. FlyFast model checking panel can be used to select the state of the single elements and to state the fraction of the individuals in the context in the different state (these fractions can be inferred from a specific state). This tool can be used to estimate the probability that an object in state S can get infected within the next k steps:

Screen Shot 2016-10-19 at 07.31.14

The result will be then visualised in the Graph View: