The modeling and analysis of probabilistic dynamical systems is becoming a central topic in the formal methods community. Usually, Markov chains of various kinds serve as the core mathematical formalism in these studies. However, in many of these settings, the probabilistic graphical model called dynamic Bayesian networks (DBNs) [4] can be a more appropriate model to work with. This is so since a DBN is often a factored and succinct representation of an underlying Markov chain. Our goal here is to describe DBNs from this standpoint. After introducing the basic formalism, we discuss inferenc-ing algorithms for DBNs. We then consider a simple probabilistic temporal logic and the associated model checking problem for DBNs with a finite time horizon. Finally, we describe how DBNs can be used to study the behavior of biochemical networks.
展开▼
