Gene Regulatory Networks (GRNs) determine how genes interact and regulate each other, in order to control various biological processes in living organisms. Each component of the GRN may be regulated by other components in the network called regulators, often divided to activators or inhibitors, and the overall effect of these regulators is determined by a regulation function. Here, we study the possible form of regulation functions, termed regulation conditions, in Boolean networks, a well established formalism for GRN modeling. Many tools exist for analyzing and modeling GRNs to gain insights on the control mechanisms for biological processes. One such tool is the Reasoning Engine for Interaction Networks (RE:IN), a powerful formal verification-based method that has been used effectively to study various GRNs of developmental and stem cell systems. We formally explain the permitted regulation functions in RE:IN, while understanding the assumptions (monotonicity, symmetry-by-groups and first order logic) and restrictions. Motivated by the effective use of RE:IN, along with an interest in understanding its assumptions and extending its capabilities, we reduce the problem of specifying regulation conditions in Boolean Networks to a matrix representation. Using this representation, we study methods to count the number of regulation conditions, provide a simple proof for those currently supported, and suggest a systematic approach for extending the regulation conditions to handle biological cases that are currently not supported by RE:IN. By analyzing a database of Boolean networks developed by the research community, we provide support for the validity of the monotonicity assumption in Boolean Networks, and identify limitations imposed by currently supported regulation functions. Based on our extension, we implemented a prototype reasoning tool for networks with extended regulation conditions.

Network-Based Biocomputation (NBC) circuits are computational devices that utilize biological agents to efficiently explore designed nanofabricated networks and thus solve combinatorial problems. The main advantages of NBCs are the potential to combine massively parallel computation, inherent energy efficiency of the biological agents and maturity of nanofabrication technology. We present an integrated computational-aided toolset for simulation and verification of these circuits that enables analysis of both circuit correctness and the effects of agent stochastic dynamics on circuit behavior. Our approach enables early identification of design flaws and can lead to significant savings in resources, thus playing an important role in advancing this emerging paradigm.

Abstract Network-Based Biocomputation Circuits (NBCs) offer a new paradigm for solving complex computational problems by utilizing biological agents that operate in parallel to explore manufactured planar devices. The approach can also have future applications in diagnostics and medicine by combining NBCs computational power with the ability to interface with biological material. To realize this potential, devices should be designed in a way that ensures their correctness and robust operation. For this purpose, formal methods and tools can offer significant advantages by allowing investigation of design limitations and detection of errors before manufacturing and experimentation. Here we define a computational model for NBCs by providing formal semantics to NBC circuits. We present a formal verification-based approach and prototype tool that can assist in the design of NBCs by enabling verification of a given design’s correctness. Our tool allows verification of the correctness of NBC designs for several NP-Complete problems, including the Subset Sum, Exact Cover and Satisfiability problems and can be extended to other NBC implementations. Our approach is based on defining transition systems for NBCs and using temporal logic for specifying and proving properties of the design using model checking. Our formal model can also serve as a starting point for computational complexity studies of the power and limitations of NBC systems.

A recurring set of small sub-networks have been identified as the building blocks of biological networks across diverse organisms. These network motifs are associated with certain dynamic behaviors and define key modules that are important for understanding complex biological programs. Besides studying the properties of motifs in isolation, current algorithms typically evaluate the occurrence frequency of a specific motif in a given biological network compared to that in random networks of similar structure. However, it remains challenging to relate the structure of motifs to the observed and expected behavior of the larger, more complex network they are contained within. This problem is compounded as even the precise structure of most biological networks remains largely unknown. Previously, we developed a formal reasoning approach enabling the synthesis of biological networks capable of reproducing some experimentally observed behavior. Here, we extend this approach to allow reasoning over the requirement for specific network motifs as a way of explaining how these behaviors arise. We illustrate the approach by analyzing the motifs involved in sign-sensitive delay and pulse generation. We demonstrate the scalability and biological relevance of the approach by studying the previously defined networks governing myeloid differentiation, the yeast cell cycle, and naïve pluripotency in mouse embryonic stem cells, revealing the requirement for certain motifs in these systems.

Computational modelling of metabolic processes has proven to be a useful approach to formulate our knowledge and improve our understanding of core biochemical systems that are crucial to maintaining cellular functions. Towards understanding the broader role of metabolism on cellular decision-making in health and disease conditions, it is important to integrate the study of metabolism with other core regulatory systems and omics within the cell, including gene expression patterns. After quantitatively integrating gene expression profiles with a genome-scale reconstruction of human metabolism, we propose a set of combinatorial methods to reverse engineer gene expression profiles and to find pairs and higher-order combinations of genetic modifications that simultaneously optimize multi-objective cellular goals. This enables us to suggest classes of transcriptomic profiles that are most suitable to achieve given metabolic phenotypes. We demonstrate how our techniques are able to compute beneficial, neutral or "toxic" combinations of gene expression levels. We test our methods on nine tissue-specific cancer models, comparing our outcomes with the corresponding normal cells, identifying genes as targets for potential therapies. Our methods open the way to a broad class of applications that require an understanding of the interplay among genotype, metabolism, and cellular behaviour, at scale.

Computational modeling is now used effectively to complement experimental work in biology, allowing to identify gaps in our understanding of the biological systems studied, and to predict system behavior based on a mechanistic model.We provide an overview of several areas in biology for which formal verification has been successfully used.We highlight examples from both natural and engineered biological systems.In natural biological systems the main goal is to understand how a system works and predict its behavior, whereas for engineered biological systems the main goal is to engineer biological systems for new purposes, e.g. for building biology-based computational devices.We compare between the challenges in applying formal verification in biology and the application to traditional domains.Finally, we outline future research directions and opportunities for formal verification experts to contribute to the field.

Understanding how biological systems develop and function remains one of the main open scientific challenges of our times. An improved quantitative understanding of biological systems, assisted by computational models is also important for future bioengineering and biomedical applications. We present a computational approach aimed towards unifying hypotheses with models and experiments, allowing to formally represent what a biological system does (specification) how it does it (mechanism) and systematically compare to data characterizing system behavior(experiments). We describe our Biocharts framework geared towards supporting this approach and illustrate its application in several biological domains including bacterial colony growth, developmental biology, and stem cell population dynamics.

We describe an approach to support UML-based development of embedded systems by formal techniques. A subset of UML is extended with timing annotations and given a formal semantics. UML models are translated, via XMI, to the input format of formal tools, to allow timed and non-timed model checking and interactive theorem proving. Moreover, the Play-Engine tool is used to execute and analyze requirements by means of live sequence charts. We apply the approach to a part of an industrial case study, the MARS system, and report about the experiences, results and conclusions.

We extend live sequence charts (LSCs), a highly expressive variant of sequence diagrams, and provide the extension with an executable semantics. The extension involves support for instances that can bind to multiple objects and symbolic variables that can bind to arbitrary values. The result is a powerful executable language for expressing behavioral requirements on the level of inter-object interaction. The extension is implemented in full in our play-engine tool, with which one can execute the requirements directly without the need to build or synthesize an intra-object system model. It seems that in addition to many advantages in testing and requirements engineering, for some kinds of systems this could lead to the requirements actually serving as the final implementation.