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 ...

This thesis explores the role of consensing, a process of cognitive consensus-building through the mechanisms of sensing and synthesizing, in digital transformation strategy formulation within the Swedish public sector. ...

The pervasive integration of Artificial Intelligence (AI) in society presents both opportunities and challenges, with the black-box issue emerging as a significant obstacle in realizing the full potential of AI. The ...

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 demonstrate a novel methodology that integrates intuitive modelling, simulation, and formal verification of collective behaviour in biological systems. To that end, we consider the case of a colony of foraging ants, ...

We study the reactive synthesis problem for distributed systems with an unbounded number of participants interacting with an uncontrollable environment. Executions of those systems are modeled by data words, and specifications ...

Background: Large Language Models (LLMs) offer users natural language interaction, technical insights and task automation capabilities. However, the systematic integration of LLMs within Requirements Engineering ...

Background: Accurate pedestrian behavior prediction is essential for reducing fatalities from pedestrian-vehicle collisions. Machine learning can support automated vehicles to better understand pedestrian behavior in complex ...

Linear temporal logic (LTL) is a popular language in formal verification, especially in the domains of model checking and reactive synthesis. Because its semantics is defined in terms of infinite sequences of symbols ...