Techniques for Temporal Logic Model Checking

摘要

Several books have been published on the subject of model checking: [141] presents an automata-based approach to model checking that underpins his verification tool COSPAN; [66] is a thorough overview of classic model-checking techniques with an emphasis on CTL model-checking; [24] describes the basis of model checking: transition systems as a model of systems, temporal logic as language for requirements, and model checking as verification algorithms.