We introduce DFAMiner, an efficient tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. The significant improvement of DFAMiner over existing tools is the use of an intermediate representation called three-valued automaton for the given set of labelled samples. This three-valued automaton has accepting and rejecting states as well as don’t-care states, so that it can exactly recognise the labelled samples. The minimal separating DFA for the labelled samples is then learned by minimising the constructed three-valued automata via a reduction to SAT solving. Separating automata are an interesting class of automata that occurs generally in regular model checking and has raised interest in foundational questions of parity game solving. Therefore, DFAMiner has the potential to further advance these fields.

We provide simple proofs of the NC results for the universality, language inclusion, and equivalence problems of unambiguous finite automata, based on recent advances in model checking.We extend all complexity results to separating parity automata and to a restricted class of separating generalised B\"uchi automata, and introduce natural distance metrics for regular and $\omega$-regular languages that can be computed in NC for these classes of automata.As a side result, we show that we can also check universality of run-unambiguous automata---automata that have at most one run for every infinite word---in NC. Lastly, we also show that the minimisation problem is NP-complete for separating automata and NP-hard for unambiguous automata and run-unambiguous automata.

We study two-player zero-sum turn-based games played on graphs with multiple reachability objectives called generalised reachability games. In classic reachability games the goal of one player, Eve, is to visit a given target set of vertices, and that of the other player, Adam, is to prevent this. In generalised reachability games, the single target set is replaced with a family of target sets and the objective of Eve is to visit all of them in any order. We study the complexity of deciding the winner in two-player games with generalised reachability objectives. Our study reveals that an important parameter that determines the complexity of this problem is the size of the target sets. We first prove that deciding the winner in such games is PSPACE-complete, and the PSPACE lower bound holds even when the size of each target set is at most three. By contrast, we show that the problem is FPT in the number of target sets of size greater than one. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the sizes of winning strategies. We also study optimisation variants of these games. For the optimisation problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability of generalised reachability in the case with singleton target sets, the optimisation problem is coNP-hard when Eve tries to maximise the number of target sets that are visited. Tractability of this case can be recovered in a different optimisation setting where Eve is required to pledge a maximum sized subset of target sets that she can guarantee to visit.

We investigate memory requirements for Nash and subgame-perfect equilibria in turn-based deterministic games with ω-regular objectives. We prove that memoryless randomised (i.e., stationary) subgame-perfect equilibria always exist in games with reachability, safety, and 0-2 Muller objectives (i.e., Muller objectives for which accepting sets are either up- or downward closed), and any combination of these objectives. We provide an algorithm to construct such an equilibrium. We also show that randomisation may be required to construct memoryless equilibria in games with reachability or Büchi as well as safety or CoBüchi objectives, and that memoryless equilibria need not exist for any other class of Muller objectives (with respect to the Mostowski hierarchy).

In several socioeconomic-critical decision-making settings, such as fair resource allocation, climate policy, or AI alignment, multiple principals interact within a common arena. While it is well established that these principals may have differing preferences, decision-making under heterogeneous time preferences remains relatively unexplored. In particular, principals may weigh future outcomes differently and may derive distinct utilities from the same decisions. Motivated by such scenarios, we introduce the notion of heterogeneous time preferences in MDPs, where multiple principals possess distinct reward functions and apply different discount factors to future rewards. To compute meaningful decisions in such settings, an AI agent must rely on a notion of optimality that accounts for the preferences of all principals. We adopt a utilitarian notion of social welfare, defined as the sum of utilities accrued to all principals, and study the synthesis of agent strategies that maximise this welfare. Under heterogeneous time preferences, we show that optimal strategies are no longer positional, even when all principals receive identical rewards. Nevertheless, optimal strategies remain structurally simple: they can be realised as pure finite-memory counting strategies, require only polynomial memory in the system size, and can be synthesised in polynomial time. On the other hand, we show that deciding threshold questions for optimal positional strategies is NP-hard, exposing a poor trade-off: insisting on positional simplicity neither makes synthesis tractable nor preserves social welfare.

Strategy synthesis typically follows an all-or-nothing paradigm, returning unrealisable whenever a specification cannot be guaranteed in an uncertain environment. In this paper, we introduce optimal LTLf synthesis, where the goal is to realise as many objectives as possible from a given specification consisting of multiple objectives, especially for the case that they are not all jointly realisable. We first consider max-guarantee synthesis, which commits to a maximal set of objectives that we can a priori guarantee to realise. We then introduce max-observation synthesis, which maximises a posteriori realised objectives that may be incomparable on different executions. Finally, we present incremental max-observation synthesis, which further improves strategies by exploiting opportunities for stronger guarantees when they arise during an execution. Experimental results show that different variations of optimal synthesis scale broadly equally well, solving a large fraction of the benchmark instances within the given timeout, demonstrating the practical feasibility of the approach.

