FoSSaCS Invited Speaker Christel Baier
Christel Baier is a full professor and head of the chair for Algebraic and Logic Foundations of Computer Science at the Faculty of Computer Science of the Technische Universität Dresden since 2006. Currently, she serves as Dean of the Faculty Computer Science. Since 2022 she holds an honorary doctorate (Dr. rer. nat. h.c.) from RWTH Aachen. From the University of Mannheim she received her Diploma in Mathematics in 1990, her Ph.D. in Computer Science in 1994 and her Habilitation in 1999. She was an associate professor for Theoretical Computer Science at the University of Bonn from 1999 to 2006. She was member of the DFG (German Research Foundation) review board for computer science from 2012 to 2019, and is a member of the DFG senate commission on Research Training Groups since 2020. She is a member of Academia Europaea and of the Saxony Academy of Science. Her research focuses on modeling, specification and verification of reactive systems, quantitative analysis of stochastic systems, probabilistic model checking, temporal and modal logics and automata theory.
Talk
Verification of Infinite-horizon Properties of Dynamic Bayesian Networks
Time: April 13, 9-10am
Room: TBA
Bayesian networks and their variants are a prominent graphical representation of distributions over random variables with a wide range of applications in, e.g., data mining, robotics, speech recognition or systems biology. They succinctly represent full joint distributions using a directed acyclic graph to capture (in)dependencies between the variables. Dynamic Bayesian networks (DBN) serve to describe the how the distributions evolve over time. Assuming a discrete time domain, DBNs thus represent sequences of distributions. While classical approaches for the analysis of DBNs focus on finite-horizon inference, the talk will be about verification problems for their long-run behavior defined by the induced infinite sequence of distributions. With this view, DBNs correspond to finite-state Markov chains under the distribution-transformer semantics. Thus, known Skolem-hardness results for verification problems for Markov chains under the distribution-transformer semantics carry over to DBNs, and existing verification algorithms are either incomplete or rely on additional assumptions. However, reasoning about infinite-horizon properties of the underlying causal network of a DBN is easier. This applies, e.g., to temporal properties of the evolution of structural conditional independencies represented by formulas of linear temporal logic or by a nondeterministic Büchi automaton. Another example where decidability results for DBNs and Markov chains under the distribution-transformer semantics can be established are mean payoff properties for polynomial weight functions or even more general classes of continuous weight functions.