In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one ...

Algorithms for model checking and satisfiability of the modal μ -calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and ...

There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a ...

In recent years, there has been an increasing interest in the connections between supervisory control theory and reactive synthesis. As the two fields use similar techniques there is great hope that technologies from one ...

Emerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be ...

We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph G=(V,E) and a set of fair moves E_f a subset of E a player is said ...

We propose a method for solving parity games with acyclic (DAG) sub-structures by computing nested fixpoints of a DAG attractor function that lives over the non-DAG parts of the game, thereby restricting the domain of the ...

We report on COOL-MC, a model checking tool for fixpoint logics that is parametric in the branching type of models (non-deterministic, game-based, probabilistic etc.) and in the next-step modalities used in formulae. The ...