BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:New frontiers for Linear Temporal Logic - Eric Koskinen (Universit
 y of Cambridge)
DTSTART:20100322T124500Z
DTEND:20100322T140000Z
UID:TALK23900@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:We describe a new algorithm for proving linear temporal proper
 ties of\ninfinite-state systems. Our approach takes advantage of the fact 
 that\nbranching-time proof methods can sometimes be used to prove\nlinear-
 time properties more efficiently than standard linear-time\ntechniques can
 . The caveat is that\, in certain instances\,\nnondeterminism in the trans
 ition relation can cause branching-time\nmethods to report counterexamples
  that are spurious in the linear-time\nsemantics. To address this problem 
 we describe an algorithm that\, as\nit attempts to apply branching-time pr
 oof methods\, finds and then\nremoves problematic non-determinism via an a
 nalysis on the spurious\ncounterexamples.  Problematic nondeterminism is c
 haracterized using\npredicates\, and removed using a predicate-based parti
 al\ndeterminization procedure. Our method is sound and relatively\ncomplet
 e.We demonstrate that our method can yield orders of magnitude\nperformanc
 e improvements over native linear-time methods.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR