Edmund M. Clark Jr. - Model Checking

Synchronous modulo 8 counter

Reachable states of Kripke structure for mutual exclusion example

Computation trees

Illustration of temporal operators

A Kripke structure that satisfies neither EXp nor EXp

The logic CTL* and its sublogics

Basic CTL operators

Counterexamples for LTL

Procedure for labeling the states satisfying E(f1Uf2)

Procedure for labeling the states satisfying EGf1

Microwave oven example

Procedure for computing least fixpoints

Procedure for computing greatest fixpoints

Illustration of the computation of the set of reachable states using the post image

Procedure for reachability analysis for checking AGp

Sequence of approximations for E(pUq)

Tableau for (heat) Uclose

The product P of the microwave M and the tableau T

Procedure for computing the set of states satisfying the CTL* formula g = Eg1

A finite automaton

An automaton for words with finitely many as

An automaton for an infinite number of as and an automaton for an infinite number of bs

An automaton for words with an infinite number of as and bs

The double DFS algorithm

7.6

Cases 2a and 2b in the proof of theorem 7.8

Transforming a Kripke structure into an automaton

A Bchi automaton specifying mutual exclusion

An eventuality property

A Bchi automaton constructed for the LTL formula (h) Uc

Splitting a node

Efficient translation of LTL to generalized Bchi automaton

Update the set Closed

Update and split

Split a node

Creating a successor

The Kripke structure resulting from algorithm EfficientLTLBuchi when given the formula (h) Uc

Binary decision tree for a twobit comparator

OBDD for a two-bit comparator with ordering a1< b1< a2< b2

OBDD for a two-bit comparator with ordering a1< a2< b1< b2

Twostate Kripke structure

Witness is in the first strongly connected component

Witness spans three strongly connected components

Relational product algorithm

Algorithm for variable elimination

Procedure for binary search for a satisfying assignment for a given CNF C, implemented using a recursive call

Search tree for equation 9.6 with traversal using decisions x1 0 and x2 1

Procedure for binary search for a satisfying assignment for a given CNF C, implemented using a trail

Algorithm for Boolean constraint propagation (BCP)

Implication graph for the clauses given as equation 9.8

Algorithm for computing a conflict clause

The resolution proof for justifying the conflict clause x3x5 generated by Analyze-Conflict for the implication graph given as

Application of bounded model checking (BMC)

Model with diameter 2

Model for illustration of the kinduction principle

A resolution proof for equation 10.10

Example for an application of McMillans interpolation system

10.6

Procedure for reachability checking using overapproximating postimage computation with Craig interpolation

Illustration of frames F0,,Fk, which are subsets of S, for k = 2

Main loop of propertydirected reachability (PDR)

Procedure for adding another frame in PDR

Procedure for removing counterexamples to induction in PDR

Propagation of clauses into other frames

Illustration of removal of counterexamples to induction, with k = 2

Unwinding preserves bisimulation

Duplication preserves bisimulation

Two nonbisimilar structures

Simulation equivalent structures that are not bisimilar

Executing three independent transitions

Depthfirst search with partial order reduction

Execution of independent transitions

Two stuttering-equivalent paths

Transition commutes with 01m

Two concurrent processes

Full and reduced state graph

Diagram illustrating problem 2

Full and reduced (thick lines) state graph for a mutual exclusion program

Code for checking condition C1 for the enabled transitions of a process