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