We study stochastic planning problems in Markov Decision Processes (MDPs) with goals specified in Linear Temporal Logic (LTL). The state-of-the-art approach transforms LTL formulas into good-for-MDP (GFM) automata, which feature a restricted form of nondeterminism. These automata are then composed with the MDP, allowing the agent to resolve the nondeterminism during policy synthesis. A major factor affecting the scalability of this approach is the size of the generated automata. In this paper, we propose a novel GFM state-space reduction technique that significantly reduces the number of automata states. Our method employs a sophisticated chain of transformations, leveraging recent advances in good-for-games minimisation developed for adversarial settings. In addition to our theoretical contributions, we present empirical results demonstrating the practical effectiveness of our state-reduction technique. Furthermore, we introduce a direct construction method for formulas of the form GFφ, where φ is a co-safety formula. This construction is provably single-exponential in the worst case, in contrast to the general doubly-exponential complexity. Our experiments confirm the scalability advantages of this specialised construction.

. While discounted payoff games and classic games that reduce to them, like parity and mean-payoff games, are symmetric, their solutions are not. We have taken a fresh view on the properties that optimal solutions need to have, and devised a novel way to converge to them, which is entirely symmetric. We achieve this by building a constraint system that uses every edge to define an inequation, and update the objective function by taking a single outgoing edge for each vertex into account. These edges loosely represent strategies of both players, where the objective function intuitively asks to make the inequation to these edges sharp. In fact, where they are not sharp, there is an 'error' represented by the difference between the two sides of the inequation, which is 0 where the inequation is sharp. Hence, the objective is to minimise the sum of these errors. For co-optimal strategies, and only for them, it can be achieved that all selected inequations are sharp or, equivalently, that the sum of these errors is zero. While no co-optimal strategies have been found, we step-wise improve the error by improving the solution for a given objective function or by improving the objective function for a given solution. This also challenges the gospel that methods for solving payoff games are either based on strategy improvement or on value iteration.

We study the complexity of solving two-player infinite duration games played on a fixed finite graph, where the control of a node is not predetermined but rather assigned randomly. In classic random-turn games, control of each node is assigned randomly every time the node is visited during a play. In this work, we study two natural variants of this where control of each node is assigned only once: (i) control is assigned randomly during a play when a node is visited for the first time and does not change for the rest of the play and (ii) control is assigned a priori before the game starts for every node by independent coin tosses and then the game is played. We investigate the complexity of computing the winning probability with three kinds of objectives–reachability, parity, and energy. We show that the qualitative questions on all variants and all objectives are NL -complete. For the quantitative questions, we show that deciding whether the maximiser can win with probability at least a given threshold for every objective is PSPACE -complete under the first mechanism, and that computing the exact winning probability for every objective is #P -complete under the second. To complement our hardness results for the second mechanism, we propose randomised approximation schemes that efficiently estimate the winning probability for all three objectives, assuming a bounded number of parity colours and unary-encoded weights for energy objectives, and we empirically demonstrate their fast convergence.

Stochastic games provide a powerful framework for controller synthesis in multi-agent systems where cooperation between agents cannot be assumed. They also serve as a core model for modular and decentralized control, where interactions between components can be captured using assume-guarantee contracts. In this setting, synthesis for an individual module reduces to computing a policy robust to the behavior of the environment, modeled as a stochastic two-player game. Many control objectives reduce to reachability objectives, leading to the study of simple stochastic games, a well-known class whose exact computational complexity remains unresolved.A classic result of Condon reformulates the value and policy computation in such games as a quadratic program—a linear program with a quadratic objective. Motivated by their "almost linear" structure, we ask whether efficient linear programming solvers can be leveraged by iterating over a sequence of linear objectives. We introduce the Objective Improvement Algorithm, which iteratively solves linear programs to compute the optimal value and policy. Unlike strategy improvement, our method treats both players symmetrically, and unlike value iteration, it terminates with the optimal value in finitely many steps. We prove convergence and correctness and present experimental results demonstrating practical effectiveness.

We have developed a framework for secure joint querying over federated graph databases using secure multiparty computation (SMPC) protocols in two stages. We start with utilizing the Neo4j graph database on top of the existing Conclave system for secure multi-party relational queries. This provides an effective solution – and thus a conceptional proof-of-concept – without the need of investing heavily into the development. However, as a consequence, it lacks efficiency, as this encounters a significant computational overhead that renders it impractical for real-world usage. Having established the effectiveness of our approach, we turn to a two-stage improvement to the original implementation. The first stage optimizes the performance of the query execution by eliminating the need for sorting after obtaining the final result. The second stage reduces waiting times in the inter-process communication by parallelizing the execution of subqueries for each party. Through a series of experiments, we demonstrate the performance enhancements achieved when executing the subqueries in two different ways: sequentially and in parallel. Furthermore, the results show that, even with a large dataset, our framework achieves execution times of fractions of a second, reducing the running time by two orders of magnitude. Our results also indicate that the execution times and overheads of our system are comparable to those of insecure federated queries with Fabric Neo4j. Overall, our framework addresses the challenges of secure joint querying over federated graph databases and provides substantial performance enhancements over our initial ad-hoc implementation, making it a practical solution for real-world usage.

