(PDF 英文版)
by Christel Baier, Joost-Pieter Katoen, Kim Guldstrand Larsen
Hardcover: 975 pages
Publisher: The MIT Press (May 31, 2008)
ISBN-10: 026202649X
ISBN-13: 978-0262026499

The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties.

It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation.

The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.

详细介绍在此：http://mitpress.mit.edu/catalog/ ... ype=2&tid=11481