Verifying Temporal Properties of Systems

摘要: This monograph aims to provide a powerful general-purpose proof tech nique for the verification of systems, whether finite or infinite. It extends idea local model-checking, which was introduced by Stirling and Walker: rather than traversing entire state space model, as is done model-checking in sense Emerson, Clarke et ai. (checking (finite) model satisfies formula), asks particular formula, only explores nearby states far enough answer that question. The technique used tableau method, constructing according formula structure model. here generalized infinite case considering sets states, single states; because logic used, propositional modal mu-calculus, separates simple boolean connectives from fix-point operators (which make more expressive many other temporal logics), it possible give rela tively straightforward set rules tableau. Much subtlety removed itself, put into relation on defined tableau-the success then depends well-foundedness this relation. exhibited Petri nets, various standard notions net theory are shown playa part use nets-in particular, invariant calculus has major role."