University of Cambridge > Talks.cam > Semantics Lunch (Computer Laboratory) > New frontiers for Linear Temporal Logic

New frontiers for Linear Temporal Logic

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2021 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity