Temporal-logics as query languages for Dynamic Bayesian Networks: Application to D. melanogaster Embryo Development

This paper introduces novel techniques for exact and approximate inference in Dynamic Bayesian Networks (DBNs) based on algorithms, data structures, and formalisms from the field of model checking. Model checking comprises a family of techniques from for formally verifying systems of concurrent reactive processes. We discuss: i) the use of temporal logics as a query language for inference over DBNs; ii) translation of DBNs into probabilistic reactive modules; and iii) the use of symbolic data structures and algorithms for deciding complex stochastic temporal logic formulas. We demonstrate the effectiveness of these new algorithms by examining the behavior of an enhanced expression model of embryogenesis in D. melanogaster. In particular, we converted an existing deterministic developmental model over a one-dimensional arrays of cells into a stochastic model over a two dimensional array of cells. Our results confirm that the rules which govern the one-dimensional model also display wild-type expression patterns in the two-dimensional case within certain parameter bounds.