Markus Latte, A Decision Procedure for CTL* Based on Tableaux and Automata

Markus Latte,
A Decision Procedure for CTL* Based on Tableaux and Automata

We present a decision procedure for the full branching-time logic CTL* which is based on tableaux with global conditions on infinite branches. These conditions can be checked using automata-theoretic machinery. The decision procedure then consists of a doubly exponential reduction to the problem of solving a parity game. This has advantages over existing decision procedures for CTL*, in particular the automata-theoretic ones: the underlying tableau only works on subformulas of the input formula. The relationship between the structure of such tableaux and the input formula is given by very intuitive tableau rules.

Joint work with Oliver Friedmann and Martin Lange