 Main
Formal Techniques for the Verification and Optimal Control of Probabilistic Systems in the Presence of Modeling Uncertainties
 Puggelli, Alberto
 Advisor(s): SangiovanniVincentelli, Alberto L.
Abstract
We present a framework to design and verify the behavior of stochastic systems whose parameters are not known with certainty but are instead affected by modeling uncertainties, due for example to modeling errors, nonmodeled dynamics or inaccuracies in the probability estimation. Our framework can be applied to the analysis of intrinsically randomized systems (e.g., random back off schemes in wireless protocols) and of abstractions of deterministic systems whose dynamics are interpreted stochastically to simplify their representation (e.g., the forecast of wind availability).
In the first part of the dissertation, we introduce the model of Convex Markov Decision Processes (ConvexMDPs) as the modeling framework to represent the behavior of stochastic systems. ConvexMDPs generalize MDPs by expressing statetransition probabilities not only with fixed realization frequencies but also with nonlinear convex sets of probability distribution functions. These convex sets represent the uncertainty in the modeling process.
In the second part of the dissertation, we address the problem of formally verifying properties of the execution behavior of ConvexMDPs. In particular, we aim to verify that the system behaves correctly under all valid operating conditions and under all possible resolutions of the uncertainty in the statetransition probabilities. We use Probabilistic Computation Tree Logic (PCTL) as the formal logic to express system properties.
Using results on strong duality for convex programs, we present a modelchecking algorithm for PCTL properties of ConvexMDPs, and prove that it runs in time polynomial in the size of the model under analysis.
The developed algorithm is the first known polynomialtime algorithm for the verification of PCTL properties of ConvexMDPs. This result allows us to lower the previously known algorithmic complexity upper bound for
IntervalMDPs from coNP to P, and it is valid also for the more expressive (convex) uncertainty models supported by the ConvexMDP formalism.
We apply the proposed framework and modelchecking algorithm to the problem of formally verifying quantitative
properties of models of the behavior of human drivers. We first propose a novel stochastic model
of the driver behavior based on Convex Markov chains. The model is capable of capturing the intrinsic uncertainty in estimating the intricacies of the human behavior starting from
experimentally collected data. We then formally verify properties of
the model expressed in PCTL. Results show
that our approach can correctly predict quantitative information
about the driver behavior depending on his/her attention state,
e.g., whether the driver is attentive or distracted while driving, and on the environmental conditions, e.g., the presence of an obstacle on the road.
Finally, in the third part of the dissertation, we analyze the problem of synthesizing optimal control strategies for ConvexMDPs, aiming to optimize a given system performance, while guaranteeing that the system behavior fulfills a specification expressed in PCTL under all resolutions of the uncertainty in the statetransition probabilities. In particular, we focus on Markov strategies, i.e., strategies that depend only on the instantaneous execution state and not on the full execution history. We first prove that adding uncertainty in the representation of the statetransition probabilities does not increase the theoretical complexity of the synthesis problem, which remains in the class NPcomplete as the analogous problem applied to MDPs, i.e., when all transition probabilities are known with certainty. We then interpret the strategysynthesis problem as a constrained optimization problem and propose the first sound and complete algorithm to solve it.
We apply the developed strategysynthesis algorithm to the problem of generating optimal energy pricing and purchasing strategies for a forprofit energy aggregator whose portfolio of energy supplies includes renewable sources, e.g., wind. Economic incentives have been proposed to manage user demand and compensate for the intrinsic uncertainty in the prediction of the supply generation. Stochastic control techniques are however needed to maximize the economic profit for the energy aggregator while quantitatively guaranteeing qualityofservice for the users. We use ConvexMDPs to model the decisionmaking scenario and train the models with measured data, to quantitatively capture the uncertainty in the prediction of renewable energy generation. An experimental comparison shows that the control strategies synthesized using the proposed technique significantly increase system performance with respect to previous approaches presented in the literature.
Main Content
Enter the password to open this PDF file:













