InhaltsangabeI: Models of Concurrency.- 1: Basic Models.- 1.1 The Generic Model.- 1.2 Model 1: Transition Diagrams.- 1.3 Model 2: Shared-Variables Text.- 1.4 Semantics of Shared-Variables Text.- 1.5 Structural Relations Between Statements.- 1.6 Behavioral Equivalence.- 1.7 Grouped Statements.- 1.8 Semaphore Statements.- 1.9 Region Statements.- 1.10 Model 3: Message-Passing Text.- 1.11 Model 4: Petri Nets.- Problems.- Bibliographic Notes.- 2: Modeling Real Concurrency.- 2.1 Interleaving and Concurrency.- 2.2 Limiting the Critical References.- 2.3 Justice (Weak Fairness).- 2.4 Implications of the Justice Requirements.- 2.5 Compassion (Strong Fairness).- 2.6 Synchronization Statements.- 2.7 Communication Statements.- 2.8 Summary: Fair Transition Systems.- 2.9 Fairness in Petri Nets.- 2.10 Semantic Considerations of Fairness.- Problems.- Bibliographic Notes.- II: Specifications.- 3: Temporal Logic.- 3.1 State Formulas.- 3.2 Temporal Formulas: Future Operators.- 3.3 Temporal Formulas: Past Operators.- 3.4 Basic Properties of the Temporal Operators.- 3.5 A Proof System.- 3.6 Axioms for a Proof System.- 3.7 Basic Inference Rules.- 3.8 Derived Inference Rules.- 3.9 Equality and Quantifiers.- 3.10 From General Validity to Program Validity.- Problems.- Bibliographic Notes.- 4: Properties of Programs.- 4.1 The Local Language.- 4.2 The Classification of Properties.- 4.3 Examples of Safety: State Invariances.- 4.4 Examples of Safety: Past Invariances.- 4.5 Examples of Progress Properties: From Guarantee to Reactivity.- 4.6 Example: A Resource Allocator.- 4.7 Expressivity of the Specification Language.- 4.8 Specification of Reactive Modules.- 4.9 Composing Modular Specifications.- Problems.- Bibliographic Notes.- References.- Index to Symbols.- General Index.