书籍介绍
Model checking领域的权威书籍
精彩摘录
- "There are two types of formulas in CTL*: state formulas(which are true in a specific state) and path formulas (which are true along a specific path)"
- "Computation Tree Logic (CTL) is a restricted subset of CTL* in which each of the temporal operators X, F, G, U and R must be immediately preceded by a path quantifier."
- "Linear Temporal Logic(LTL),on the other hand, will consist of formulas that have the form A f where f is path formula in which the only state subformulas permitted are atomic propositions"
用户评论
模型检测的入门，由Clarke大牛领衔著书再合适不过了。
Clarke，图灵奖得主，这本书很经典，值得每一个做推理和验证相关，甚至每一个做计算机理论的人认真读
模型检查的入门读物，但是语言偏晦涩
This is an excellent book for the introduction of model checking. From my view point, there is still a lot of space for improvement on teaching model checking. Model checking is a very simple problem on how to explore the huge space. This book tells the solutions, but does not tell how people find out these solutions.
The MIT Press的其他书籍查看全部
Essentials of Compilation
Make it Clear
An Introduction to Statistical Genetic Data Analysis
Cloud Computing for Machine Learning and Cognitive Applications
Introduction to Computation and Programming Using Python (2/e)
How Not to Network a Nation
收藏