ABSTRACT. We introduce a novel semantic framework for Linear Temporal Logic over finite traces ($\mathrm{LTL}_f$) that interprets formulas via $\mathit{sl}$-truth on FM-domains, capturing a finitistic truth-in-the-limit notion over increasingly large temporal models. We complement this semantic foundation with a sound and complete proof-theoretic calculus, enabling formal derivations under the new semantics. Using these tools, we formalize several Yablo-type sentences in temporal logic and examine their behavior. Our analysis shows that all principal Yablo variants (including "always", "sometimes", "almost-always", and "unboundedly-often" sentences) are satisfiable in $\mathrm{LTL}_f$ models, so that no genuine paradox arises in the finite-trace setting. Moreover, in the limit semantics one finds that key Yablo formulas become stably true: for example, the unboundedly-often Yablo sentence holds in all sufficiently long finite traces (i.e., it belongs to the $\mathit{sl}$-theory of the class of all finite traces). These results imply that deep nesting of beliefs in temporal interactions is well-founded, avoiding paradoxical loops when agents operate in bounded time domains.

ABSTRACT. Rational synthesis and rational verification study temporal properties of multi-agent systems with strategic agents. Existing procedures focus on existence. They return equilibrium outcomes, but these outcomes can be unnecessarily long and hard to inspect. We introduce Minimal Rational Synthesis (MRS), a procedure for extracting shortest ultimately periodic equilibrium witnesses from the finite automata–game products used in rational synthesis and rational verification. MRS does not change the underlying equilibrium notions. Instead, it optimises witness extraction after the standard rational verification construction has fixed the relevant winner sets, payoff vectors, and punishment conditions. Our method combines exact shortest-lasso search with automata and product reductions, and may output auxiliary certificates containing on-path actions and punishment information. We implement the approach in EVE for the LTL–LTL, GR(1)– LTL, and GR(1)–GR(1) settings, and report initial experiments showing shorter witnesses and fewer brute-force timeouts on the considered benchmarks.

ABSTRACT. We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.

ABSTRACT. We study synthesis for obligation properties expressed in LTLf+, the extension of LTLf to infinite traces. Obligation properties are positive Boolean combinations of safety and guarantee (co-safety) properties and form the second level of the temporal hierarchy of Manna and Pnueli. Although obligation properties are expressed over infinite traces, they retain most of the simplicity of LTLf. In particular, we show that they admit a translation into symbolically represented deterministic weak automata (DWA) obtained directly from the symbolic deterministic finite automata (DFA) for the underlying LTLf properties on trace prefixes. We show that synthesis for LTLf+ obligation properties is theoretically highly efficient -- solvable in linear time once the DWA is constructed. We investigate several symbolic algorithms for solving DWA games that arise in the synthesis of obligation properties and evaluate their effectiveness experimentally. Overall, the results indicate that synthesis for LTLf+ obligation properties can be performed with virtually the same effectiveness as LTLf synthesis.

ABSTRACT. The logic of inferable, L-DINF, models cooperative agents that reason through explicit beliefs, background knowledge, mental actions, physical actions, roles, resources, costs, preferences, and equivalence classes of actions. We add a probabilistic package to the modular semantics of L-DINF, assigning probability measures to epistemic alternatives and success probabilities to physical actions, while preserving the original separation between the core epistemic model and optional packages. We define probabilistic explicit belief, probabilistic executability, and a deterministic instantiation of the L-DINF action selector based on a probability-aware desirability score. We show how an agent can select a lower-preference but more reliable action when reliability outweighs preference. The proposal is conservative, explainable, and directly extensible towards dynamic probability update.

ABSTRACT. We consider the Strategy Repair problem for an autonomous agent acting in a stochastic dynamic environment. The problem concerns finding the minimum number of modifications that refine a strategy for a probabilistic reachability game into an optimal one, i.e. maximising the probability of winning. After introducing and motivating the problem, we first present a polynomial-time solution for one-player games, i.e. Markov decision processes. The approach exploits a game-to-game reduction, followed by solving a suitable instance of the minimum spanning tree problem. We then extend the problem to the discounted case, where the agent is required to win the game in the fewest possible moves.

