Uninterpreted functions are a key modeling tool for systems with unknown or abstracted components. Certain domains, such as systems biology, additionally impose monotonicity constraints on these components, requiring specific inputs to have a consistently positive or negative effect on the output. In this paper, we tackle the model inference problem for biological systems by applying the theory of uninterpreted functions with monotonicity constraints. We compare the performance of naive quantified encodings of the problem and the performance of the existing approach based on eager quantifier instantiation, which is based on the fact that a finite set of quantifier-free monotonicity lemmas is sufficient to encode the monotonicity of uninterpreted functions. Additionally, we consider a lazy variant of the approach that introduces the monotonicity lemmas on demand. We evaluate the SMT-based approach to model inference using a large collection of systems biology benchmarks. The results demonstrate that the instantiation-based encodings significantly outperform quantified encodings, which typically struggle with large function arities and complex instances. As the key result, we show that our approach based on SMT with uninterpreted functions and monotonicity constraints significantly outperforms state-of-the-art domain-specific tools used in systems biology, such as the ASP-based Bonesis and the BDD-based AEON.

MOTIVATION: The problem of model inference is of fundamental importance to systems biology. Logical models (e.g. Boolean networks; BNs) represent a computationally attractive approach capable of handling large biological networks. The models are typically inferred from experimental data. However, even with a substantial amount of experimental data supported by some prior knowledge, existing inference methods often focus on a small sample of admissible candidate models only. RESULTS: We propose Boolean network sketches as a new formal instrument for the inference of Boolean networks. A sketch integrates (typically partial) knowledge about the network's topology and the update logic (obtained through, e.g. a biological knowledge base or a literature search), as well as further assumptions about the properties of the network's transitions (e.g. the form of its attractor landscape), and additional restrictions on the model dynamics given by the measured experimental data. Our new BNs inference algorithm starts with an 'initial' sketch, which is extended by adding restrictions representing experimental data to a 'data-informed' sketch and subsequently computes all BNs consistent with the data-informed sketch. Our algorithm is based on a symbolic representation and coloured model-checking. Our approach is unique in its ability to cover a broad spectrum of knowledge and efficiently produce a compact representation of all inferred BNs. We evaluate the method on a non-trivial collection of real-world and simulated data. AVAILABILITY AND IMPLEMENTATION: All software and data are freely available as a reproducible artefact at https://doi.org/10.5281/zenodo.7688740.

SUMMARY: AEON.py is a Python library for the analysis of the long-term behaviour in very large asynchronous Boolean networks. It provides significant computational improvements over the state-of-the-art methods for attractor detection. Furthermore, it admits the analysis of partially specified Boolean networks with uncertain update functions. It also includes techniques for identifying viable source-target control strategies and the assessment of their robustness with respect to parameter perturbations. AVAILABILITY AND IMPLEMENTATION: All relevant results are available in Supplementary Materials. The tool is accessible through https://github.com/sybila/biodivine-aeon-py. SUPPLEMENTARY INFORMATION: Supplementary data are available at Bioinformatics online.