Computational modelling of materials using machine learning (ML) and historical data has become integral to materials research across physical sciences. The accuracy of predictions for material properties using computational modelling is strongly affected by the choice of the numerical representation that describes a material's composition, crystal structure and constituent chemical elements. Structure, both extended and local, has a controlling effect on properties, but often only the composition of a candidate material is available. However, existing elemental and compositional descriptors lack direct access to structural insights such as the coordination geometry of an element. In this study, we introduce Local Environment-induced Atomic Features (LEAFs), which incorporate information about the statistically preferred local coordination geometry at an element in a crystal structure into descriptors for chemical elements, enabling the modelling of materials solely as compositions without requiring knowledge of their crystal structure. In the crystal structure of a material, each atomic site can be quantitatively described by similarity to common local structural motifs; by aggregating these unique features of similarity from the experimentally verified crystal structures of inorganic materials, LEAFs formulate a set of descriptors for chemical elements and compositions. The direct connection of LEAFs to the local coordination geometry enables the analysis of ML model property predictions, linking compositions to the underlying structure-property relationships. We demonstrate the versatility of LEAFs in structure-informed property predictions for compositions, mapping of chemical space in structural terms, and prioritisation of elemental substitutions. Based on the latter for predicting crystal structures of binary ionic compounds, LEAFs achieve the state-of-the-art accuracy of 86%. These results suggest that the structurally informed description of chemical elements and compositions developed in this work can effectively guide synthetic efforts in discovering new materials.

The temporal logics LTLf+ and PPLTL+ have recently been proposed to express objectives over infinite traces. These logics are appealing because they match the expressive power of LTL on infinite traces while enabling efficient DFA-based techniques, which have been crucial to the scalability of reactive synthesis and adversarial planning in LTLf and PPLTL over finite traces. In this paper, we demonstrate that these logics are also highly effective in the context of MDPs. Introducing a technique tailored for probabilistic systems, we leverage the benefits of efficient DFA-based methods and compositionality. This approach is simpler than its non-probabilistic counterparts in reactive synthesis and adversarial planning, as it accommodates a controlled form of nondeterminism (``good for MDPs") in the automata when transitioning from finite to infinite traces. Notably, by exploiting compositionality, our solution is both implementation-friendly and well-suited for straightforward symbolic implementations.

Families of deterministic finite automata (FDFA) represent regular omega-languages through their ultimately periodic words (UP-words). An FDFA accepts pairs of words, where the first component corresponds to a prefix of the UP-word, and the second component represents a period of that UP-word. An FDFA is termed saturated if, for each UP-word, either all or none of the pairs representing that UP-word are accepted. We demonstrate that determining whether a given FDFA is saturated can be accomplished in polynomial time, thus improving the known PSPACE upper bound by an exponential. We illustrate the application of this result by presenting the first polynomial learning algorithms for representations of the class of all regular omega-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular omega-languages when they are not saturated, we also address the regularity problem and show that it is PSPACE-complete. Finally, we explore a variant of FDFAs called families of deterministic weak automata (FDWA), where the semantics for the periodic part of the UP-word considers omega-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular omega-languages, and we compare the succinctness of these different models.

The vast size of composition space poses a significant challenge for materials chemistry: exhaustive enumeration of potentially interesting compositions is typically infeasible, hindering assessment of important criteria ranging from novelty and stability to cost and performance. We report a tool, Comgen, for the efficient exploration of composition space, which makes use of logical methods from computer science used for proving theorems. We demonstrate how these techniques, which have not previously been applied to materials discovery, can enable reasoning about scientific domain knowledge provided by human experts. Comgen accepts a variety of user-specified criteria, converts these into an abstract form, and utilises a powerful automated reasoning algorithm to identify compositions that satisfy these user requirements, or prove that the requirements cannot be simultaneously satisfied. In contrast to machine learning techniques, explicitly reasoning about domain knowledge, rather than making inferences from data, ensures that Comgen's outputs are fully interpretable and provably correct. Users interact with Comgen through a high-level Python interface. We illustrate use of the tool with several case studies focused on the search for new ionic conductors. Further, we demonstrate the integration of Comgen into an end-to-end automated workflow to propose and evaluate candidate compositions quantitatively, prior to experimental investigation. This highlights the potential of automated formal reasoning in materials chemistry.

We present an efficient Angluin-style learning algorithm for weak deterministic Büchi automata (wDBAs). Different to ordinary deterministic Büchi and co-Büchi automata, wDBAs have a minimal normal form, and we show that we can learn this minimal normal form efficiently. We provide an improved result on the number of queries required and show on benchmarks that this theoretical advantage translates into significantly fewer queries: while previous approaches require a quintic number of queries, we only require quadratically many queries in the size of the canonic wDBA that recognises the target language.