The paper provides a synthesis between two main approaches to automatic verification of finite-state systems: temporal logic model checking and language containment of automata on infinite tapes. A new branching-time temporal logic is suggested, in which automata on infinite tapes are used to define new temporal operators. Each such operator defines a set of acceptable computation paths. Path quantifiers are used to specify whetherallpaths orsomepath from a state should be in some acceptable set. The logic is very powerful and includes both linear-time and branching-time temporal logics. We give an efficient model checking procedure that checks whether a finite-state system satisfies its specification, given by a formula of the new logic. Our procedure is linear in the size of the system and a low level polynomial in the size of the specification.
展开▼
