Institute for Informatics
Georg-August-Universität Göttingen

Databases and Information Systems

Uni Göttingen

International Conference on Analytic Tableaux and Related Methods (TABLEAUX'97),
Pont-ā-Mousson, France, May 13-16, 1997. LNCS 1227, Springer, pp. 261-275.

Proving Correctness of Labeled Transition Systems by Semantic Tableaux

Wolfgang May


The paper presents a method for formally proving correctness of processes specified by transition systems which is based on a tableau calculus for an extended temporal logic. The model-theoretic semantics is given by labeled Kripke structures, incorporating information about the actions performed in transitions. Extending first-order CTL for handling action labels, the multi-modal logic MCTL is defined which is well-suited for specifying transition systems and their properties. For MCTL, a tableau semantics and -calulus is presented, allowing formal verification.