ABSTRACT. Multi-agent decision making under uncertainty can be modelled using decentralised partially observable Markov decision processes (DecPOMDPs). However, DecPOMDPs are notoriously difficult to solve due to their exponential dependence on the number of agents. Lifting is a technique that treats groups of indistinguishable instances through representatives if possible, yielding tractable inference in the number of instances in a model. This paper discusses the assumptions necessary for indistinguishability among agents, providing a definition of so-called isomorphic DecPOMDPs that have a model complexity no longer dependent on the number of agents, as well as a lifted solution approach that exploits this lifted agent set for space and runtime gains.

ABSTRACT. In this paper, we prove that \PATLH is exponentially more succinct than \PATLC. In prior work it was shown that \PATLC strictly subsumes \PATLH in expressive power, yet it was conjectured that any \PATLC-specifiable property could be encoded with exponentially shorter formulas than in \PATLH. Establishing this remained elusive, since existing succinctness proofs (e.g., for non-probabilistic \ATLH vs \ATLK) do not readily transfer to the Shannon-entropy setting. Here we resolve the conjecture by explicitly constructing a family of \PATLH formulas $\varphi_n$ of size $O(n)$ and proving that any equivalent \PATLC formula requires size $2^{\Omega(n)}$. Our argument uses the one-person formula-size-game framework. This formally confirms a conjecture from the previous \PATLH/\PATLC study, demonstrating a genuine exponential succinctness gap and advancing recent developments in logical succinctness for strategic-epistemic logics.

ABSTRACT. Multi-agent systems are commonly designed to reduce disagreement through voting, consensus protocols, debate, or fault-tolerant aggregation. We argue that this objective is insufficient for value-laden tasks, where disagreement may reflect genuine normative uncertainty rather than agent error. Building on prior work on reasoning-trace disagreement in human-AI collaborative moderation, we propose a knowledge-representation layer in which reasoning traces and agent decisions are abstracted into symbolic disagreement states. Given agents producing explicit reasoning traces and binary decisions, we distinguish four states according to reasoning similarity and conclusion agreement: convergent agreement, divergent agreement, convergent disagreement and divergent disagreement. These states support defeasible strategic routing rules. We instantiate the framework in content moderation and argue that disagreement-aware routing provides a bridge between sub-symbolic LLM deliberation and symbolic knowledge representation for multi-agent strategic reasoning.

ABSTRACT. We extend concurrent game structures with a simple notion of preference over computations and define a minimal notion of rationality for agents based on the concept of dominance. We use this notion to interpret a CL and an ATL languages that extend the basic CL and ATL languages with modalities for rational capability, namely, a coalition's capability to rationally enforce a given property.

ABSTRACT. Recent work in the field of multi-agent systems has sought to apply techniques and concepts from formal methods to provide rigorous theoretical analysis and guarantees for complex systems in which multiple agents strategically interact, thereby creating the field of equilibrium analysis, also called rational verification. The main goal of equilibrium analysis is to study the complexity-theoretic properties of equilibria and solution concepts for multiplayer games in game theory, as a way to reason about the overall system in a precise, mathematical manner. Multi-agent systems, however, are complicated mathematical objects that consist of multiple different components. Therefore, even specifying deterministic multi-agent systems, the focus of this paper, is a non-trivial matter. In this paper, we argue that issues of representation create a recurring issue in the literature that we call the model gap. This model gap issue often causes issues for researchers wishing to provide complexity-theoretic lower bounds. We further argue that the model gap issue can be resolved by representing multi-agent systems implicitly, using circuits to compute functions.

ABSTRACT. Alternating-time temporal logic (ATL or more generally, ATL*) is a logic for reasoning about computational models of multi-agent decision-making. It mainly deals with strategic capabilities of agent coalitions in multi-player games. Whilst ATL* is useful for the specification and verification of multi-agent systems, it needs further extensions for modeling human players because they usually have to make decisions with uncertain and vague information. As probability calculus is the standard approach to model uncertain information, there have been some probabilistic extensions of ATL. However, in real-world situations, forms of incomplete information are diverse. Hence, in this paper, we propose another two extensions of ATL* to accommodate incomplete information. On one hand, the possibilistic ATL* can represent and reason about uncertainty arising from imprecise predictions of outcomes caused by agents' actions in terms of possibility theory. On the other hand, the many-valued ATL* facilitates the representation and reasoning of fuzzy events. In both extensions, we introduce the syntax and formal semantics of the proposed logics.

