| 书目名称 | Verifying Temporal Properties of Systems | | 编辑 | Julian Charles Bradfield | | 视频video | | | 丛书名称 | Progress in Theoretical Computer Science | | 图书封面 |  | | 描述 | This monograph aims to provide a powerful general-purpose proof tech nique for the verification of systems, whether finite or infinite. It extends the idea of finite local model-checking, which was introduced by Stirling and Walker: rather than traversing the entire state space of a model, as is done for model-checking in the sense of Emerson, Clarke et ai. (checking whether a (finite) model satisfies a formula), local model-checking asks whether a particular state satisfies a formula, and only explores the nearby states far enough to answer that question. The technique used was a tableau method, constructing a tableau according to the formula and the local structure of the model. This tableau technique is here generalized to the infinite case by considering sets of states, rather than single states; because the logic used, the propositional modal mu-calculus, separates simple modal and boolean connectives from powerful fix-point operators (which make the logic more expressive than many other temporal logics), it is possible to give a rela tively straightforward set of rules for constructing a tableau. Much of the subtlety is removed from the tableau itself, and put into a relati | | 出版日期 | Book 1992 | | 关键词 | Finite; Invariant; calculus; logic; petri net; proof; verification | | 版次 | 1 | | doi | https://doi.org/10.1007/978-1-4684-6819-9 | | isbn_softcover | 978-1-4684-6821-2 | | isbn_ebook | 978-1-4684-6819-9 | | copyright | Julian Charles Bradfield 1992 |
The information of publication is updating
|
|
发表于 2025-3-21 17:37:03
