Procrustes : Pattern-based property editor
Models of the dynamics of cellular interaction networks have become increasingly large in recent years. The study of these models by analysis and simulation tools generates a large number of predictions of the possible dynamical behaviors of the system. When representing the system dynamics by means of discrete state transition graphs (e.g., Kripke structures), it becomes possible to use formal verification techniques for the verification of certain properties of interest. However, this requires the formulation of the properties in temporal logic, which is not evident for the non-expert user.
In order to deal with this problem, a set of patterns (high-level query templates) were defined to capture recurring biological questions posed by modelers. The patterns consist of structured natural language phrases which can be translated into temporal logic formulas.
Procrustes is a pattern-based property editor that enables the translation of each pattern into a temporal logic formula (currently CTL, CTRL and mu-calculus are supported). Procrustes has been implemented in Java 1.5 and is composed of two modules : the graphical user interface and the pattern translator API. The latter has been integrated in Genetic Network Analyzer (GNA), a computer tool for the modeling and simulation of genetic regulatory networks.
Obtaining and using Procrustes
Alternatively, it can be obtained through the following links and integrated in other modeling tools :
P.T. Monteiro, D. Ropers, R. Mateescu, A.T. Freitas and H. de Jong (2008), Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks, Bioinformatics, 24(16) : i227-i233