"Antelope": a hybrid-logic model checker for branching-time Boolean GRN analysis.

ABSTRACT:

Background

In Thomas' formalism for modeling gene regulatory networks (GRNs), branching time, where a state can have more than one possible future, plays a prominent role. By representing a certain degree of unpredictability, branching time can model several important phenomena, such as (a) asynchrony, (b) incompletely specified behavior, and (c) interaction with the environment. Introducing more than one possible future for a state, however, creates a difficulty for ordinary simulators, because infinitely many paths may appear, limiting ordinary simulators to statistical conclusions. Model checkers for branching time, by contrast, are able to prove properties in the presence of infinitely many paths.

Results

We have developed Antelope ("Analysis of Networks through TEmporal

SUBMITTER: Arellano G 

PROVIDER: S-EPMC3316443 | biostudies-literature | 2011 Dec

REPOSITORIES: biostudies-literature