Abstract
In this paper, we present a new consistency checking method for temporal logic specifications. The new method verifies consistency of a whole specification by using a tableau graph constructed from tableau graphs obtained on the verifications of partial specifications. The new method is applicable not only to on-the-fly verification, but also to comositional verification. By on-the-fly verification, we mean a verification that proceeds as a specification is evolved. Compositional verification is verification constructed by merging modular verifications. By verifying a specification at each step of its refinement, we can make specification evolution process efficient. A tableau graph constructed by a traditional tableau method does not suit reuse. The traditional tableau method has two phases; a tableau graph construction phase and eventuality checking phase. It is difficult to reflect the results of the eventuality checking on the tableau graph because there is no suitable substructre which can keep the results. For that reason, it is necessary to check eventuality formulae repeatedly on the reuse of the tableau graphs A tableau graph, introduced in this paper, has a new structure and is obtained by piling up tableau graphs of subformulae. In this new structure, the checked results of eventuality checking are encoded. Therefore, all the results of the verification in each step can be reused for constructing the verification for a whole specifcation.