Upcoming GroLog events are listed below. Past events can be found in the Archive page.

Clemens Kupke - 11 July 2024 - Constructing disjunctive formulas in the modal mu-calculus 

SPEAKER: Clemens Kupke (University of Strathclyde, Glasgow)

DATE: Thursday 11 July 2024

TIME: 16:00-17:00

PLACE: BernoulliBorg, room 5161.0289

TITLE: Constructing disjunctive formulas in the modal mu-calculus

ABSTRACT:  In this talk, I will discuss a key result about the modal mu-calculus: Every formula is equivalent to a so-called disjunctive formula. Constructing a disjunctive formula of "small" size is important e.g. for satisfiability checking. I am going to sketch a construction that yields a disjunctive formula that is single-exponential in the closure size of the input formula. The construction will highlight a few subtleties that arise when thinking about the size of a mu-calculus formula.

Based on joint work with Johannes Marti and Yde Venema.