## Modal and Temporal Properties of ProcessesIn recent years, model checking has become an essential technique for the formal verification of systems. With a clarity of presentation and its many illuminating examples, this book makes this technical material easy to grasp. It is perfectly suited for an advanced undergraduate or graduate class in formal verification and will serve as a valuable resource to practitioners of formal methods. |

### What people are saying - Write a review

We haven't found any reviews in the usual places.

### Contents

1 | |

12 Concurrent interaction | 8 |

13 Observable transitions | 17 |

14 Renaming and linking | 21 |

15 More combinations of processes | 25 |

16 Sets of processes | 28 |

31 | |

21 HennessyMilner logic I | 32 |

46 Duality | 100 |

103 | |

51 Modal logic with fixed points | 104 |

52 Macros and normal formulas | 107 |

53 Observable modal logic with fixed points | 110 |

54 Preservation of bisimulation equivalence | 112 |

55 Approximants | 115 |

56 Embedded approximants | 121 |

22 HennessyMilner logic II | 36 |

23 Algebraic structure and modal properties | 39 |

24 Observable modal logic | 42 |

25 Observable necessity and divergence | 47 |

51 | |

32 Interactive games | 56 |

33 Bisimulation relations | 64 |

34 Modal properties and equivalences | 69 |

35 Observable bisimulations | 72 |

36 Equivalence checking | 77 |

83 | |

42 Processes and their runs | 85 |

43 The temporal logic CTL | 89 |

44 Modal formulas with variables | 91 |

45 Modal equations and fixed points | 95 |

57 Expressing properties | 128 |

133 | |

62 Property checking games | 135 |

63 Correctness of games | 144 |

64 CTL games | 147 |

65 Parity games | 151 |

66 Deciding parity games | 156 |

163 | |

71 Infinite state systems | 164 |

72 Generalising satisfaction | 165 |

73 Tableaux I | 168 |

74 Tableaux II | 173 |

References | 183 |

187 | |

### Other editions - View all

### Common terms and phrases

approximants Assume behaviour bisimilar bisimulation closed bisimulation equivalence contain Crossing defined definition example Exercises Figure finite state processes fixed point formula fixed point subformula fixed point variable flow graph free variables function game equivalent game G greatest fixed point history-free winning strategy image-finite induction hypothesis infinite length initial instance least fixed point limit ordinal modal formulas modal logic modal operators modal properties model checking monotonic function node observable actions observable bisimulation observable transition occurring infinitely ordinal parity game player V chooses player V wins position previous section process calculus proof Proposition Protocol Prove safety property set of processes Show silent activity slot machine subgoal sublogic subset subsumes successful tableau temporal logic tick tick)tt tick)Z transition graph transition relations transition rules User Userv2 valuation Ven3 vending machines vertex