View article

If we restrict our attention to finite state programs (variables and communication channels if any range over finite domains), then the whole program can be represented as a (generally large) finite graph. Each transition of this state graph is valued with the atomic action which has just changed the state. Consequently, a finite state program can be viewed as a finite model over which temporal formulas can be evaluated. Checking that a given finite model satisfies a given temporal formula is what one calls" model-checking". We consider the linear time version of temporal logic (LTL) and atomic propositions as actions [16]. Our terminology is no essential restriction and simplifies the transition to the automata framework we use thereafter. Models for linear logic are totally ordered computations. We restrict our attention to finite computations. Extension to the infinite case will be discussed. Classical model-checking as …