ABSTRACT. We introduce a new planning problem with deterministic actions where a plan has to be computed for an instance when initial knowledge is incomplete. The automated planning community has developed a number of domain independent heuristics that facilitate search and help compute long plans. There are several research sub-areas related to planning and scheduling. In classical planning and conformant planning, it is assumed that there are finitely many named objects given in advance, and that only they can participate in actions and in fluents. This is the Domain Closure Assumption (DCA). However, there are realistic open-world deterministic planning problems where the set of initially given objects changes as planning proceeds: new objects are created, and old objects cease to exist. These problems are particularly challenging when knowledge is incomplete. We formulate the novel bounded proper planning (BPP) problem in first-order logic, assume an initial incomplete theory is a finite consistent set of fluent literals, consider a special form of weakly context free action theories, impose an integer upper bound on the length of the plan, and propose to organize search for a plan over sequences of actions that are grounded at planning time. In contrast to numeric planning problems, where each state is a finite set, in the BPP each state is associated with infinitely many infinitely sized first order models. We show how a planner can solve the BPP problem by using a domain-independent heuristic that guides search over sequences of actions. We propose a proof-of-concept implementation. We discuss the differences between our approach and the previously explored formulations of the automated planning problem.

ABSTRACT. We present plank, a practical toolkit for epistemic planning based on Dynamic Epistemic Logic (DEL), a well-known powerful semantics for reasoning about knowledge change. The toolkit has been developed with two audiences in mind: for more expert researchers, plank provides a rich set of features to assist in the development and testing of benchmarks written in EPDDL, a recent language to represent epistemic planning tasks; for less experienced practitioners, the toolkit offers several commands to manipulate, model-check and visualise epistemic states, thus facilitating the early learning process of the main theoretical constituents of DEL. In this paper, we briefly showcase the main features of our open-source software, and highlight the benefits of using plank to assist epistemic planning research.

ABSTRACT. Organizations rely on structured business processes to coordinate complex tasks. While business process management (BPM) has traditionally assumed full control over participants, also called agents, real processes involve autonomous decision-makers such as human workers and, increasingly, AI-based agents powered by, e.g., large language models. Agents are strategic reasoners that pursue individual goals, subject to a shared process specification constraining the joint execution, a modeling referred to as agentic BPM. We identify and formalize three fundamental settings of agentic BPM, for each of which we study four core problems, namely realizability, synthesis, model-checking, and guardrailing.

ABSTRACT. The video game industry continuously demands highly sophisticated, realistic, and autonomous Non-Player Characters (NPCs). While commercial game engines have historically approached AI from a strictly technical perspective, the core of video game logic remains largely distanced from formal Game Theory. Recently, formal methods have emerged to bridge this gap, recognizing games as Multi-Agent Systems. In our foundational work, we introduced a novel framework utilizing Alternating-time Temporal Logic (ATL) directly within a modern game engine. This paper reports the salient points of that offline-to-runtime architecture, provides a comparative analysis with recent formal developments, such as logics for imperfect information and natural strategic ability, and discusses future extensions, including Probabilistic ATL (PATL) and Neuro-Symbolic integration, to enhance the strategic reasoning of video game AI.

ABSTRACT. We present a formalisation of RTFD*, a multi-agent argumentation protocol, in the Run-Time Event Calculus (RTEC→), a stream reasoning engine with native support for events with delayed effects. Compared to the original specification of RTFD* in the action language C+, our formulation supports time windows for objections and efficient reasoning over high-velocity streams of agent messages, allowing us to handle more realistic argumentation scenarios. We report empirical results demonstrating low-latency monitoring of argumentation procedures at scale.

ABSTRACT. Multi-Agent Systems (MAS) require formalisms capable of handling partial and evolving information. While imperfect-information extensions of Alternating-time Temporal Logic (ATL) are highly expressive, they typically make model checking undecidable. This paper summarises \emph{Intuitionistic ATL} (IATL), an extension of ATL that replaces classical propositional truth with intuitionistic truth, capturing a novel, computationally tractable notion of imperfect information based on \emph{information refinement}. We review IATL's syntax and semantics over \emph{birelational concurrent game structures} (BCGS), the truth-monotonicity characterisation, and the PTIME-completeness of model checking, matching the complexity of classical ATL.

ABSTRACT. Generative AI systems are known to amplify biases present in their training data. While several inference-time mitigation strategies have been proposed, they remain largely empirical and lack formal guarantees. In this paper we introduce CTLF, a branching-time logic designed to reason about bias in series of generative AI outputs. CTLF adopts a counting worlds semantics where each world represents a possible output at a given step in the generation process and introduces modal operators that allow us to verify whether the current output series respects an intended probability distribution over a protected attribute, to predict the likelihood of remaining within acceptable bounds as new outputs are generated, and to determine how many outputs are needed to remove in order to restore fairness. We illustrate the framework on a toy example of biased image generation, showing how CTLF formulas can express concrete fairness properties at different points in the output series.

ABSTRACT. The expressive power of First-Order Logic (\FO) over infinite trees remains poorly understood. In particular, it is still an open problem whether one can decide if a given regular language of infinite (or finite) trees is definable in \FO. A common approach to better understand such formalisms is to provide alternative characterizations using, for example, automata or regular expressions; indeed, two automaton-based characterizations of \FO have recently been introduced. In this note, we return to a purely logical perspective to investigate the syntactic constraints required for the well-known modal $\mu$-calculus to precisely capture the expressiveness of \FO. We demonstrate that by employing the two-way modal $\mu$-calculus, we can identify the exact fragment corresponding to \FO. As a by-product, we obtain tight complexity results for the extension of the well-known logic \CTL with past operators. Conversely, eliminating past operators yields a significantly more intricate landscape. We present a specific fragment of the standard $\mu$-calculus that we conjecture to be expressively equivalent to \FO, and discuss the main challenges in establishing a formal proof for this claim. This underscores the complex nature of \FO over infinite trees and highlights how—unlike in word logics—past operators are crucial for expressiveness in tree logics.

ABSTRACT. We present Strategy Logic as a formalism for reasoning about strategies in multi-agent systems, and survey its main extensions, including imperfect information, epistemic reasoning, quantitative and probabilistic aspects, counting strategies, and hyperproperties.

ABSTRACT. We examine one particular dimension of AI governance: how to monitor and audit AI-enabled products and services throughout the AI development lifecycle, from pre-deployment testing to post-deployment auditing. Combining principles from formal methods with SoTA machine learning, we propose techniques that enable AI-enabled product and service developers and evaluators to perform offline auditing and online (runtime) monitoring of behavioral constraints such as safety constraints, norms, rules and regulations with respect to black-box advanced AI systems, notably LLMs.