Formal Techniques for the Verification and Optimal Control of Probabilistic Systems in the Presence of Modeling Uncertainties
Alberto Puggelli

Citation
Alberto Puggelli. "Formal Techniques for the Verification and Optimal Control of Probabilistic Systems in the Presence of Modeling Uncertainties". PhD thesis, University of California, Berkeley, August, 2014.

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, non-modeled 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 (Convex-MDPs) as the modeling framework to represent the behavior of stochastic systems. Convex-MDPs generalize MDPs by expressing state-transition probabilities not only with fixed realization frequencies but also with non-linear 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 Convex-MDPs. 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 state-transition 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 model-checking algorithm for PCTL properties of Convex-MDPs, and prove that it runs in time polynomial in the size of the model under analysis. The developed algorithm is the first known polynomial-time algorithm for the verification of PCTL properties of Convex-MDPs. This result allows us to lower the previously known algorithmic complexity upper bound for Interval-MDPs from co-NP to P, and it is valid also for the more expressive (convex) uncertainty models supported by the Convex-MDP formalism. We apply the proposed framework and model-checking 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 Convex-MDPs, 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 state-transition 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 state-transition probabilities does not increase the theoretical complexity of the synthesis problem, which remains in the class NP-complete as the analogous problem applied to MDPs, i.e., when all transition probabilities are known with certainty. We then interpret the strategy-synthesis problem as a constrained optimization problem and propose the first sound and complete algorithm to solve it. We apply the developed strategy-synthesis algorithm to the problem of generating optimal energy pricing and purchasing strategies for a for-profit 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 quality-of-service for the users. We use Convex-MDPs to model the decision-making 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.

Electronic downloads

Citation formats  
  • HTML
    Alberto Puggelli. <a
    href="http://www.terraswarm.org/pubs/354.html"
    ><i>Formal Techniques for the Verification and
    Optimal Control of Probabilistic Systems in the Presence of
    Modeling Uncertainties</i></a>, PhD thesis, 
    University of California, Berkeley, August, 2014.
  • Plain text
    Alberto Puggelli. "Formal Techniques for the
    Verification and Optimal Control of Probabilistic Systems in
    the Presence of Modeling Uncertainties". PhD thesis, 
    University of California, Berkeley, August, 2014.
  • BibTeX
    @phdthesis{Puggelli14_FormalTechniquesForVerificationOptimalControlOfProbabilistic,
        author = {Alberto Puggelli},
        title = {Formal Techniques for the Verification and Optimal
                  Control of Probabilistic Systems in the Presence
                  of Modeling Uncertainties},
        school = {University of California, Berkeley},
        month = {August},
        year = {2014},
        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, non-modeled 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 (Convex-MDPs) as the
                  modeling framework to represent the behavior of
                  stochastic systems. Convex-MDPs generalize MDPs by
                  expressing state-transition probabilities not only
                  with fixed realization frequencies but also with
                  non-linear 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 Convex-MDPs. 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
                  state-transition 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 model-checking algorithm for PCTL
                  properties of Convex-MDPs, and prove that it runs
                  in time polynomial in the size of the model under
                  analysis. The developed algorithm is the first
                  known polynomial-time algorithm for the
                  verification of PCTL properties of Convex-MDPs.
                  This result allows us to lower the previously
                  known algorithmic complexity upper bound for
                  Interval-MDPs from co-NP to P, and it is valid
                  also for the more expressive (convex) uncertainty
                  models supported by the Convex-MDP formalism. We
                  apply the proposed framework and model-checking
                  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
                  Convex-MDPs, 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 state-transition 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 state-transition
                  probabilities does not increase the theoretical
                  complexity of the synthesis problem, which remains
                  in the class NP-complete as the analogous problem
                  applied to MDPs, i.e., when all transition
                  probabilities are known with certainty. We then
                  interpret the strategy-synthesis problem as a
                  constrained optimization problem and propose the
                  first sound and complete algorithm to solve it. We
                  apply the developed strategy-synthesis algorithm
                  to the problem of generating optimal energy
                  pricing and purchasing strategies for a for-profit
                  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 quality-of-service for the users. We
                  use Convex-MDPs to model the decision-making
                  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. },
        URL = {http://terraswarm.org/pubs/354.html}
    }
    

Posted by Alberto Puggelli on 1 Sep 2014.
Groups: tools

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.