摘要：
Computation Tree Logic (CTL) is a logic of fundamental importance in
Computer Science. Model-checking is now a well-established method for
checking whether a given model satisfies a given formula. On the other
hand, practical methods for deciding whether a given formula is
CTL-satisfiable have not received much attention. The main obstacle is
that the problem of deciding CTL-satisfiability is known to be
EXPTIME-complete.

The traditional tableaux method for deciding CTL-satisfiability first
constructs a cyclic graph and then prunes nodes and edges in multiple
subsequent passes until the root node is pruned, indicating that the
given formula is CTL-unsatisfiable, or until no further pruning is
possible, indicating that the given formula is CTL-satisfiable.

We give the first single-pass tableau decision procedure for
CTL-satisfiability. Our method extends Schwendimann's single-pass
decision procedure for propositional linear temporal logic (PLTL) and
extends to many other fix-point logics like propositional dynamic
logic (PDL) and the logic of common knowledge (LCK).

Our method builds a rooted tree with ancestor cycles and often
outperforms the traditional method. In the worst case however, our
method may require 2EXPTIME. A similar phenomenon occurs in extremely
efficient practical single-pass tableau algorithms for very expressive
description logics with EXPTIME-complete decision problems because the
2EXPTIME worst-case behaviour rarely arises.  Our method is amenable
to the numerous optimisation methods invented for these description
logics and has been implemented in the Tableau Work Bench
(twb.rsise.anu.edu.au) without these extensive optimisations.

报告人： Pietro Abate, Rajeev Gore' and Florian Widmann
Logic and Computation Group
College of Engineering and Computer Science
The Australian National University
Canberra ACT 0200, Australia
Rajeev.Gore@anu.edu.au