Formal Methods for Discrete-Time Dynamical Systems (Studies in Systems, Decision and Control, Band 89) - Softcover

Christos G. Cassandras, Ph.D., is a Distinguished Professor of Engineering at Boston University. He is Head of the Division of Systems Engineering, Professor of Electrical and Computer Engineering, and co-founder of Boston University's Center for Information and Systems Engineering (CISE). He received a B.S. from Yale University, a M.S.E.E from Stanford University, and S.M. and Ph.D. degrees from Harvard University. He specializes in the areas of discrete event and hybrid systems, cooperative control, stochastic optimization, and computer simulation, with applications to computer and sensor networks, manufacturing systems, and transportation systems. He has published over 450 refereed papers in these areas and six books. He has guest-edited several technical journal issues and serves on several journal editorial boards. In addition to his academic activities, he has worked extensively with industrial organizations on various systems integration projects and the development of decision-support software. He has most recently collaborated with MathWorks, Inc. in the development of the discrete event and hybrid system simulator SimEvents. Calin Belta, Ph.D, is a Professor in the Department of Mechanical Engineering at Boston University, where he holds the Tegan family Distinguished Faculty Fellowship. He is also the Director of the BU Robotics Lab. He received B.Sc. and M.Sc. degrees from the Technical University of Iasi and M.Sc. and Ph.D. degrees from the University of Pennsylvania. His research interests include dynamics and control theory, with particular emphasis on hybrid and cyber-physical systems, formal synthesis and verification, and applications in robotics and systems biology. He has received the Air Force Office of Scientific Research Young Investigator Award and the National Science Foundation CAREER Award. He is a Fellow and Distinguished Lecturer of IEEE.

This book bridges fundamental gaps between control theory and formal methods. Although it focuses on discrete-time linear and piecewise affine systems, it also provides general frameworks for abstraction, analysis, and control of more general models.

The book is self-contained, and while some mathematical knowledge is necessary, readers are not expected to have a background in formal methods or control theory. It rigorously defines concepts from formal methods, such as transition systems, temporal logics, model checking and synthesis. It then links these to the infinite state dynamical systems through abstractions that are intuitive and only require basic convex-analysis and control-theory terminology, which is provided in the appendix. Several examples and illustrations help readers understand and visualize the concepts introduced throughout the book.