Boolean networks are an important qualitative modelling technique that provide techniques for analysing the attractors (important cyclic behaviour) in a model. However, their practical application is limited by the state space explosion problem and this had led to researchers considering compositional techniques. In this paper we take a recently developed compositional framework for Boolean networks based on using logical connectives to merge entities and extend it with compositional techniques for attractor analysis. Our approach is based on using strongly connected components to identify potential cyclic behaviour taking into account the interference arising from a composition. We develop tool support for our approach and illustrate its practical application by a case study.

Qualitative logical modelling techniques play an important role in biology and are seen as crucial for developing scalable methods for modelling and synthesizing biological systems. While a range of interesting work has been done in this area there still exists challenging issues that need to be ad dressed for the practical application of these modelling techniques. In this paper we present an algebraic framework for exploring these issues by developing techniques for modelling and analysing qualitative biological models using Rewriting Logic (RL). The aim here is to develop a universal formal framework which is able to integrate models expressed in different formalisms (e.g. Boolean networks, Petri Nets and process algebra) and provide a basis for new work in this area (e.g. merging models based on different formalisms; compositional model construction and analysis; and tools for synthetic biology). We take as our starting point Multi-valued networks (MVNs), a simple yet expressive qualitative state based modelling approach widely used in biology. We develop a semantic translation from MVNs to a corresponding RL model and formally show that this translation is correct. We consider both the asynchronous and synchronous update semantics, and investigate the use of rewriting strategies to enable synchronisation to be modelled. We illustrate the RL framework developed and the potential RL analysis possible by presenting two detailed case studies.

Abstract The process algebras Timed Mobility (TiMo) and its extension Permissions, Timers and Mobility (PerTiMo) were recently proposed to support engineering applications in distributed system design.TiMoprovides a formal framework in which process migration between distinct locations and timing constraints linked to local clocks can be modelled and analysed. This is extended inPerTiMoby associating access permissions to communication to model security aspects of a distributed system. In this paper we develop a new semantic model forTiMousing Rewriting Logic (RL) and strategies, with the aim of providing a foundation for tool support; in particular, strategies are used to capture the locally maximal concurrent step of aTiMospecification which previously required the use of action rules based on negative premises. This RL model is then extended with access permissions in order to develop a new semantic model forPerTiMo. These RL semantical models are formally proved to be sound and complete with respect to the original operational semantics on which they were based. We present examples of how the developed RL models forTiMoandPerTiMocan be implemented within the strategy-based rewriting systemElanand illustrate the range of (behavioural) properties that can be analysed using such a tool.

MOTIVATION: New developments in post-genomic technology now provide researchers with the data necessary to study regulatory processes in a holistic fashion at multiple levels of biological organization. One of the major challenges for the biologist is to integrate and interpret these vast data resources to gain a greater understanding of the structure and function of the molecular processes that mediate adaptive and cell cycle driven changes in gene expression. In order to achieve this biologists require new tools and techniques to allow pathway related data to be modelled and analysed as network structures, providing valuable insights which can then be validated and investigated in the laboratory. RESULTS: We propose a new technique for constructing and analysing qualitative models of genetic regulatory networks based on the Petri net formalism. We take as our starting point the Boolean network approach of treating genes as binary switches and develop a new Petri net model which uses logic minimization to automate the construction of compact qualitative models. Our approach addresses the shortcomings of Boolean networks by providing access to the wide range of existing Petri net analysis techniques and by using non-determinism to cope with incomplete and inconsistent data. The ideas we present are illustrated by a case study in which the genetic regulatory network controlling sporulation in the bacterium Bacillus subtilis is modelled and analysed. AVAILABILITY: The Petri net model construction tool and the data files for the B. subtilis sporulation case study are available at http://bioinf.ncl.ac.uk/gnapn.

SUMMARY: SARGE is a tool for creating, visualizing and manipulating a putative genetic network from time series microarray data. The tool assigns potential edges through time-lagged correlation, incorporates a clustering mechanism, an interactive visual graph representation and employs simulated annealing for network optimization. AVAILABILITY: The application is available as a .jar file from http://www.bioinformatics.cs.ncl.ac.uk/sarge/index.html.