*banner
 

Formal Methods for Dynamical Systems
Calin Belta

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

Citation formats  
  • 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.

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.

©2002-2018 Chess