Type: Article

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

Gustavo Arellano, Julián Argil, Eugenio Azpeitia, Mariana Benítez, Miguel Carrillo, Pedro Góngora, David A Rosenblueth, Elena R Alvarez-Buylla;

Abstract:

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.