Structured Synthesis For Probabilistic Systems

We introduce the concept of structured synthesis for Markov decision processes. A structure is induced from finitely many pre-specified options for a system configuration. We define the structured synthesis problem as a nonlinear programming problem (NLP) with integer variables. As solving NLPs is not feasible in general, we present an alternative approach. A transformation of models specified in the PRISM probabilistic programming language creates models that account for all possible system configurations by nondeterministic choices. Together with a control module that ensures consistent configurations throughout a run of 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. We motivate and demonstrate the usefulness of the approach along a realistic case study involving surveillance by unmanned aerial vehicles in a shipping facility.