MIRACH

MIRACH performs online model checking of biological pathway models to verify pathway behaviors against formally specified properties.

Key Features:

• Supported formats: Accepts pathway models in CSML (Cell Signaling Markup Language) and SBML (Systems Biology Markup Language).
• Model checking mode: Performs efficient on-the-fly (online) verification of pathway models rather than offline batch checking.
• Simulation engine: Uses a Petri-net-based simulation engine to drive model execution and checking.
• Property specification: Allows properties and rules to be expressed in Propositional Linear Temporal Logic (PLTLs) for formal verification.
• Performance: Reported experimental evaluation using Levchenko et al.'s model indicates time-savings exceeding 400% compared to offline methods.
• Model focus: Targets correctness verification of complex biological signaling and pathway models.

Scientific Applications:

• Pathway model verification: Formally verifies that CSML and SBML pathway models satisfy specified temporal properties.
• Behavioral validation: Validates that pathway behaviors align with expected outcomes expressed as PLTLs.
• Systems biology analysis: Supports rigorous analysis and validation of signaling and regulatory pathways in systems biology studies.

Methodology:

Performs on-the-fly model checking by simulating CSML and SBML pathway models with a Petri-net-based simulation engine while checking PLTLs-specified properties during execution.