文章目录[隐藏]
Explicit-State Model Checking
Breadth-first Search
- X!y: add y as the last element of X
- X!!y: add y as the first element of X
- X?y: remove the first element of X as y
Depth-first Search
Nested Depth-First Search
- dfs from a reachable final state to check if a loop exists
Bitstate Hashing
Binary Decision Diagrams
- (X0 && ! X1) || (X0 && X1) == X0
- Boolean Function API
- A BDD represents a Boolean function as an acyclic directed graph
- Nonterminal vertices labeled by Boolean variables
- Leaf vertices labeled with the values 1 and 0
- Restrict(f,i,b):
- R(x1 && x2, 1, True) == x2
- …
BDD-based symbolic model checking
- represent sets of state
- represent transition relation
- p’: p of next state
- BddImage & BddPreImage
