5. Principles of Model Checking. Baier_ Joost (2008) (5. Principles of Model Checking. Baier_ Joost (2008).pdf), страница 2

. . . . . . . . . . . . . . . . . . . . . . . .6.2 Computation Tree Logic . . . . . . . . . . . . . . . . . . . . .6.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . .6.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . .6.2.3 Equivalence of CTL Formulae . . . . . . . . . . .

. . .6.2.4 Normal Forms for CTL . . . . . . . . . . . . . . . . .6.3 Expressiveness of CTL vs. LTL . . . . . . . . . . . . . . . . .6.4 CTL Model Checking . . . . . . . . . . . . . . . . . . . . . .6.4.1 Basic Algorithm . . . . . . . . . . . . . . . . . . . . .6.4.2 The Until and Existential Always Operator . . . . . .6.4.3 Time and Space Complexity .

. . . . . . . . . . . . . .6.5 Fairness in CTL . . . . . . . . . . . . . . . . . . . . . . . . .6.6 Counterexamples and Witnesses . . . . . . . . . . . . . . . .6.6.1 Counterexamples in CTL . . . . . . . . . . . . . . . .6.6.2 Counterexamples and Witnesses in CTL with Fairness6.7 Symbolic CTL Model Checking . . . . . . .

. . . . . . . . . .6.7.1 Switching Functions . . . . . . . . . . . . . . . . . . .6.7.2 Encoding Transition Systems by Switching Functions .6.7.3 Ordered Binary Decision Diagrams . . . . . . . . . . .6.7.4 Implementation of ROBDD-Based Algorithms . .

. .6.8 CTL∗ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .6.8.1 Logic, Expressiveness, and Equivalence . . . . . . . . .6.8.2 CTL∗ Model Checking . . . . . . . . . . . . . . . . . .6.9 Summary . . . . . . . . . . . . . . . . . . . . .

. . . . . . . .6.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . . . . .6.11 Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . .................................................................................................................................................................................................................3133133173173203293323343413413473553583733763803813823863924074224224274304314337 Equivalences and Abstraction7.1 Bisimulation . .

. . . . . . . . . . . . . .7.1.1 Bisimulation Quotient . . . . . .7.1.2 Action-Based Bisimulation . . .7.2 Bisimulation and CTL∗ Equivalence . .7.3 Bisimulation-Quotienting Algorithms . .7.3.1 Determining the Initial Partition7.3.2 Refining Partitions . . . . . . . .........................................................449451456465468476478480....................................................................................xCONTENTS7.3.3 A First Partition Refinement Algorithm . .

. . .7.3.4 An Efficiency Improvement . . . . . . . . . . . .7.3.5 Equivalence Checking of Transition Systems . . .7.4 Simulation Relations . . . . . . . . . . . . . . . . . . . .7.4.1 Simulation Equivalence . . . . . . . . . . . . . .7.4.2 Bisimulation, Simulation, and Trace Equivalence7.5 Simulation and ∀CTL∗ Equivalence . . . . . . . . . . . .7.6 Simulation-Quotienting Algorithms .

. . . . . . . . . . .7.7 Stutter Linear-Time Relations . . . . . . . . . . . . . . .7.7.1 Stutter Trace Equivalence . . . . . . . . . . . . .7.7.2 Stutter Trace and LTL\ Equivalence . . . . . .7.8 Stutter Bisimulation . . . . . . . . . . . . . . . . . . . .7.8.1 Divergence-Sensitive Stutter Bisimulation . . . .7.8.2 Normed Bisimulation . . . . .

. . . . . . . . . . .7.8.3 Stutter Bisimulation and CTL∗\ Equivalence . .7.8.4 Stutter Bisimulation Quotienting . . . . . . . . .7.9 Summary . . . . . . . . . . . . . . . . . . . . . . . . . .7.10 Bibliographic Notes . . . . . . . . . . . . . . . . . . . . .7.11 Exercises . . . . . . . .

. . . . . . . . . . . . . . . . . .8 Partial Order Reduction8.1 Independence of Actions . . . . . . . . . .8.2 The Linear-Time Ample Set Approach . .8.2.1 Ample Set Constraints . . . . . . .8.2.2 Dynamic Partial Order Reduction8.2.3 Computing Ample Sets . . . . . .8.2.4 Static Partial Order Reduction . .8.3 The Branching-Time Ample Set Approach8.4 Summary . . . . .

. . . . . . . . . . . . .8.5 Bibliographic Notes . . . . . . . . . . . . .8.6 Exercises . . . . . . . . . . . . . . . . . ..................................................................................................................................................................................................................486487493496505510515521529530534536543552560567579580582................................................................................................................................................................5955986056066196276356506616616639 Timed Automata9.1 Timed Automata .

