Citation
Calin Belta. "Formal Methods for Dynamical Systems". Talk or presentation, 28, September, 2015.

Abstract
In control theory, complex models of physical processes, such as systems of differential equations, are usually checked against simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as languages and formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition graphs. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinite-space continuous and hybrid systems. However, provably correct but conservative approaches, in which the satisfaction of a property by a dynamical system is implied by the satisfaction of the property by a finite over-approximation (abstraction) of the system, have received a lot of attention in recent years. The focus of this talk is on discrete-time linear systems, for which it is shown that finite abstractions can be constructed through polyhedral operations only. By using techniques from model checking and automata games, this allows for verification and control from specifications given as Linear Temporal Logic (LTL) formulae over linear predicates in the state variables. The usefulness of these computational tools is illustrated with various examples.

Electronic downloads

• seminar.2015-09-28.Calin_Belta.pdf · application/pdf · 15955 kbytes

• HTML

  Calin Belta. <a
  href="http://chess.eecs.berkeley.edu/pubs/1118.html"
  ><i>Formal Methods for Dynamical
  Systems</i></a>, Talk or presentation,  28,
  September, 2015.

• Plain text

  Calin Belta. "Formal Methods for Dynamical
  Systems". Talk or presentation,  28, September, 2015.

• BibTeX

  @presentation{Belta15_FormalMethodsForDynamicalSystems,
      author = {Calin Belta},
      title = {Formal Methods for Dynamical Systems},
      day = {28},
      month = {September},
      year = {2015},
      abstract = {In control theory, complex models of physical
                processes, such as systems of differential
                equations, are usually checked against simple
                specifications, such as stability and set
                invariance. In formal methods, rich
                specifications, such as languages and formulae of
                temporal logics, are checked against simple models
                of software programs and digital circuits, such as
                finite transition graphs. With the development and
                integration of cyber physical and safety critical
                systems, there is an increasing need for
                computational tools for verification and control
                of complex systems from rich, temporal logic
                specifications. The formal verification and
                synthesis problems have been shown to be
                undecidable even for very simple classes of
                infinite-space continuous and hybrid systems.
                However, provably correct but conservative
                approaches, in which the satisfaction of a
                property by a dynamical system is implied by the
                satisfaction of the property by a finite
                over-approximation (abstraction) of the system,
                have received a lot of attention in recent years.
                The focus of this talk is on discrete-time linear
                systems, for which it is shown that finite
                abstractions can be constructed through polyhedral
                operations only. By using techniques from model
                checking and automata games, this allows for
                verification and control from specifications given
                as Linear Temporal Logic (LTL) formulae over
                linear predicates in the state variables. The
                usefulness of these computational tools is
                illustrated with various examples. },
      URL = {http://chess.eecs.berkeley.edu/pubs/1118.html}
  }
  

Posted by Sadigh Dorsa on 5 Oct 2015.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.