ABSTRACT. Reactive (Program) Synthesis is an area of Formal Methods that studies how to automatically synthesize interactive programs (reactive systems) from a human-readable specification, typically expressed in temporal logic. In this talk, we will discuss its use in Autonomous AI Systems to equip them with strategic reasoning capabilities, as well as frame such capabilities within formally specified bounds that provide guardrails for their self-deliberated behavior. We will show that Reactive Synthesis is related to certain forms of AI Planning in partially controllable environments and to MDP solving. Technically, we will focus on specifications expressed in Linear Temporal Logic (LTL) and, in particular, its finite-trace variants such as LTLf. A key advantage of these finite-trace variants is their simplicity, due to their reducibility to equivalent regular automata, which can be easily determinized and transformed into two-player games on graphs. This simplicity leads to an unprecedented computational effectiveness and scalability of synthesis in LTLf compared to LTL. Finally, we will also show how to lift this finite-trace "technology" to infinite traces by leveraging Manna and Pnueli’s safety-progress hierarchy for temporal properties, which is ultimately based on a finite-trace core.

ABSTRACT. Argumentation frameworks (AFs) provide a central formalism for abstract argumentation, representing arguments and their interactions as attack graphs and serving as reasoning engines across diverse domains. One of their main strengths lies in their ability to support explanations. However, their usefulness is often limited by size and structural complexity, which can hinder understanding. To address this challenge, we investigate simplification techniques for AFs, with particular emphasis on clustering-based abstraction. By grouping arguments into clusters and interpreting attacks in various manners, clustered AFs provide reduced representations that preserve essential argumentative properties while hiding redundant details. We study the formal underpinnings for clustering on AFs, analyze its effects on standard semantics, and explore conditions under which simplifications remain faithful and avoid spurious results. Our approach positions clustering as a principled method of abstraction and highlights its potential for enhancing explainability in argumentation.

ABSTRACT. Central reasoning tasks arising in computational argumentation are NP-hard. The field of knowledge compilation studies formal representations that permit efficient reasoning, which, however, have so far not found their way into mainstream research in computational argumentation. We study how to compile parts of argumentation frameworks (AFs)---a central representation for argumentative reasoning---to binary decision diagrams (BDDs) in search-based algorithms. We show promise of compilation in an experimental evaluation of the resulting algorithms, which incorporate multiple heuristics.

ABSTRACT. Fixed-parameter tractable (FPT) algorithms have been successfully applied to many intractable problems - with a focus on decision and optimization problems. Their aim is to confine the exponential explosion to some parameter, while the time complexity only depends polynomially on the instance size. In contrast, intractable enumeration problems have received comparatively little attention so far.

The goal of this work is to study how FPT decision algorithms could be turned into FPT enumeration algorithms. We thus inspect several fundamental approaches for designing FPT decision or optimization algorithms and we present ideas how they can be extended to FPT enumeration algorithms.

ABSTRACT. The guarded fluted (forward) fragment is the intersection of the guarded fragment and the fluted (forward) fragment of first-order logic. In this paper we showcase a simple and special model construction technique, which turns each first-order structure into a modal structure and back. Based on that, we devise a translation of the guarded fluted (forward) fragment to the basic modal logic extended with the universal modality, providing a simulation of the two guarded fragments as well as a new proof of the ExpTime-completeness of the satisfiability problem. Moreover, our technique induces a simpler unraveling construction for the two guarded fragments. As an application of the unraveling, we prove the Łoś–Tarski Preservation Theorem in the two fragments.

ABSTRACT. We initiate the study of the complexity-theoretic properties of convex logics in team semantics. We focus on the extension of classical propositional logic with the nonemptiness atom ne, a logic known to be both convex and union closed. We show that the satisfiability problem for this logic is NP-complete, that its validity problem is coNP-complete, and that its model-checking problem is in P.

ABSTRACT. We prove two (strong) undefinability results for logics based on inquisitive semantics (or its variant, team semantics). Namely: 1) we show that, in extended propositional inquisitive logic with tensor, intuitionistic implication is independent of the other connectives; 2) we show the undefinability of global disjunction in extended propositional dependence logic.

ABSTRACT. We study various notions of dependency in semiring team semantics. Semiring teams are essentially database relations, where each tuple is annotated with some element from a positive semiring. We consider semiring generalizations of several dependency notions from database theory and probability theory, including functional and inclusion dependencies, marginal identity, and (probabilistic) independence. We examine axiomatizations of implication problems, which are rule-based characterizations for the logical implication and inference of new dependencies from a given set of dependencies. Semiring team semantics provides a general framework, where different implication problems can be studied simultaneously for various semirings. The choice of the semiring leads to a specific semantic interpretation of the dependencies and hence different semirings offer a way to study different semantics (e.g., relational, bag, and probabilistic semantics) in a unified framework.