New frontiers for Linear Temporal Logic

Add to your list(s) Download to your calendar using vCal

• Eric Koskinen (University of Cambridge)
• Monday 22 March 2010, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

We describe a new algorithm for proving linear temporal properties of infinite-state systems. Our approach takes advantage of the fact that branching-time proof methods can sometimes be used to prove linear-time properties more efficiently than standard linear-time techniques can. The caveat is that, in certain instances, nondeterminism in the transition relation can cause branching-time methods to report counterexamples that are spurious in the linear-time semantics. To address this problem we describe an algorithm that, as it attempts to apply branching-time proof methods, finds and then removes problematic non-determinism via an analysis on the spurious counterexamples. Problematic nondeterminism is characterized using predicates, and removed using a predicate-based partial determinization procedure. Our method is sound and relatively complete.We demonstrate that our method can yield orders of magnitude performance improvements over native linear-time methods.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.