A big challenge of current biology is understanding the principles and functioning of complex biological systems. Describing biological systems by means originally developed by computer scientists can provide tools and methods to get an insight into the modelled phenomena.
Temporal logics and model-checking have proved successful to respectively express biological properties of complex biochemical systems, and automatically verify their satisfaction in both qualitative and quantitative models. However, especially complex systems analysis suffers from the state-space explosion.
In our work we go beyond model checking, we consider revising, simplifying and synthesising models of biological systems by using formally specified properties of the system.
In this seminar we show a polynomial method for synthesising qualitative models of biological systems from temporal logic specifications. Moreover these models can be model checked for specific shapes of properties using only small portion of the entire model.