##
**Verification and control of hybrid systems. A symbolic approach. Foreword by Rajeev Alur.**
*(English)*
Zbl 1195.93001

New York, NY: Springer (ISBN 978-1-4419-0223-8/hbk; 978-1-4419-0224-5/ebook). xv, 202 p. (2009).

The rapidly growing and interdisciplinary research demands that researchers must understand concepts and tools from both computer science and control theory. This is undoubtedly a daunting task, and this is where this book can come to the rescue. It covers a wide range of foundational topics in verification and control of hybrid systems. More impressively, it thematically weaves them together using the recurring theme of simulation relations. The notion of a simulation or a bisimulation relation between two descriptions of a system, possibly at different levels of detail, has proved to be an important concept, both in theory and practice, for modeling and verification of discrete systems. Using richer concepts such as alternating relations and approximate relations, this book develops the foundations for hybrid control systems.

The book is divided into four parts. The first part presents basic concepts centered around a notion of system that is general enough to describe finite-state machines, differential equations, and hybrid systems. However, a system, by itself, is not very interesting. More interesting are the ways in which systems relate to other systems. Two such relationships are presented in Part II: behavioral inclusion/equivalence and simulation/bisimulation. These relationships are then used to study verification and control synthesis problems for finite-state systems. Only a flavor of the existing results is provided since the focus of the book are the infinite-state (hybrid) systems discussed in Part III and Part IV. By drawing inspiration from times automata, several classes of hybrid systems with richer continuous dynamics are shown to be related to finite-state symbolic systems in Part III. Once such (bi)simulation relations are established, verification and control synthesis problems can be immediately solved by resorting to the techniques described in Part II for finite-state systems. The same stategy is followed in Part IV by generalizing (bi)simulation relationships to approximate (bi)simulation relationships that can be used for wider classes of hybrid systems.

This book will be useful for researchers, engineers, computer scientists, and graduate students in the areas of formal methods, verification, model checking, and control.

The book is divided into four parts. The first part presents basic concepts centered around a notion of system that is general enough to describe finite-state machines, differential equations, and hybrid systems. However, a system, by itself, is not very interesting. More interesting are the ways in which systems relate to other systems. Two such relationships are presented in Part II: behavioral inclusion/equivalence and simulation/bisimulation. These relationships are then used to study verification and control synthesis problems for finite-state systems. Only a flavor of the existing results is provided since the focus of the book are the infinite-state (hybrid) systems discussed in Part III and Part IV. By drawing inspiration from times automata, several classes of hybrid systems with richer continuous dynamics are shown to be related to finite-state symbolic systems in Part III. Once such (bi)simulation relations are established, verification and control synthesis problems can be immediately solved by resorting to the techniques described in Part II for finite-state systems. The same stategy is followed in Part IV by generalizing (bi)simulation relationships to approximate (bi)simulation relationships that can be used for wider classes of hybrid systems.

This book will be useful for researchers, engineers, computer scientists, and graduate students in the areas of formal methods, verification, model checking, and control.

Reviewer: Alexander O. Ignatyev (Donetsk)

### MSC:

93-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to systems and control theory |

93C83 | Control/observation systems involving computers (process control, etc.) |

68-01 | Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science |