ABSTRACT. We use Alternating-time Temporal Logic to study strategies in classical reachability turn-based sabotage games. We extend the usual scope of sabotage games with a liveness version of the game and with concurrent sabotage games. We relate our temporal approach to the graph-theoretical notion of minimal $s{-}t$ cut, and propose its dynamic counterpart. Finally, we indicate how epistemic extensions of ATL and ATL$^{\ast}$ can be useful in studying imperfect-information sabotage games.

ABSTRACT. We study multi-modal logics applied to multi-agent systems modelled by concurrent game models (CGMs) where the commonly assumed principle of independence of agents' actions need not hold. In reality, this principle is often violated by various physical, normative, or other natural constraints on the possible, or admissible, combinations of actions that may be executed by the agents. This motivates the study of variants of CGMs with constraints on the admissible action profiles. We consider three natural approaches for implementing such constraints. The first two allow the agents to choose actions simultaneously, where non-admissible action profiles respectively block or deadlock the system. The third approach requires agents to choose actions sequentially in some priority order, and only presents each agent with choices of actions that do not conflict with previously made choices by other agents, thus making it impossible to select a non-admissible action profile. These approaches are modelled by variants of CGMs. To formalize reasoning in each of them, we introduce suitable conservative extensions of Alternating-time Temporal Logic (ATL, ATL*). For most of these logics, we have shown that they have the same complexity of model checking and satisfiability decision as their ATL/ATL* bases, and proposed complete axiomatic systems.

ABSTRACT. In standard concurrent game models, the set of available actions for agents at each state is fixed. In real-world scenarios, however, this assumption rarely holds. The actions available to an agent at a given state often depend on various constraints, which can be external (objective) or internal (subjective). For instance, one agent’s choice of an action may affect another agent’s available actions; selecting a goal may change an agent’s action set; adopting a particular strategy may alter the set of feasible actions. Strategic reasoning in such settings thus frequently involves changes of agents’ available actions. In this work, we introduce a logic for local strategic reasoning with dynamic action contexts, designed to capture reasoning that involve such changes. Related frameworks include logics using strategy contexts, logics for strategic reasoning in social scenarios, logics for conditional strategic reasoning, and strategy logics. Our logic introduces four dynamic operators: adding action constraints, action choice, constraint relaxation, and full action-resetting. Formulas of the logic are evaluated over a tuple (M, s, AC), where M is a standard concurrent game model, s is a state, and AC is an action context specifying the available actions for each agent at every state. The four dynamic operators are interpreted as local updates of the action context. The logic is expressive and versatile: various other operators, well-known or new, can be defined in the language.

ABSTRACT. The paper presents the logic of local nested conditional abilities, allowing for formal reasoning about what coalitions can achieve, conditional on others acting conditionally on yet others, etc. A two-sorted formal language NConStR is introduced, interpreted over concurrent game models, in which such nested conditional abilities of coalitions can be expressed. It is demonstrated that NConStR can be embedded into Local Basic Strategy Logic (LBSL) via a recursive translation, establishing that LBSL is at least as expressive as NConStR. This embedding allows for the transfer of known metalogical results from LBSL — such as decidability and axiomatizability — to NConStR.

ABSTRACT. Humans can often achieve their goals by delegating sub-goals/tasks to other agents. They may do this without knowing the details of other agents' strategies or getting agreement on a joint strategy. Instead, they use their knowledge about other agents' abilities and make assumptions about others' cooperativeness to synthesize their own individual strategy which uses delegation and handles possible interference between it and that of others. In this paper, we examine how we can formalize such subjective/first-person reasoning about ability under imperfect information as a kind of subjective strategic reasoning under cooperativeness assumptions in a multi-agent epistemic situation calculus with strategic operators.

ABSTRACT. The same arguments often need to be evaluated under different external regimes. An agent with influence over the regime has a strategic lever that standard formalisms do not directly capture. We introduce context-dependent argumentation frameworks (CDAFs), an extension of Dung's theory in which a defeat function determines, per context, which attacks succeed. A perspective-labeled specialisation derives the defeat function from a relevance set $\rho$ and a priority $\pi$. The relevance set is the agent's action space. In a small worked example, the agent's target argument is rejected under every full-relevance injective priority, yet accepted under a partial activation that no VAF audience can mirror. We define the corresponding decision problem, ACTIVATION-MANIPULATION, and record baseline complexity bounds. Tight bounds and multi-agent variants are left open.