International Conference on Analytic Tableaux and
Related Methods (TABLEAUX'97),
LNCS 1227, Springer,
Proving Correctness of Labeled Transition Systems by Semantic Tableaux
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
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.