Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:How to Win a First-Order Safety Game
Speaker:Helmut Seidl
coming from:TUM
Speakers Bio:Helmut Seidl graduated in Mathematics (1983) and received his Ph.D. degree in Computer Science (1986) from the Johann Wolfgang Goethe Universität, Frankfurt. He received his Dr. Habil. (1994) from the Universität des Saarlandes, Saarbrücken. 1994 he was appointed Full Professor at the University of Trier. Since 2003, he holds the chair for "Languages and Specification Formalisms" at TU München. From 2009 to 2018, he has been speaker of the research training group PUMA ("Programm- Und Modell-Analyse") and now is speaker of the research training group ConVeY ("Continuous Verification of CYber-Physical Systems"). His research interests include static analysis by abstract interpretation and model checking, efficient fixpoint algorithms, and expressive domains for numerical invariants. He has worked on dedicated analyses of concurrent and parametric systems, safety critical C programs, and cryptographic protocols. He is also interested in tree automata and corresponding classes of Horn clauses, in tree transducers and XML processing.
Event Type:SWS Distinguished Lecture Series
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Friday, 1 February 2019
Time:10:30
Duration:60 Minutes
Location:Kaiserslautern
Building:G26
Room:111
Abstract
First-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows. Desirable properties of these systems such as functional correctness or non-interference have conveniently been formulated as safety properties. Here, we go one step further. Our goal is to verify safety, and also to develop techniques for automatically synthesizing strategies to enforce safety. For that reason, we generalize FO transition systems to FO safety games. We prove that the existence of a winning strategy of safety player in finite games is equivalent to second-order quantifier elimination. For monadic games, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal invariants only. We identify a non-trivial sub-class where safety is decidable. For the general case, we provide meaningful abstraction and refinement techniques for realizing a CEGAR based synthesis loop.

Joint work with:
Christian Müller, TUM
Bernd Finkbeiner, Universität des Saarlandes

Contact
Name(s):Mouna Litz
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created:
Mouna Litz/MPI-SWS, 01/24/2019 12:51 PM
Last modified:
Uwe Brahm/MPII/DE, 02/01/2019 07:01 AM
  • Mouna Litz, 01/24/2019 12:59 PM -- Created document.