Control in Boolean networks with model checking

TL;DR

This paper introduces a model checking-based method for identifying all minimal control strategies in Boolean networks, enhancing flexibility and completeness over existing approaches, with applications to biological systems.

Contribution

A novel model checking approach that guarantees finding all minimal control strategies in Boolean networks, addressing limitations of previous methods.

Findings

Successfully identified all minimal control strategies in various biological systems.

Outperformed existing methods in completeness and flexibility.

Demonstrated applicability across multiple control problems.

Abstract

Understanding control mechanisms in biological systems plays a crucial role in important applications, for instance in cell reprogramming. Boolean modeling allows the identification of possible efficient strategies, helping to reduce the usually high and time-consuming experimental efforts. Available approaches to control strategy identification usually focus either on attractor or phenotype control, and are unable to deal with more complex control problems, for instance phenotype avoidance. They also fail to capture, in many situations, all possible minimal strategies, finding instead only sub-optimal solutions. In order to fill these gaps, we present a novel approach to control strategy identification in Boolean networks based on model checking. The method is guaranteed to identify all minimal control strategies, and provides maximal flexibility in the definition of the control target. We investigate the applicability of the approach by considering a range of control problems for different biological systems, comparing the results, where possible, to those obtained by alternative control methods.