Corina Cirstea

Automata admitting at most one accepting run per structure, known as unambiguous automata, find applications in verification of reactive systems as they extend the class of deterministic automata whilst maintaining some of their desirable properties. In this paper, we generalise a classical construction of unambiguous automata from thin trees to thin coalgebras for analytic functors. This achieves two goals: extending the existing construction to a larger class of structures, and providing conceptual clarity and parametricity to the construction by formalising it in the coalgebraic framework. As part of the construction, we link automaton acceptance of languages of thin coalgebras to language recognition via so-called coherent algebras, which were previously introduced for studying thin coalgebras. This link also allows us to establish an automata-theoretic characterisation of languages recognised by finite coherent algebras.

Traces form a coarse notion of semantic equivalence between states of a process, and have been studied coalgebraically for various types of system. We instantiate the finitary coalgebraic trace semantics framework of Hasuo et al. for controller-versus-environment games, encompassing both nondeterministic and probabilistic environments. Although our choice of monads is guided by the constraints of this abstract framework, they enable us to recover familiar game-theoretic concepts. Concretely, we show that in these games, each element in the trace map corresponds to a collection (a subset or distribution) of plays the controller can force. Furthermore, each element can be seen as the outcome of following a controller strategy. Our results are parametrised by a weak distributive law, which computes what the controller can force in a single step.

We introduce continuation semantics for both fixpoint modal logic (FML) and Computation Tree Logic* (CTL*), parameterised by a choice of branching type and quantitative predicate lifting. Our main contribution is proving that they are equivalent to coalgebraic semantics, for all branching types. Our continuation semantics is defined over coalgebras of the continuation monad whose answer type coincides with the domain of truth values of the formulas. By identifying predicates and continuations, such a coalgebra has a canonical interpretation of the modality by evaluation of continuations. We show that this continuation semantics is equivalent to the coalgebraic semantics for fixpoint modal logic. We then reformulate the current construction for coalgebraic models of CTL*. These models are usually required to have an infinitary trace/maximal execution map, characterized as the greatest fixpoint of a special operator. Instead, we allow coalgebraic models of CTL* to employ non-maximal fixpoints, which we call execution maps. Under this reformulation, we establish a general result on transferring execution maps via monad morphisms. From this result, we obtain that continuation semantics is equivalent to the coalgebraic semantics for CTL*. We also identify a sufficient condition under which CTL can be encoded into fixpoint modal logic under continuation semantics.

Recent research has suggested that category theory can provide useful insights into the field of machine learning (ML). One example is improving the connection between an ML problem and the design of a corresponding ML algorithm. A tool from category theory called a Kan extension is used to derive the design of an unsupervised anomaly detection algorithm for a commonly used benchmark, the Occupancy dataset. Achieving an accuracy of 93.5% and an ROCAUC of 0.98, the performance of this algorithm is compared to state-of-the-art anomaly detection algorithms tested on the Occupancy dataset. These initial results demonstrate that category theory can offer new perspectives with which to attack problems, particularly in making more direct connections between the solutions and the problem’s structure.

This research focuses on establishing trust in multiagent systems where human and AI agents collaborate. We propose a computational notion of actual trust, emphasising the modelling of an agent’s capacity to deliver tasks. Unlike reputation-based trust or performing a statistical analysis on past behaviour, our approach considers the specific setting in which agents interact. We integrate non-deterministic semantics for capturing inherent uncertainties within the behaviour of a multiagent system, but stress the importance of verifying an agent’s actual capabilities. We provide a conceptual analysis of actual trust’s characteristics and highlight relevant trust verification tools. By advancing the understanding and verification of trust in collaborative systems, this research contributes to responsible and trustworthy human-AI interactions, enhancing reliability in various domains.

Ensuring trustworthy performance of autonomous agents and multiagent systems (MAS) requires computational methods and formal tools to support reasoning about different forms of responsibility. In particular, such tools are needed to support identifying agents or agent groups that are responsible, blameworthy, accountable, or sanctionable for outcomes of collective decisions, for fulfilling tasks, or for adhering to norms and social values. As a step toward developing computational frameworks to represent, reason about, and distinguish these forms of responsibility in MAS, for the first time, we present sociotechnical characteristics of these notions of responsibility, identify their requirements, and discuss their applicability for coordinating MAS and ensuring their trustworthiness. This is a step toward establishing a research agenda on how computational techniques for reasoning about and distinguishing different forms of responsibility contribute to the transformation toward ethical and trustworthy autonomous systems.

We consider quantitative notions of parity automaton and parity game aimed at modelling resourceaware behaviour, and study (memory-full) strategies for exhibiting accepting runs that require a minimum amount of initial resources, respectively for winning a game with minimum initial resources. We also show how such strategies can be simplified to consist of only two types of moves: the former aimed at increasing resources, the latter aimed at satisfying the acceptance condition.

We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that suitably adapting the definition of coalgebraic bisimulation yields a general and uniform account of the linear-time behaviour of a state in such