Formal methods for discrete-time dynamical systems (Q2012356)

The book presents an introduction to the concept of characterizing discrete-time dynamical systems through the use of transition systems and temporal logic. This novel approach has been the cutting edge in the analysis of control systems the last decades, and this book is an excellent choice for readers being introduced to the concept. By providing the required background from the fields of dynamical systems and also formal methods, this textbook can introduce researchers from both fields to the concept of integrating formal methods and control, building up from introductory material to more advanced concepts. Thus, this work is suitable both for researchers from these fields, and also young graduates, provided they are familiar with fundamental concepts of systems theory and theoretical computer science. A strong feature of this work is its plethora of examples, which greatly help in understanding the presented theory, and also help the reader get an idea for the applications that can be considered. Part I is the introductory part of the book and presents transition systems, which are used to represent dynamical systems. Finite abstractions of systems are defined, along with simulation and bisimulation relations. Linear temporal logic and finite automata are also introduced. Part II develops model checking techniques and finite temporal logic control. Part III takes up the largest portion of the book, and is devoted to various control problems for discrete time dynamical systems, starting from the largest satisfying region and building up to advanced problems like language guided controller synthesis and optimal temporal logic control.