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.

[PS-File]
[Slides]