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". Tutorial, 15, May, 2014; Bio: Alberto Puggelli received the B.Sc. degree and the double M.Sc. degree in Electrical Engineering (summa cum laude) from Polytechnic of Milan and from Polytechnic of Turin, Italy, in 2006 and 2008, respectively. In 2009, he was with ST-Ericsson as an intern analog designer. In 2009, he joined the EECS department at the University of California at Berkeley, where he is currently pursuing the Ph.D. degree. From 2011 to 2013, he hold intern positions in the R&D and product divisions at Texas Instruments (Kilby Labs) and Lion Semiconductor. Alberto is the recipient of two Best Student awards at Polytechnic of Milan, the AEIT fellowship entitled to "Isabella Sassi Bonadonna" for the year 2010, and the 2012 Margarida Jacome GSRC Best Poster Award. He also serves as a reviewer for the Journal of Solid State Circuits (JSSC) and the Transactions on Circuit and Systems II (TCAS-II). His research interests include methodologies for the design of energy-efficient SoCs and techniques for the formal verification of nonlinear and stochastic hybrid systems.

Abstract
Accurate modeling of cyber-physical systems (CPSs) is a notoriously challenging problem due, among other reasons, to the intrinsic limitations in representing the physical part of the system, whose behavior can only be inferred through a finite number of finite resolution measurements. The problem is even exacerbated in the context of the formal verification and optimal control of these systems, where the generated guarantees on the system properties and control strategies are only as accurate as the model itself. In this talk, we present a framework that allows the formal verification of quantitative properties of CPSs and the generation of robust control strategies for these systems, while taking into account uncertainties in the modeling process. We first present the model of Convex Markov Decision Processes (CMDPs), i.e., MDPs in which transition probabilities are only known to lie in convex uncertainty sets. These convex sets can be used to formally capture the uncertainties that are present in the modeling process. Using results on strong duality for convex programs, we then present the first provably-polynomial verification algorithm for Probabilistic Computation Tree (PCTL) properties of CMDPs. Further, we present a novel algorithm for the synthesis of robust control strategies for CMDPs. The synthesized strategy optimizes a desired cost function and is guaranteed to satisfy a given specification expressed in PCTL. We conclude the talk by describing how we recently applied the proposed techniques to the verification of the behavior of car drivers performing complex maneuvers, and to the problem of generating optimal energy pricing and dispatch strategies in smart-grids that integrate renewable energy sources.

