Talk by Martin Zimmermann

Martin Zimmermann will give his lecture on Tuesday, 8 July at 3:00 p.m. at JvF 25, Room 303 in Dortmund.

About the talk:

Title: Game-based Model-Checking of HyperLTL

Abstract: Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the $\forall^\exists^$-fragment has been presented. Here, we employ imperfect information-games to extend the game-based approach to full HyperLTL, i.e., to arbitrary quantifier prefixes. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperQPTL properties.

About the speaker:

Martin Zimmermann is an associate professor at the Distributed, Embedded and Intelligent Systems research group of the Department of Computer Science at Aalborg University. His main research interests are on temporal logics, the reactive synthesis problem, and automata theory. Before arriving in Aalborg, he was a lecturer at the Department of Computer Science at the University of Liverpool. Even before that, heI spent postdocs at the Reactive Systems Group at Saarland University and at the Institute of Informatics of the University of Warsaw. He did his PhD in Computer Science under the supervision of Wolfgang Thomas at RWTH Aachen University. Before that, Zimmermann studied Computer Science, also at RWTH Aachen University. During this time, he was a Fulbright student at DePaul University in Chicago.

More details can be found here.