New methods verify and control complex decision systems with changing parameters
Supermartingale Certificates for Parametric MDPs
Logic in Computer ScienceArtificial Intelligence
Summary
Some decision-making systems rely on probabilities that depend on parameters we cannot fix in advance. The authors show how to transform these systems to a form without parameters, preserving the behavior exactly. They introduce a new type of mathematical certificate called parametric supermartingales to analyze these systems. Their approach supports both checking if the system behaves correctly and designing decisions for it, even when states and actions form continuous ranges. They validate their methods with experiments on continuous random walks that change with parameters.
What this means in practice
- •For control system engineers: Verify and design controllers for systems with continuous parameters and states using the new parametric supermartingale techniques.
- •For robotics developers: Build planning algorithms that adapt to uncertain, parameter-dependent environments modeled as parametric MDPs with continuous actions.
Authors
Kaushik Mallik, Ðorđe Žikelić
Abstract
We consider the problems of formal verification and synthesis in parametric Markov decision processes (MDPs) with general measurable state and action spaces. The heart of our approach is a parameter flattening transformation, which allows us to transform parametric MDPs into semantically equivalent non-parametric MDPs. Building on this transformation, we introduce the novel notion of parametric supermartingale certificates, which generalize the traditional supermartingale certificates---used for non-parametric MDPs---to the parametric setting. We use our parametric supermartingale certificates to design algorithms for verification and approximate synthesis in polynomial arithmetic parametric MDPs. This leads to the first verification and synthesis algorithms for parametric MDPs with general state and action spaces. We implement our algorithms and experimentally evaluate them on several continuous parametric random walk benchmarks.