Electronic downloads


Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.
Citation formats  
  • HTML
    Alberto Puggelli. <a
    href="http://www.terraswarm.org/pubs/248.html"
    ><i>Formal Techniques for the Verification and
    Optimal Control of Probabilistic Systems in the Presence of
    Modeling Uncertainties</i></a>, Tutorial,  15,
    May, 2014; Bio: Alberto Puggelli received the B.Sc. degree
    and the double M.Sc. degree in Electrical Engineering (summa
    cum laude) from Polytechnic of Milan and from Polytechnic of
    Turin, Italy, in 2006 and 2008, respectively. In 2009, he
    was with ST-Ericsson as an intern analog designer. In 2009,
    he joined the EECS department at the University of
    California at Berkeley, where he is currently pursuing the
    Ph.D. degree. From 2011 to 2013, he hold intern positions in
    the R&D and product divisions at Texas Instruments
    (Kilby Labs) and Lion Semiconductor. Alberto is the
    recipient of two Best Student awards at Polytechnic of
    Milan, the AEIT fellowship entitled to "Isabella Sassi
    Bonadonna" for the year 2010, and the 2012 Margarida
    Jacome GSRC Best Poster Award. He also serves as a reviewer
    for the Journal of Solid State Circuits (JSSC) and the
    Transactions on Circuit and Systems II (TCAS-II). His
    research interests include methodologies for the design of
    energy-efficient SoCs and techniques for the formal
    verification of nonlinear and stochastic hybrid systems.
  • Plain text
    Alberto Puggelli. "Formal Techniques for the
    Verification and Optimal Control of Probabilistic Systems in
    the Presence of Modeling Uncertainties". Tutorial,  15,
    May, 2014; Bio: Alberto Puggelli received the B.Sc. degree
    and the double M.Sc. degree in Electrical Engineering (summa
    cum laude) from Polytechnic of Milan and from Polytechnic of
    Turin, Italy, in 2006 and 2008, respectively. In 2009, he
    was with ST-Ericsson as an intern analog designer. In 2009,
    he joined the EECS department at the University of
    California at Berkeley, where he is currently pursuing the
    Ph.D. degree. From 2011 to 2013, he hold intern positions in
    the R&D and product divisions at Texas Instruments
    (Kilby Labs) and Lion Semiconductor. Alberto is the
    recipient of two Best Student awards at Polytechnic of
    Milan, the AEIT fellowship entitled to "Isabella Sassi
    Bonadonna" for the year 2010, and the 2012 Margarida
    Jacome GSRC Best Poster Award. He also serves as a reviewer
    for the Journal of Solid State Circuits (JSSC) and the
    Transactions on Circuit and Systems II (TCAS-II). His
    research interests include methodologies for the design of
    energy-efficient SoCs and techniques for the formal
    verification of nonlinear and stochastic hybrid systems.
  • BibTeX
    @tutorial{Puggelli14_FormalTechniquesForVerificationOptimalControlOfProbabilistic,
        author = {Alberto Puggelli},
        title = {Formal Techniques for the Verification and Optimal
                  Control of Probabilistic Systems in the Presence
                  of Modeling Uncertainties},
        day = {15},
        month = {May},
        year = {2014},
        note = {Bio: Alberto Puggelli received the B.Sc. degree
                  and the double M.Sc. degree in Electrical
                  Engineering (summa cum laude) from Polytechnic of
                  Milan and from Polytechnic of Turin, Italy, in
                  2006 and 2008, respectively. In 2009, he was with
                  ST-Ericsson as an intern analog designer. In 2009,
                  he joined the EECS department at the University of
                  California at Berkeley, where he is currently
                  pursuing the Ph.D. degree. From 2011 to 2013, he
                  hold intern positions in the R\&D and product
                  divisions at Texas Instruments (Kilby Labs) and
                  Lion Semiconductor. Alberto is the recipient of
                  two Best Student awards at Polytechnic of Milan,
                  the AEIT fellowship entitled to "Isabella Sassi
                  Bonadonna" for the year 2010, and the 2012
                  Margarida Jacome GSRC Best Poster Award. He also
                  serves as a reviewer for the Journal of Solid
                  State Circuits (JSSC) and the Transactions on
                  Circuit and Systems II (TCAS-II). His research
                  interests include methodologies for the design of
                  energy-efficient SoCs and techniques for the
                  formal verification of nonlinear and stochastic
                  hybrid systems.},
        abstract = {Accurate modeling of cyber-physical systems (CPSs)
                  is a notoriously challenging problem due, among
                  other reasons, to the intrinsic limitations in
                  representing the physical part of the system,
                  whose behavior can only be inferred through a
                  finite number of finite resolution measurements.
                  The problem is even exacerbated in the context of
                  the formal verification and optimal control of
                  these systems, where the generated guarantees on
                  the system properties and control strategies are
                  only as accurate as the model itself. In this
                  talk, we present a framework that allows the
                  formal verification of quantitative properties of
                  CPSs and the generation of robust control
                  strategies for these systems, while taking into
                  account uncertainties in the modeling process. We
                  first present the model of Convex Markov Decision
                  Processes (CMDPs), i.e., MDPs in which transition
                  probabilities are only known to lie in convex
                  uncertainty sets. These convex sets can be used to
                  formally capture the uncertainties that are
                  present in the modeling process. Using results on
                  strong duality for convex programs, we then
                  present the first provably-polynomial verification
                  algorithm for Probabilistic Computation Tree
                  (PCTL) properties of CMDPs. Further, we present a
                  novel algorithm for the synthesis of robust
                  control strategies for CMDPs. The synthesized
                  strategy optimizes a desired cost function and is
                  guaranteed to satisfy a given specification
                  expressed in PCTL. We conclude the talk by
                  describing how we recently applied the proposed
                  techniques to the verification of the behavior of
                  car drivers performing complex maneuvers, and to
                  the problem of generating optimal energy pricing
                  and dispatch strategies in smart-grids that
                  integrate renewable energy sources. },
        URL = {http://terraswarm.org/pubs/248.html}
    }
    

Posted by Barb Hoversten on 29 Jan 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.