Here you can find my PhD thesis and the slides I used during my public PhD defence.
Abstract
Reaction systems are a formal model inspired by the functioning of living cells. This model allows for specifying and analysing computational processes in which reactions operate on sets of molecules.
The behaviour of a reaction system is determined by the interactions of its reactions, which are based on the mechanisms of facilitation and inhibition. The formal treatment of reaction systems is qualitative and there is no direct representation of the number of molecules involved in reactions.
In this thesis we introduce formal verification methods for reaction systems. Behaviour of reaction systems depends on interactions of the system with its environment. We show extensions of reaction systems that allow for generating the behaviours of the environment, which are considered realistic or relevant for the verification. We introduce an extension of reaction systems, which allows for direct quantitative modelling of discrete concentration levels. We also propose multi-agent reaction systems that allow for modelling of distributed and multi-agent systems in the reaction systems setting.
To allow for specifying properties of reaction systems and their extensions we introduce temporal logics for reaction systems: rsCTL, which is a branching-time temporal logic, and rsLTL, which is a linear-time temporal logic. Additionally, to enable reasoning about temporal and epistemic properties of multi-agent reaction systems we propose rsCTLK, which is a temporal-epistemic logic. Operators of the introduced logics allow for selecting the desired environment behaviours.
We define parametric reaction systems where reactions may be defined partially, by using parameters in place of ordinary reaction elements. We demonstrate a parameter synthesis approach which under a set of rsLTL specifications calculates a valuation for the parameters which meets the provided specification.
For the defined formalisms we propose symbolic model checking methods based on binary decision diagrams and satisfiability modulo theories. We implement and evaluate these methods experimentally. For the experimental results we introduce a number of scalable reaction systems modelled using the proposed extensions.
Finally, we introduce a verification toolkit for reaction systems, which implements the methods proposed in this thesis.