Showing 1–2 of 2 results for author: Spel, J

Gradient-Descent for Randomized Controllers under Partial Observability

Authors: Linus Heck, Jip Spel, Sebastian Junges, Joshua Moerman, Joost-Pieter Katoen

Abstract: Randomization is a powerful technique to create robust controllers, in particular in partially observable settings. The degrees of randomization have a significant impact on the system performance, yet they are intricate to get right. The use of synthesis algorithms for parametric Markov chains (pMCs) is a promising direction to support the design process of such controllers. This paper shows how… ▽ More Randomization is a powerful technique to create robust controllers, in particular in partially observable settings. The degrees of randomization have a significant impact on the system performance, yet they are intricate to get right. The use of synthesis algorithms for parametric Markov chains (pMCs) is a promising direction to support the design process of such controllers. This paper shows how to define and evaluate gradients of pMCs. Furthermore, it investigates varieties of gradient descent techniques from the machine learning community to synthesize the probabilities in a pMC. The resulting method scales to significantly larger pMCs than before and empirically outperforms the state-of-the-art, often by at least one order of magnitude. △ Less

Submitted 8 November, 2021; originally announced November 2021.

Comments: Technical Report VMCAI22 submission

Are Parametric Markov Chains Monotonic?

Authors: Jip Spel, Sebastian Junges, Joost-Pieter Katoen

Abstract: This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct - only using the graph structure of the Markov chain and local transition probabilities - a pre-order on the states. Our algorithm cheaply checks a sufficient condition for monotonicity. Experiments show that monotonicity… ▽ More This paper presents a simple algorithm to check whether reachability probabilities in parametric Markov chains are monotonic in (some of) the parameters. The idea is to construct - only using the graph structure of the Markov chain and local transition probabilities - a pre-order on the states. Our algorithm cheaply checks a sufficient condition for monotonicity. Experiments show that monotonicity in several benchmarks is automatically detected, and monotonicity can speed up parameter synthesis up to orders of magnitude faster than a symbolic baseline. △ Less

Submitted 19 July, 2019; originally announced July 2019.

Comments: Extended version of ATVA 2019 paper with the same title