Structured Synthesis for Probabilistic Systems
Abstract
We introduce the concept of structured synthesis for Markov decision processes where the structure is induced from finitely many pre-specified options for a system configuration. The resulting synthesis problem is in general a nonlinear programming problem (NLP) with integer variables. As solving NLPs is in general not feasible, we present an alternative approach. We present a transformation of models specified in the {PRISM} probabilistic programming language to models that account for all possible system configurations by means of nondeterministic choices. Together with a control module that ensures consistent configurations throughout the system, this transformation enables the use of optimized tools for model checking in a black-box fashion. While this transformation increases the size of a model, experiments with standard benchmarks show that the method provides a feasible approach for structured synthesis. Moreover, we demonstrate the usefulness along a realistic case study involving surveillance by unmanned aerial vehicles in a shipping facility.
Cite
@article{arxiv.1807.06106,
title = {Structured Synthesis for Probabilistic Systems},
author = {Nils Jansen and Laura Humphrey and Jana Tumova and Ufuk Topcu},
journal= {arXiv preprint arXiv:1807.06106},
year = {2018}
}