Scalable Model Checking.
Subtask 2.1: Parametric approximated inference in DBN
Subtask 2.2: Prototype of the inference algorithm
Subtask 2.3: Model-checker for DBN
Subtask 3.1: Compute the contracting factor of a DBN
Subtask 3.2: Compute one-step error of the approximated inference
Subtask 4.1: (Un)decidable class of MDPs for LTL over distribution.
Subtask 4.2: Approximation algorithm on this compact model
Subtask 4.3: Model for representing compactly a MDP
Subtask 5.1: Model Hela cells death as a DBN and application
Subtask 5.2: Model stress response in yeast as a MDP and application