BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:One-pass Tableaux for Computation Tree Logic - Rajeev Goré (Austr
 alian National University)
DTSTART:20070807T120000Z
DTEND:20070807T130000Z
UID:TALK7761@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We give the first single-pass ("on the fly") tableau decision 
 procedure for computational tree logic (CTL). Our method extends Schwendim
 ann's single-pass decision procedure for propositional linear temporal log
 ic (PLTL) but the extension is non-trivial because of the interactions bet
 ween the branching inherent in CTL-models\, which is missing in PLTL-model
 s\, and the "or" branching inherent in tableau search.  Our method extends
  to many other fix-point logics like propositional dynamic logic (PDL) and
  the logic of common knowledge (LCK).\n\nThe decision problem for CTL is k
 nown to be EXPTIME-complete\, but our procedure requires 2EXPTIME in the w
 orst case. A similar phenomenon occurs in extremely efficient practical si
 ngle-pass tableau algorithms for very expressive description logics with E
 XPTIME-complete decision problems because the 2EXPTIME worst-case behaviou
 r rarely arises.  Our method is amenable to the numerous optimisation meth
 ods invented for these description logics and has been implemented in the 
 Tableau Work Bench (twb.rsise.anu.edu.au} without these extensive optimisa
 tions.  Its one-pass nature also makes it amenable to parallel proof-searc
 h on multiple processors.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR