Belief-Desire-Intention (BDI) is a framework for modelling agents based on their beliefs, desires, and intentions. Plans are a central component of BDI agents, and define sequences of actions that an agent must undertake to achieve a certain goal. Existing approaches to plan generation often require significant manual effort, and are mainly focused on single-agent systems. As a result, in this work, we have developed a tool that automatically generates BDI plans using Alternating-Time Temporal Logic (ATL). By using ATL, the plans generated accommodate for possible competition or cooperation between the agents in the system. We demonstrate the effectiveness of the tool by generating plans for an illustrative game that requires agent collaboration to achieve a shared goal. We show that the generated plans allow the agents to successfully attain this goal.
Classic reachability games on graphs are zero-sum games, where the goal of one player, Eve, is to visit a vertex from a given target set, and that of other player, Adam, is to prevent this. Generalised reachability games, studied by Fijalkow and Horn, are a generalisation of reachability objectives, where instead of a single target set, there is a family of target sets and Eve must visit all of them in any order. In this work, we further study the complexity of solving two-player games on graphs with generalised reachability objectives. Our results are twofold: first, we provide an improved complexity picture for generalised reachability games, expanding the known tractable class from games in which all target sets are singleton to additionally allowing a logarithmic number of target sets of arbitrary size. Second, we study optimisation variants of generalised reachability with a focus on the size of the target sets. For these problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability in the classic variant for singleton target sets, the optimisation problem is NP-hard when Eve tries to maximise the number of singleton target sets that are visited. Tractability can be recovered in the optimisation setting when all target sets are singleton by requiring that Eve pledges a maximum sized subset of target sets that she can guarantee to visit.
Chains of co-Buchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary w-regular languages. They can be minimized in polynomial time and are hence an attractive language representation for applications in which normally, deterministic wautomata are used. While it is known how to build COCOA from deterministic parity automata, little is currently known about their relationship to automaton models introduced earlier than COCOA. In this paper, we analyze the conciseness of chains of co-Buchi automata. We show that even in the case that all automata in the chain are deterministic, chains of co-Buchi automata can be exponentially more concise than deterministic parity automata. We then answer the question if this conciseness is retained when performing Boolean operations (such as disjunction and conjunction) over COCOA by showing that there exist families of languages for which these operations lead to an exponential growth of the sizes of the automata. The families have the property that when representing them using deterministic parity automata, taking the disjunction or conjunction of them only requires a polynomial blow-up, which shows that Boolean operations over COCOA do not retain their conciseness in general.
This paper proposes appropriate sound and complete proof systems for algebraic structure over metric spaces by combining the development of Quantitative Equational Theories (QET) with the Enriched Lawvere Theories. We extend QETs to Metric Equational Theories (METs) where operations no longer have finite sets as arities (as in QETs and in the general theory of universal algebras), but arities are now drawn from countable metric spaces. This extension is inspired by the theory of Enriched Lawvere Theories which suggests that the arities of operations should be the 2,-presentable objects of the underlying 2,-accessible category. In this setting, the validity of terms in METs can no longer be guaranteed independently of the validity of equations, as it is the case with QET. We solve this problem, and adapt the sound and complete proof system for QETs to these more general METs, taking advantage of the specific structure of metric spaces.
In this paper, we study First Order Logic (FO) over (unordered) infinite trees and its connection with branching-time temporal logics. More specifically, we provide an automata-theoretic characterisation of FO interpreted over infinite trees. To this end, two different classes of hesitant tree automata are introduced and proved to capture precisely the expressive power of two branching time temporal logics, denoted cCTL(+/-)(p) and cCTL(f)(star), which are, respectively, a restricted version of counting CTL with past and counting CTL star over finite paths, both of which have been previously shown equivalent to FO over infinite trees. The two automata characterisations naturally lead to normal forms for the two temporal logics, and highlight the fact that FO can only express properties of the tree branches which are either safety or co-safety in nature.
