I am delighted to post Orna Kupferman's interview with CONCUR 2022 Test-of-Time Award recipients Christel Baier, Holger Hermanns and Joost-Pieter Katoen.
Thanks to Christel, Holger and Joost-Pieter for their answers (labelled BHK in what follows) and to Orna (Q below) for conducting the interview. Enjoy and watch this space for upcoming interviews with the other award recipients!
Q: You receive the CONCUR Test-of-Time Award 2022 for your paper "Approximate symbolic model checking of continuous-time Markov chains," which appeared
at CONCUR 1998. In that article, you combine three different challenges: symbolic algorithms, real-time systems, and probabilistic systems. Could you briefly explain to our readers what the main challenge in such a combination is?
BHK: The main challenge is to provide a fixed-point characterization of time-bounded reachability probabilities: the probability to reach a given target state within a given deadline. Almost all works in the field up to 1999 treated discrete-time probabilistic models and focused on "just" reachability probabilities: what is the probability to eventually end up in a given target state? This can be characterized as a unique solution of a linear equation system. The question at stake was: how to incorporate a real-valued deadline d? The main insight was
to split the problem in staying a certain amount of time, x say, in the current state and using the remaining d-x time to reach the target from its successor state. This yields a Volterra integral equation system; indeed time-bounded reachability probabilities are unique solutions of such equation systems. In the CONCUR'99 paper we suggested to use symbolic data structures to do the numerical integration; later we found out that much more efficient techniques can be applied.
Q: Could you tell us how you started your collaboration on the award-winning paper? In particular, as the paper combines three different challenges, is it the case that each of you has brought to the research different expertise?
BHK: Christel and Joost-Pieter were both in Birmingham, where a meeting of a
collaboration project between German and British research groups on stochastic systems and process algebra took place. There the first ideas of model checking continuous-time Markov chains arose, especially for time-bounded reachability: with stochastic process algebras there were means to model CTMCs in a compositional manner, but verification was lacking. Back in Germany, Holger suggested to include a steady-state operator, the counterpart of transient properties that can be expressed using timed reachability probabilities. We then also developed the symbolic data structure to support the verification of the entire logic.
Q: Your contribution included a generalization of BDDs (binary decision diagrams) to MTDDs (multi-terminal decision diagrams), which allow both Boolean and real-valued variables. What do you think about the current state of symbolic algorithms, in particular the choice between SAT-based methods and methods that are based on decision diagrams?
BHK: BDD-based techniques entered probabilistic model checking in the mid 1990's for discrete-time models such as Markov chains. Our paper was one of the first, perhaps even the first, that proposed to use BDD structures for real-time stochastic processes. Nowadays, SAT, and in particular SMT-based techniques belong to the standard machinery in probabilistic model checking. SMT techniques are e.g., used in bisimulation minimization at the language level, counterexample generation, and parameter synthesis. This includes both linear as well as non-linear theories. BDD techniques are still used, mostly in combination with sparse representations, but it is fair to say that SMT is becoming more and more relevant.
Q: What are the research topics that you find most interesting right now? Is there any specific problem in your current field of interest that you'd like to see solved?
BHK: This depends a bit on whom you ask! Christel's recent work is about cause-effect reasoning and notions of responsibility in the verification context. This ties into the research interest of Holger who looks at the foundations of perspicuous software systems. This research is rooted in the observation that the explosion of opportunities for software-driven innovations comes with an implosion of human opportunities and capabilities to understand and control these innovations. Joost-Pieter focuses on pushing the borders of automation in weakest-precondition reasoning of probabilistic programs. This involves loop invariant synthesis, probabilistic termination proofs, the development of deductive verifiers, and so forth. Challenges are to come up with good techniques for synthesizing quantitative loop invariants, or even complete probabilistic programs.
Q: What advice would you give to a young researcher who is keen to start working on topics related to symbolic algorithms, real-time systems, and probabilistic systems?
BHK: Try to keep it smart and simple.
No comments:
Post a Comment