. . . . . . . . . . . . . . . . .9.1.1 Semantics . . . . . . . . . . . . . . . . . .9.1.2 Time Divergence, Timelock, and Zenoness9.2 Timed Computation Tree Logic . . . . . . . . . .9.3 TCTL Model Checking . . . . . . . . . . . . . . .9.3.1 Eliminating Timing Parameters . . . . . .9.3.2 Region Transition Systems . . . . . . . .9.3.3 The TCTL Model-Checking Algorithm . .9.4 Summary . .

. . . . . . . . . . . . . . . . . . . ........................................................................................................................................673677684690698705706709732738..............................CONTENTS9.59.6xiBibliographic Notes . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 739Exercises . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 74010 Probabilistic Systems10.1 Markov Chains . . . . . . . . . . . . . . . .10.1.1 Reachability Probabilities . . . . . .10.1.2 Qualitative Properties . . . . . . . .10.2 Probabilistic Computation Tree Logic . .

.10.2.1 PCTL Model Checking . . . . . . .10.2.2 The Qualitative Fragment of PCTL10.3 Linear-Time Properties . . . . . . . . . . .10.4 PCTL∗ and Probabilistic Bisimulation . . .10.4.1 PCTL∗ . . . . . . . . . . . . . . . .10.4.2 Probabilistic Bisimulation . . . . . .10.5 Markov Chains with Costs .

. . . . . . . . .10.5.1 Cost-Bounded Reachability . . . . .10.5.2 Long-Run Properties . . . . . . . . .10.6 Markov Decision Processes . . . . . . . . . .10.6.1 Reachability Probabilities . . . . . .10.6.2 PCTL Model Checking . . . . . . .10.6.3 Limiting Properties . . .

. . . . . .10.6.4 Linear-Time Properties and PCTL∗10.6.5 Fairness . . . . . . . . . . . . . . . .10.7 Summary . . . . . . . . . . . . . . . . . . .10.8 Bibliographic Notes . . . . . . . . . . . . . .10.9 Exercises . . . . . . . . . . . . . . . . . . .............................................................................................................................................................................................................................................................................................................................................................................................................745747759770780785787796806806808816818827832851866869880883894896899A Appendix: PreliminariesA.1 Frequently Used Symbols andA.2 Formal Languages . .

. . . .A.3 Propositional Logic . . . . . .A.4 Graphs . . . . . . . . . . . . .A.5 Computational Complexity ...........................................................................................909909912915920925Notations. . . . . .. .

. . . .. . . . . .. . . . . ...........Bibliography931Index965ForewordSociety is increasingly dependent on dedicated computer and software systems to assistus in almost every aspect of daily life. Often we are not even aware that computers andsoftware are involved. Several control functions in modern cars are based on embeddedsoftware solutions, e.g., braking, airbags, cruise control, and fuel injection. Mobile phones,communication systems, medical devices, audio and video systems, and consumer electronics in general are containing vast amounts of software.

Also transport, production, andcontrol systems are increasingly applying embedded software solutions to gain flexibilityand cost-efficiency.A common pattern is the constantly increasing complexity of systems, a trend which isaccelerated by the adaptation of wired and wireless networked solutions: in a moderncar the control functions are distributed over several processing units communicating overdedicated networks and buses. Yet computer- and software-based solutions are becoming ubiquitous and are to be found in several safety-critical systems.

Therefore a mainchallenge for the field of computer science is to provide formalisms, techniques, and toolsthat will enable the efficient design of correct and well-functioning systems despite theircomplexity.Over the last two decades or so a very attractive approach toward the correctness ofcomputer-based control systems is that of model checking. Model checking is a formalverification technique which allows for desired behavioral properties of a given system tobe verified on the basis of a suitable model of the system through systematic inspectionof all states of the model.

The attractiveness of model checking comes from the fact thatit is completely automatic – i.e., the learning curve for a user is very gentle – and that itoffers counterexamples in case a model fails to satisfy a property serving as indispensabledebugging information. On top of this, the performance of model-checking tools has longsince proved mature as witnessed by a large number of successful industrial applications.xiiixivForewordIt is my pleasure to recommend the excellent book Principles of Model Checking by Christel Baier and Joost-Pieter Katoen as the definitive textbook on model checking, providingboth a comprehensive and a comprehensible account of this important topic.

The bookcontains detailed and complete descriptions of first principles of classical Linear TemporalLogic (LTL) and Computation Tree Logic (CTL) model checking. Also, state-of-the artmethods for coping with state-space explosion, including symbolic model checking, abstraction and minimization techniques, and partial order reduction, are fully accountedfor. The book also covers model checking of real-time and probabilistic systems, importantnew directions for model checking in which the authors, being two of the most industriousand creative researchers of today, are playing a central role.The exceptional pedagogical style of the authors provides careful explanations of constructions and proofs, plus numerous examples and exercises of a theoretical, practicaland tool-oriented nature.