The Theory of Timed I/O Automata, Second Edition / Synthesis Lectures on Distributed Computing Theory (PDF)

"FLP" impossibility result for distributed consensus in the presence of process failures (with Fischer and Paterson), the "DLS" algorithms for stabilizing fault-tolerant consensus (with Dwork and Stockmeyer), and the I/O automata mathematical modeling frameworks (with Tuttle, Vaandrager, Segala, and Kaynar). Prior to this monograph, she wrote two books: on "Atomic Transactions" (with Merritt, Weihl, and Fekete) and on "Distributed Algorithms." She is a member of the National Academy of Engineering and the American Academy of Arts and Sciences,and is an ACM Fellow. She is a winner of several prizes for her work in distributed computing theory, including the Dijkstra Prize (2001 and 2007), the van Wijngaarden Prize (2006), the Knuth Prize (2007), and the IEEE Piore Prize (2010). Roberto Segala is a Professor at the University of Verona, Italy, and heads the Formal Models and Verification group at the Department of Computer Science. Prior to joining the University of Verona in 2001,he was research associate at the University of Bologna.He received his Laurea in Computer Science from the University of Pisa as a student of the Scuola Normale Superiore, and his Masters and PhD in Computer Science from MIT. As part of his PhD work, he made contributions to the theory of liveness and receptiveness for real-time systems and he designed the model of Probabilistic Automata for the formal analysis of randomized distributed algorithms. After that, he worked with Lynch, Kaynar, Vaandrager and others on the hybrid extension of the I/O automata framework. He also worked on model checking of probabilistic real-time systems, contributing to the design of some of the algorithms used in the PRISM model checker. One of his long-term goals is to design a general mathematical model that can be used for the description and analysis of systems that exhibit stochastic hybrid behavior. Frits Vaandrager is a Professor at the Radboud University Nijmegen, the Netherlands, within the Institute of Computing and Information Sciences.Prior to joining the Radboud University in 1995, he was group leader at the CWI in Amsterdam and held postdoctoral positions at MIT in the group of Nancy Lynch, and in the group of Gerard Berry at the Ecole Nationale Superieure des Mines in Sophia-Antipolis. He received his M.S. degree in Mathematics from the University of Leiden, and his PhD in Computer Science from the University of Amsterdam. As part of his PhD work, he made major contributions to the general theory of structural operational semantics. After that he worked with Lynch, Segala, Kaynar, and others on the theory and applications of the I/O automata framework. He has been and is involved in a large number of projects in which formal verification and model checking technology is applied to tackle practical problems from industrial partners. His group has been and is closely involved in the use and development of the timed automata model checker Uppaal. In part due to these efforts, Uppaalis now routinely used for industrial case studies and has thousands of users, both in academia and industry.