• compartmental modelling
• formal methods
• simulation
• spatial modelling
• systems biology

In Systems Biology, spatial modelling allows an accurate description of phenomena whose behaviour is influenced by the spatial arrangement of the elements. In this thesis, we present various modelling formalisms with spatial features, each using a different abstraction level of the real space. From the formalisms with the most abstract notion of space, to the most concrete, we formally define the MIM Calculus with compartments, the Spatial P systems, and the Spatial CLS. Each formalism is suitable for the description of different kinds of systems, which call for the use of different space modelling abstractions. We present models of various real-world systems which benefit from the ability to precisely describe space-dependent behaviours.

We define the MIM Calculus, inspired by Molecular Interaction Maps, a graphical notation for bioregulatory networks. The MIM Calculus provides high-level operators with a direct biological meaning, which are used to describe the interaction capabilities of the elements of such systems. Its spatial extension includes the most abstract notion of space, namely it only allows the modelling of compartments. Such a feature allows distinguishing only the abstract position where an element is, identified by the name of the compartment.

Subsequently, we propose a spatial extension to the membrane computing formalism P systems. In this case, we follow a more precise approach to spatial modelling, by embedding membranes and objects in a two-dimensional discrete space. Some objects of a Spatial P system can be declared as mutually exclusive objects, with the constraint that each position can accommodate at most one of them. The distinction between ordinary and mutually exclusive objects can be thought of as an abstraction on the size of the objects. We study the computational complexity of the formalism and the problem of efficient simulation of some kinds of models.

Finally, we present the Spatial Calculus of Looping Sequences (Spatial CLS), which is an extension of the Calculus of Looping Sequences (CLS), a formalism geared towards the modelling of cellular systems. In this case, models are based on two/three dimensional continuous space, and allow an accurate description of the motion of the elements, and of their size. In particular, Spatial CLS allows the description of the space occupied by elements and membranes, which can change their sizes dynamically as the system evolves. Space conflicts which may occur can be resolved by performing a rearrangement of elements and membranes. As example applications of the calculus we present a model of cell proliferation, and a model of the quorum sensing process in Pseudomonas aeruginosa.