Hybrid systems reachability

We partition multi-affine hybrid systems on a rectangular grid, and produce directed graphs by calculating the flux through the facets between adjacent grid elements. This allows us to use graph analysis methods to ask questions about reachability, and to identify some features of the system, such as sinks, sources, and watersheds. It should be noted that the generated directed graphs can offer strong results only when they suggest that there is no path from one region to another, the graphs generally allow for paths that the system does not.

Reachability visualization

It can be difficult to make sense of the directed graphs generated by our reachability algorithm. They often have a high number of dimensions, and may have a massive number of nodes. This tool allows a user to visualize several different projections and cross sections of the graph at once. By allowing the user to visualize the graph, to inspect different pieces of it from different angles, a greater understanding of the system is made easier.

Simulation of hybrid systems with event detection

CHARON

CHARON is a language for modular specification of interacting hybrid systems based on the notions of agent and mode. For hierarchical description of the system architecture, CHARON provides the operations of instantiation, hiding, and parallel composition on agents, which can be used to build a complex agent from other agents. The discrete and continuous behaviors of an agent are described using modes. For hierarchical description of the behavior of an agent, CHARON supports the operations of instantiation and nesting of modes. Furthermore, features such as weak preemption, history retention, and externally defined Java functions, facilitate the description of complex discrete behavior. Continuous behavior can be specified using differential as well as algebraic constraints, and invariants restricting the flow spaces, all of which can be declared at various levels of the hierarchy. The modular structure of the language is not merely syntactic, but also reflected in the semantics so that it can be exploited during analysis. You may download the latest version.

Bio Sketch Pad

Bio Sketch Pad is an interactive tool for modeling and designing biomolecular and cellular networks with a simple, easy-to-use, graphical front end, leveraging powerful tools from control theory, hybrid systems, and software engineering. More details can be found here. You can download it.

Hybrid Systems Model Builder

Hybrid Systems Model Builder (HSMB) is a tool to construct hybrid systems models from kinetic models expressed in SBML Level 2 annotated with rate law names. HSMB performs piecewise-linear approximation of a number of rate laws, including commonly used Michaelis-Menten and Hill laws. The approximation is represented in SBML using events that change parameters of rate laws in reactions. HSMB also converts original and hybrid SBML models into the input format of the CHARON tool for further analysis.

Annotation for SBML

We have proposed an annotation scheme to facilitate the automated transformation of models written in SBML into hybrid models. Hybridization depends on the rate laws in the model. The vast majority of the rate laws that one encounters can be identified with a small set of reaction types. Examples are mass action and Michaelis-Menten. Yet they are not trivial to recognize as such when coded in MathML, since any given formula can be written in many different ways.
We tag the rate laws that appear in an SBML file according to their type in order to facilitate their automated handling (in our case, replacing them with piecewise approximations). Here is a document describing a small set of annotations, the XML schema that codifies them and an example of an annotated file.
The annotation appears useful in other contexts. It has been adopted in the ESS tool (University of Tennessee).

Producibility analysis tool

Producability Analysis Tool allows the user to analyze a model of the metabolic network for consistency. The user can specify an organism in the BioCyc database or provide a network in the BioCyc flat file format or SBML. The tool can initialize and check the network for consistency. If leaks are found, the tool will prompt the user and suggest species to serve as patches. The user will be able to either proceed with defaults or manually specify corrections.
The session can proceed with the user asking queries regarding metabolite producibility and knockout in the context of various nutrient media and mutant genotypes. Specifically the user can input a set of metabolites in the nutrient media and a set of gene deletions, and the tool will analyze the network to determine producible metabolites. The user may also specify a survival criteria posed in the form of an essential metabolite set and use the tool to determine survival in various nutritional and mutational contexts.

HybridSBML

HybridSBML is a toolset written in C++ that provides utilities for performing simulation and reachability tests of SBML models. The primary goal of this package is to provide high performance tools, that are based on standard packages. It depends on the GNU Scientific Library (GSL) and a computer algebra system called GiNaC. The adoption of these packages gives it flexibility and a performance boost. The utilities take as input SBML models. The SBML files are parsed by libSBML, and the special annotations in the SBML needed for special tasks are parsed with Xerces. The utilities are command line based. The two utilities included in this toolset are: The toolset can be downloaded from here