Monday 14 May, 15.00, talk on temporal logic, Denis Therien

Monday 14 May, 15.00, talk on temporal logic, Denis Therien
Title: Decidability questions in temporal logic
Speaker: Denis Therien (McGill; on leave at University of Tubingen)
Date and Time: Monday, May 14, 15.00 hours (sharp)
Location: Room P.327, Euclides Building, Plantage Muidergracht 24, Amsterdam

Abstract:
Linear temporal logic is the most fundamental formalism used in computer-aided verification for specifying properties of both hardware and software. Much attention has been devoted to classifying temporal properties according to their syntactical complexity. For example, one defines a fragment of the global logic, e.g. by restricting which operators are allowed, and then tries to understand the expressive power of that fragment. An important question is thus to decide for a given property if it is expressible or not in a given fragment. Such problems are in general very difficult to resolve. Recently, natural subclasses of temporal formulas have been algebraically characterized. We will survey some of these results. In particular, we will show that the levels of the Since/Until hierarchy are decidable, using algebraic methods.

For further information, please contact Yde Venema, yde@science.uva.nl.