USI - Email

Archive / INF Seminars / INF_2023_03_22_Philipp_Ruemmer

USI - Email

	Regular Model Checking Revisited

Host: Natasha Sharygina

Wednesday

22.03

USI Campus Est, room D1.14, Sector D

10:30 - 11:30


	Philipp Rümmer University of Regensburg, Germany and Uppsala University, Sweden

Abstract: Regular model checking, broadly construed, is the idea of reasoning about infinite-state systems using regular languages as symbolic representations. Regular model checking is a useful technique in particular for the analysis of parameterized systems, i.e., for checking properties of infinite families of finite-state systems, for instance self-stabilizing systems or various protocols. Regular model checking has been studied since the late 90s. In the talk, I will present a new formulation of regular model checking in terms of existential second-order logic over automatic structures. The formulation is general enough to capture many interesting correctness properties (e.8., safety, liveness, safety games, bisimulation), and can be turned into an effective analysis procedure by combination with methods from the automata learning area.

The talk presents joint work with Anthony W. Lin.

Biography: Philipp Rümmer is Professor in Theoretical Computer Science at the newly founded Department of Informatics and Data Science of the University of Regensburg, Germany. He also holds a position as Associate Professor at Uppsala University, Sweden. His research alternates between automated reasoning, SMT solving, formal methods, embedded systems, and various other topics.