Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2010 / Oberseminar / Markus Latte, A Decision Procedure for CTL* Based on Tableaux and Automata


Inhaltsbereich

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

TCS Oberseminar, 18.06.2010, 10.30 Uhr
Wann 10:30 12:00 18.06.2010
von bis
Wo L109
Termin übernehmen vCal
iCal

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

Artikelaktionen

abgelegt unter:

Funktionsleiste