The topic of this thesis is a novel contribution to the problem of automated analysis of Boolean networks dynamics under uncertainty of logical parameters. Parametrised Boolean networks are considered where the parameter space is defined by unknown target levels of regulatory interactions. Recently, there have been proposed several results that employed coloured or symbolic model checking. In this thesis, a specific focus is given to attractors and their reachability which are of strong interest in systems biology.

In the first part, the goal of the thesis is to define formally the problem of attractors identification and their reachability in the setting with unknown parameters. This part will include analysis of the problem complexity.

In the second part, the goal is to investigate encoding of boolean networks by means of place/transition Petri nets. In this framework, the problem of reachable attractors identification will be reformulated and the notion of finite unfoldings will be extended to parametrised setting. The main part of the thesis is to explore the possibility of employing the Petri net unfoldings for efficient analysis of attractors.

The theoretical results will be supplemented with adequate algorithms and their prototype implementation. Based on these, empirical evaluation will be conducted on several biologically-relevant case studies.