Structured Synthesis for Probabilistic Systems
This addresses the challenge of synthesizing configurations for probabilistic systems, offering an incremental method for specific domains like surveillance.
The paper tackles the problem of structured synthesis for Markov decision processes by transforming models to account for system configurations, enabling the use of existing model checking tools; experiments show it provides a feasible approach with standard benchmarks and is demonstrated in a surveillance case study.
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.