Bi-Weekly Talk: Jip Spel: Finding Provably Optimal Markov Chains
Wednesday, January 27, 2021, 10:00am
Already at 10:00 we meet for a break: Let’s talk, exchange, chat and drink our coffee or tea till the talk starts!
The zoom-room will be open.
Location: Online session
Speaker: Jip Spel
Parametric Markov chains (pMCs) are Markov chains withsymbolic (aka: parametric) transition probabilities. They are a convenientoperational model to treat robustness against uncertainties. A typicalobjective is to find the parameter values that maximize the reachabilityof some target states. In this paper, we consider automatically provingrobustness, that is, an ε-close upper bound on the maximal reachabilityprobability. The result of our procedure actually provides an almost-optimal parameter valuation along with this upper bound. We propose totackle these ETR-hard problems by a tight combination of two seeminglyunrelated techniques: monotonicity checking and parameter lifting. Theformer builds a partial order on states to check whether a pMC is (local orglobal) monotonic in a certain parameter, whereas parameter lifting is anabstraction technique based on the iterative evaluation of pMCs withoutparameter dependencies. We explain our novel algorithmic approach andexperimentally show that we significantly improve the time to determinealmost-optimal synthesis.