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.

We study asymmetrically discounted stochastic games, in which players use distinct and reasonably apart discount factors. We show that optimal strategies in these games may require both memory and randomisation, in contrast to the classical symmetrically discounted setting. Our main technical contribution establishes that computing incentive Stackelberg equilibria - a variant of Stackelberg equilibria in which one player, called Player Max, can offer payments to the other player, called Player Min - is no harder than solving classical discounted games. We further show that optimal strategies in this setting can be realised by finite counting strategies, whereas restricting players to stationary strategies makes the problem computationally intractable. Finally, we establish that computing classical Stackelberg equilibria in these games under the constraint of memoryless strategies is NP-complete and remains NP-hard even when general or counting strategies are allowed.

We survey word automata with limited nondeterminism, a family of models lying between deterministic and fully nondeterministic automata. While determinism provides a simple algorithmic basis for verification, reactive synthesis, and probabilistic analysis, determinisation incurs large state blow-up, especially for ω-regular specifications. Limited nondeterminism offers a middle ground: it preserves some of the succinctness of nondeterministic automata while retaining enough structure for algorithmic use. We focus on three notions: unambiguous automata, in which each accepted word has at most one accepting run; good-for-games automata, whose nondeterministic choices can be resolved on the fly from the input prefix; and good-for-MDPs automata, which preserve optimal satisfaction probabilities when composed with MDPs. We compare these models in terms of expressiveness, succinctness, decision problems, minimisation, and applications to model checking, synthesis, reinforcement learning, and stochastic planning. Finally, we discuss how these threads converge: recent work has used good-for-games minimisation as a preprocessing step to reduce unambiguous and good-for-MDPs automata before composition, yielding more compact constructions for probabilistic analysis and planning. We present this as a recurring algorithmic pattern - resolving an automaton’s nondeterminism before it is amplified by the product with the system - that unifies otherwise separate lines of work.

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).

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. arXiv admin note: substantial text overlap with arXiv:2310.01008

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.

In machine learning, splitting data into training and test sets is usually achieved using random stratified sampling, in which classes are proportionally divided into two subsets. Other methods also consider feature-aware criteria, and some of those methods claim to have achieved optimal split of minimised variance. We do not advocate aiming to achieve an optimal split or minimise variance since this would be counterproductive for ensemble methods, where the diversity of the training set is desired. Ensemble methods achieve diversity through bagging and boosting schemes. In the recently introduced Monte Carlo ensemble approach, diversity can be maintained through random stratified sampling without using bagging or boosting methods. This work introduces a feature-aware split that retains the diversity of the ensemble. To this end, we propose an evolutionary algorithm that starts with an entirely random population and aims at objectives of proportional class-representation and minimisation of the normalized mean error rather than minimisation of variance. The proposed data-split method is tested on three different models used within a hierarchical Monte Carlo ensemble. The results show that the method positively affects the predictability performance when applied on two domain-specific material science datasets and a collection of 38 general machine learning datasets.

Abstract Good-for-Games (GfG) automata require that their nondeterminism can be resolved on-the-fly, while unambiguous automata guarantee that no word has more than one accepting run. These two mutually exclusive ways of restricted nondeterminism play their roles independently in Markov chain model checking (MCMC) for almost a decade but synthesising them seems hopeless: an automaton that is both GfG and unambiguous is essentially deterministic. This work breaks this perception by combining the strengths of unambiguity with the GfG co-Büchi minimisation recently proposed by Abu Radi and Kupferman. More precisely, this combination allows us to turn unambiguous automata to certain types of probabilistic automata that can be used for MCMC. The resulting automata can be exponentially smaller, and we have provided a family of automata exemplifying this state space reduction, which translates into a significant acceleration of MCMC.

History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting. Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomise and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is λ-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.

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.

Families of deterministic finite automata (FDFA) represent regular ω-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 ω-languages. Furthermore, we establish that deciding a weaker property, referred to as almost saturation, is PSPACE-complete. Since FDFAs do not necessarily define regular ω-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 ω-words instead of finite words. We demonstrate that saturation for FDWAs is also decidable in polynomial time, that FDWAs always define regular ω-languages, and we compare the succinctness of these different models.

The temporal logics LTLf+ and PPLTL+ have recently been introduced 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 nonprobabilistic 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.

Adversarial training has emerged as a highly effective way to improve the robustness of deep neural networks (DNNs). It is typically conceptualized as a min-max optimization problem over model weights and adversarial perturbations, where the weights are optimized using gradient descent methods, such as SGD. In this paper, we propose a novel approach by treating model weights as random variables, which paves the way for enhancing adversarial training through Second-Order Statistics Optimization (S$^{2}$2O) over model weights. We challenge and relax a prevalent, yet often unrealistic, assumption in prior PAC-Bayesian frameworks: the statistical independence of weights. From this relaxation, we derive an improved PAC-Bayesian robust generalization bound. Our theoretical developments suggest that optimizing the second-order statistics of weights can substantially tighten this bound. We complement this theoretical insight by conducting an extensive set of experiments that demonstrate that S$^{2}$2O not only enhances the robustness and generalization of neural networks when used in isolation, but also seamlessly augments other state-of-the-art adversarial training techniques.

Regular decision processes (RDPs) are a subclass of non-Markovian decision processes where the transition and reward functions are guarded by some regular property of the past (a lookback). While RDPs enable intuitive and succinct representation of non-Markovian decision processes, their expressive power coincides with finite-state Markov decision processes (MDPs). We introduce omega-regular decision processes (ODPs) where the non-Markovian aspect of the transition and reward functions are extended to an omega-regular lookahead over the system evolution. Semantically, these lookaheads can be considered as promises made by the decision maker or the learning agent about her future behavior. In particular, we assume that, if the promised lookaheads are not met, then the payoff to the decision maker is falsum (least desirable payoff), overriding any rewards collected by the decision maker. We enable optimization and learning for ODPs under the discounted-reward objective by reducing them to lexicographic optimization and learning over finite MDPs. We present experimental results demonstrating the effectiveness of the proposed reduction.

Alternating-time temporal logic (ATL) extends branching time logic by enabling quantification over paths that result from the strategic choices made by multiple agents in various coalitions within the system. While classical temporal logics express properties of “closed” systems, ATL can express properties of “open” systems resulting from interactions among several agents. Reinforcement learning (RL) is a sampling-based approach to decision-making where learning agents, guided by a scalar reward function, discover optimal policies through repeated interactions with the environment. The challenge of translating high-level objectives into scalar rewards for RL has garnered increased interest, particularly following the success of model-free RL algorithms. This paper presents an approach for deploying model-free RL to verify multi-agent systems against ATL specifications. The key contribution of this paper is a verification procedure for model-free RL of quantitative and non-nested classic ATL properties, based on Q-learning, demonstrated on a natural subclass of non-nested ATL formulas.

Abstract We propose , a passive learning tool for learning minimal separating deterministic finite automata (DFA) from a set of labelled samples. 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. We first propose a simple and linear-time algorithm that incrementally constructs a three-valued DFA (3DFA) from a set of labelled samples given in the usual lexicographical order. This 3DFA has accepting and rejecting states as well as don’t-care states, so that it can exactly recognise the labelled examples. We then apply our tool to mining a minimal separating DFA for the labelled samples by minimising the constructed automata via a reduction to SAT solving. Empirical evaluation shows that our tool outperforms current state-of-the-art tools significantly on standard benchmarks for learning minimal separating DFAs from samples. Progress in the efficient construction of separating DFAs can also lead to finding the lower bound of parity game solving, where we show that can create optimal separating automata for simple languages with up to 7 colours. Future improvements might offer inroads to better data structures.

Binarized neural networks (BNNs) are a class of deep neural networks (DNNs) known for their minimal computational requirements during inference, making them ideal for low-performance environments. Despite their efficiency, BNNs are as vulnerable to safety and security issues as other types of DNNs, and hence analyzing their robustness is essential. In contrast to general DNNs, BNNs are relatively small and straightforward, making it feasible to assess their robustness analytically. We propose a method for rigorously analyzing BNN robustness based on 0–1 Integer Linear Programming (0–1 ILP), which utilizes the dual functionality of boolean variables within BNNs as both boolean (with values of ‘true’ and ‘false’) and real-valued variables constrained to binary values (0 and 1). By leveraging this duality, we formalize the robustness problem as a linear programming problem augmented with boolean reasoning. We minimize the distance to a differently classified image using either the L1-norm (binarized and non-binarized inputs) or the Lœ-norm (non-binarized inputs). We have implemented our approach using the Z3 solver and evaluated it on the MNIST and FashionMNIST datasets. Our results demonstrate the capability to construct optimal adversarial examples with minimal deviations from the ground truth images. We achieved a one-pixel difference between the original and perturbed images for all binarized images. We also identified minimal perturbations on grayscale images using the L1and Lœ-norms. For the latter, we simplified the analysis to determine the existence of epsilon-close adversarial examples across a range of epsilon values.

We study robust, efficient, and stealthy attacks on object detector types of classifiers. Such adversarial attacks are meant to suppress the correct classification of objects in a real world scenario, in our case the classification of road signs by a self-driving car. In this scenario, we need to design a physical attack, e.g. in the form of adding a sticker that looks natural (like an algae patina or marks left by a bird), so that it does not arouse suspicion, but reliably suppresses the classification during an approach without being affected by minor changes in brightness or distance. We show that such an attack can be achieved against a known network, applying a multi-phase approach to successively learn how to place and mildly adjust bird marks to robustly and effectively fool Yolo while retaining a natural look.

This paper presents the theory of probabilistic hier-archical supervised ensemble learning (TPHSEL), a classification approach we have developed with the goal of obtaining classifications for material selection with a degree of interpretability of the results. We found that TPHSEL is a competitive classifier, not only for our target application, but also for a broader range of standard datasets, where it outperformed support vector machines, random forests, and optimal classification trees. The dataset we developed the method for within the field of materials science is small (405 entries), leading to relatively low accuracy (81 % to 82 %) for both our method and a deep learning approach used earlier. In this context, we found that selection based on a large vote share left close to 20 % of candidate materials, and in this bracket, accuracy and other model performance metrics are above 0.95. This is excellent news for prioritising experimental targets (and related tasks), as it indicates that it is possible to identify promising candidates based on data that still leaves shortfalls in classification.

This paper presents hierarchical supervised Monte Carlo ensemble learning (HSMEL). This provides an extension to the theory of probabilistic hierarchical supervised ensemble learning (TPHSEL), which itself evolved from the theory of prob-abilistic hierarchical supervised learning (TPHSL). The basic idea captured in TPHSL is that a complex model can be replaced with a hierarchy of simple and mathematically understandable models. Such models are amenable to interpretation, and they are therefore more likely to contribute to explainable AI, in comparison to black box models. The basic TPHSL was subsequently advanced to TPHSEL, where several hierarchical models make a classification decision by majority vote. In this paper TPHSEL is further advanced to include the notion of Monte Carlo ensemble. We show that this ensemble is computationally faster and has broader reach on training examples. The method has been deployed in use cases from materials science, specifically to study the impact of various features on the conductivity of materials. Based on the performance of individual features, the method has been devised that applies set theory over ensemble outcomes to predict the average accuracy that could be achieved if those features are grouped in some way. We argue that this method has potential to accelerate material design procedures by providing predictions about machine learning performance parameters without engaging in extensive computational effort and consequently will also reduce chemistry lab experimentation. In addition, to show resilience of HSMEL, we have also applied it on 28 general machine learning datasets, where its performance is compared with the classical methods from the literature.

We present an innovative approach for capturing the complexity of ω-regular languages using the concept of flowers. This semantic tool combines two syntax-based definitions, namely the Mostowski hierarchy of word languages and syntactic flowers. The former is based on deterministic parity automata with a limited number of priorities, while the latter simplifies deterministic parity automata by reducing the number of priorities used, without altering their structure. Synthesising these two approaches yields a semantic concept of flowers, which offers a more effective way of dealing with the complexity of ω-regular languages. This letter provides a comprehensive definition of semantic flowers and shows that it captures the complexity of ω-regular languages. We also show that this natural concept yields simple proofs of the expressive power of good-for-games automata.

We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step. We show that the class of timed $\omega$-languages recognized by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA. For non-deterministic timed automata it is known that universality is already undecidable for safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete. For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automaton states.

We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalize constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak Büchi automata (AVAs)—automata that have only singleton strongly connected components (SCCs); these AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)n vs. (0.76n)n), while the input of our construction can be exponentially more succinct.

We introduce a method for translating an alternating weak Büchi automaton (AWA), which corresponds to a Linear Dynamic Logic (LDL) formula, to an unambiguous Büchi automaton (UBA). Our translations generalise constructions for Linear Temporal Logic (LTL), a less expressive specification language than LDL. In classical constructions, LTL formulas are first translated to alternating very weak automata (AVAs) - automata that have only singleton strongly connected components (SCCs); the AVAs are then handled by efficient disambiguation procedures. However, general AWAs can have larger SCCs, which complicates disambiguation. Currently, the only available disambiguation procedure has to go through an intermediate construction of nondeterministic Büchi automata (NBAs), which would incur an exponential blow-up of its own. We introduce a translation from general AWAs to UBAs with a singly exponential blow-up, which also immediately provides a singly exponential translation from LDL to UBAs. Interestingly, the complexity of our translation is smaller than the best known disambiguation algorithm for NBAs (broadly (0.53n)ⁿ vs. (0.76n)ⁿ), while the input of our construction can be exponentially more succinct.

Nondeterministic good-for-MDPs (GFM) automata are for MDP model checking and reinforcement learning what good-for-games automata are for reactive synthesis: a more compact alternative to deterministic automata that displays nondeterminism, but only so much that it can be resolved locally, such that a syntactic product can be analysed. GFM has recently been introduced as a property for reinforcement learning, where the simpler Büchi acceptance conditions it allows to use is key. However, while there are classic and novel techniques to obtain automata that are GFM, there has not been a decision procedure for checking whether or not an automaton is GFM. We show that GFM-ness is decidable and provide an EXPTIME decision procedure as well as a PSPACE-hardness proof.

Reinforcement learning (RL) is a powerful approach for training agents to perform tasks, but designing an appropriate reward mechanism is critical to its success. However, in many cases, the complexity of the learning objectives goes beyond the capabilities of the Markovian assumption, necessitating a more sophisticated reward mechanism. Reward machines and ω-regular languages are two formalisms used to express non-Markovian rewards for quantitative and qualitative objectives, respectively. This paper introduces ω-regular reward machines, which integrate reward machines with ω-regular languages to enable an expressive and effective reward mechanism for RL. We present a model-free RL algorithm to compute ε-optimal strategies against ω-regular reward machines and evaluate the effectiveness of the proposed algorithm through experiments.

Abstract Mungojerrie is an extensible tool that provides a framework to translate linear-time objectives into reward for reinforcement learning (RL). The tool provides convergent RL algorithms for stochastic games, reference implementations of existing reward translations for $$\omega $$ ω -regular objectives, and an internal probabilistic model checker for $$\omega $$ ω -regular objectives. This functionality is modular and operates on shared data structures, which enables fast development of new translation techniques. Mungojerrie supports finite models specified in PRISM and $$\omega $$ ω -automata specified in the HOA format, with an integrated command line interface to external linear temporal logic translators. Mungojerrie is distributed with a set of benchmarks for $$\omega $$ ω -regular objectives in RL.

The expanding role of reinforcement learning (RL) in safety-critical system design has promoted ω-automata as a way to express learning requirements—often non-Markovian—with greater ease of expression and interpretation than scalar reward signals. However, real-world sequential decision making situations often involve multiple, potentially conflicting, objectives. Two dominant approaches to express relative preferences over multiple objectives are: (1) weighted preference , where the decision maker provides scalar weights for various objectives, and (2) lexicographic preference , where the decision maker provides an order over the objectives such that any amount of satisfaction of a higher-ordered objective is preferable to any amount of a lower-ordered one. In this article, we study and develop RL algorithms to compute optimal strategies in Markov decision processes against multiple ω-regular objectives under weighted and lexicographic preferences. We provide a translation from multiple ω-regular objectives to a scalar reward signal that is both faithful (maximising reward means maximising probability of achieving the objectives under the corresponding preference) and effective (RL quickly converges to optimal strategies). We have implemented the translations in a formal reinforcement learning tool, Mungojerrie , and we present an experimental evaluation of our technique on benchmark learning problems.

The increasing use of Machine Learning (ML) components embedded in autonomous systems—so-called Learning-Enabled Systems (LESs)—has resulted in the pressing need to assure their functional safety. As for traditional functional safety, the emerging consensus within both, industry and academia, is to use assurance cases for this purpose. Typically assurance cases support claims of reliability in support of safety, and can be viewed as a structured way of organising arguments and evidence generated from safety analysis and reliability modelling activities. While such assurance activities are traditionally guided by consensus-based standards developed from vast engineering experience, LESs pose new challenges in safety-critical application due to the characteristics and design of ML models. In this article, we first present an overall assurance framework for LESs with an emphasis on quantitative aspects, e.g., breaking down system-level safety targets to component-level requirements and supporting claims stated in reliability metrics. We then introduce a novel model-agnostic Reliability Assessment Model (RAM) for ML classifiers that utilises the operational profile and robustness verification evidence. We discuss the model assumptions and the inherent challenges of assessing ML reliability uncovered by our RAM and propose solutions to practical use. Probabilistic safety argument templates at the lower ML component-level are also developed based on the RAM. Finally, to evaluate and demonstrate our methods, we not only conduct experiments on synthetic/benchmark datasets but also scope our methods with case studies on simulated Autonomous Underwater Vehicles and physical Unmanned Ground Vehicles.

Adversarial training has been shown to be one of the most effective approaches to improve the robustness of deep neural networks. It is formalized as a min-max optimization over model weights and adversarial perturbations, where the weights can be optimized through gradient descent methods like SGD. In this paper, we show that treating model weights as random variables allows for enhancing adversarial training through Second-Order Statistics Optimization (S2O) with respect to the weights. By relaxing a common (but unrealistic) assumption of previous PAC-Bayesian frameworks that all weights are statistically independent, we derive an improved PAC-Bayesian adversarial generalization bound, which suggests that optimizing second-order statistics of weights can effectively tighten the bound. In addition to this theoretical insight, we conduct an extensive set of experiments, which show that S2O not only improves the robustness and generalization of the trained neural networks when used in isolation, but also integrates easily in state-of-the-art adversarial training techniques like TRADES, AWP, MART, and AVMixup, leading to a measurable improvement of these techniques. The code is available at https://github.com/Alexkael/S2O.

We introduce hidden 1-counter Markov models (H1MMs) as an attractive sweet spot between standard hidden Markov models (HMMs) and probabilistic context-free grammars (PCFGs). Both HMMs and PCFGs have a variety of applications, e.g., speech recognition, anomaly detection, and bioinformatics. PCFGs are more expressive than HMMs, e.g., they are more suited for studying protein folding or natural language processing. However, they suffer from slow parameter fitting, which is cubic in the observation sequence length. The same process for HMMs is just linear using the well-known forward-backward algorithm. We argue that by adding to each state of an HMM an integer counter, e.g., representing the number of clients waiting in a queue, brings its expressivity closer to PCFGs. At the same time, we show that parameter fitting for such a model is computationally inexpensive: it is bi-linear in the length of the observation sequence and the maximal counter value, which grows slower than the observation length. The resulting model of H1MMs allows us to combine the best of both worlds: more expressivity with faster parameter fitting.

Recursion is the fundamental paradigm to finitely describe potentially infinite objects. As state-of-the-art reinforcement learning (RL) algorithms cannot directly reason about recursion, they must rely on the practitioner's ingenuity in designing a suitable "flat" representation of the environment. The resulting manual feature constructions and approximations are cumbersome and error-prone; their lack of transparency hampers scalability. To overcome these challenges, we develop RL algorithms capable of computing optimal policies in environments described as a collection of Markov decision processes (MDPs) that can recursively invoke one another. Each constituent MDP is characterized by several entry and exit points that correspond to input and output values of these invocations. These recursive MDPs (or RMDPs) are expressively equivalent to probabilistic pushdown systems (with call-stack playing the role of the pushdown stack), and can model probabilistic programs with recursive procedural calls. We introduce Recursive Q-learning---a model-free RL algorithm for RMDPs---and prove that it converges for finite, single-exit and deterministic multi-exit RMDPs under mild assumptions.

Zielonka's classic recursive algorithm for solving parity games is perhaps the simplest among the many existing parity game algorithms. However, its complexity is exponential, while currently the state-of-the-art algorithms have quasipolynomial complexity. Here, we present a modification of Zielonka's classic algorithm that brings its complexity down to $n^{O\left(\log\left(1+\frac{d}{\log n}\right)\right)}$, for parity games of size $n$ with $d$ priorities, in line with previous quasipolynomial-time solutions.

Abstract We study reinforcement learning for the optimal control of Branching Markov Decision Processes (BMDPs), a natural extension of (multitype) Branching Markov Chains (BMCs). The state of a (discrete-time) BMCs is a collection of entities of various types that, while spawning other entities, generate a payoff. In comparison with BMCs, where the evolution of a each entity of the same type follows the same probabilistic pattern, BMDPs allow an external controller to pick from a range of options. This permits us to study the best/worst behaviour of the system. We generalise model-free reinforcement learning techniques to compute an optimal control strategy of an unknown BMDP in the limit. We present results of an implementation that demonstrate the practicality of the approach.

Abstract We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative $$\omega $$ ω -regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy levelk, is decidable and in $$\mathsf {NP}\cap \mathsf {coNP}$$ NP∩coNP . The same holds for checking if such akexists and if a givenkis minimal.

The ever increasing number of connected devices has lead to a metoric rise in the amount data to be processed. This has caused computation to be moved to the edge of the cloud increasing the importance of efficiency in the whole of cloud. The use of this fog computing for time-critical control applications is on the rise and requires robust guarantees on transmission times of the packets in the network while reducing total transmission times of the various packets. We consider networks in which the transmission times that may vary due to mobility of devices, congestion and similar artifacts. We assume knowledge of the worst case tranmssion times over each link and evaluate the typical tranmssion times through exploration. We present the use of reinforcement learning to find optimal paths through the network while never violating preset deadlines. We show that with appropriate domain knowledge, using popular reinforcement learning techniques is a promising prospect even in time-critical applications.

This paper discusses the hardness of finding minimal good-for-games (GFG) Buchi, Co-Buchi, and parity automata with state based acceptance. The problem appears to sit between finding small deterministic and finding small nondeterministic automata, where minimality is NP-complete and PSPACE-complete, respectively. However, recent work of Radi and Kupferman has shown that minimising Co-Buchi automata with transition based acceptance is tractable, which suggests that the complexity of minimising GFG automata might be cheaper than minimising deterministic automata. We show for the standard state based acceptance that the minimality of a GFG automaton is NP-complete for Buchi, Co-Buchi, and parity GFG automata. The proofs are a surprisingly straight forward generalisation of the proofs from deterministic Buchi automata: they use a similar reductions, and the same hard class of languages.

This paper studies the novel concept of weight correlation in deep neural networks and discusses its impact on the networks' generalisation ability. For fully-connected layers, the weight correlation is defined as the average cosine similarity between weight vectors of neurons, and for convolutional layers, the weight correlation is defined as the cosine similarity between filter matrices. Theoretically, we show that, weight correlation can, and should, be incorporated into the PAC Bayesian framework for the generalisation of neural networks, and the resulting generalisation bound is monotonic with respect to the weight correlation. We formulate a new complexity measure, which lifts the PAC Bayes measure with weight correlation, and experimentally confirm that it is able to rank the generalisation errors of a set of networks more precisely than existing measures. More importantly, we develop a new regulariser for training, and provide extensive experiments that show that the generalisation error can be greatly reduced with our novel approach.

We characterize the class of nondeterministic $$\omega $$ -automata that can be used for the analysis of finite Markov decision processes (MDPs). We call these automata ‘good-for-MDPs’ (GFM). We show that GFM automata are closed under classic simulation as well as under more powerful simulation relations that leverage properties of optimal control strategies for MDPs. This closure enables us to exploit state-space reduction techniques, such as those based on direct and delayed simulation, that guarantee simulation equivalence. We demonstrate the promise of GFM automata by defining a new class of automata with favorable properties—they are Büchi automata with low branching degree obtained through a simple construction—and show that going beyond limit-deterministic automata may significantly benefit reinforcement learning.

We provide the first solution for model-free reinforcement learning of $$\omega $$ -regular objectives for Markov decision processes (MDPs). We present a constructive reduction from the almost-sure satisfaction of $$\omega $$ -regular objectives to an almost-sure reachability problem, and extend this technique to learning how to control an unknown model so that the chance of satisfying the objective is maximized. We compile $$\omega $$ -regular properties into limit-deterministic Büchi automata instead of the traditional Rabin automata; this choice sidesteps difficulties that have marred previous proposals. Our approach allows us to apply model-free, off-the-shelf reinforcement learning algorithms to compute optimal strategies from the observations of the MDP. We present an experimental evaluation of our technique on benchmark learning problems.

Quantitative extensions of parity games have recently attracted significant interest. These extensions include parity games with energy and payoff conditions as well as finitary parity games and their generalization to parity games with costs. Finitary parity games enjoy a special status among these extensions, as they offer a native combination of the qualitative and quantitative aspects in infinite games: The quantitative aspect of finitary parity games is a quality measure for the qualitative aspect, as it measures the limit superior of the time it takes to answer an odd color by a larger even one. Finitary parity games have been extended to parity games with costs, where each transition is labeled with a nonnegative weight that reflects the costs incurred by taking it. We lift this restriction and consider parity games with costs with arbitrary integer weights. We show that solving such games is in NP $\cap$ coNP, the signature complexity for games of this type. We also show that the protagonist has finite-state winning strategies, and provide tight pseudo-polynomial bounds for the memory he needs to win the game. Naturally, the antagonist may need infinite memory to win. Moreover, we present tight bounds on the quality of winning strategies for the protagonist. Furthermore, we investigate the problem of determining, for a given threshold $b$, whether the protagonist has a strategy of quality at most $b$ and show this problem to be EXPTIME-complete. The protagonist inherits the necessity of exponential memory for implementing such strategies from the special case of finitary parity games.

Prefetching constitutes a valuable tool toward efficient Web surfing. As a result, estimating the amount of resources that need to be preloaded during a surfer's browsing becomes an important task. In this regard, prefetching can be modeled as a two-player combinatorial game [Fomin et al., Theoretical Computer Science 2014], where a surfer and a marker alternately play on a given graph (representing the Web graph). During its turn, the marker chooses a set of $k$ nodes to mark (prefetch), whereas the surfer, represented as a token resting on graph nodes, moves to a neighboring node (Web resource). The surfer's objective is to reach an unmarked node before all nodes become marked and the marker wins. Intuitively, since the surfer is step-by-step traversing a subset of nodes in the Web graph, a satisfactory prefetching procedure would load in cache all resources lying in the neighborhood of this growing subset. Motivated by the above, we consider the following problem to which we refer to as the Maximum Rooted Connected Expansion (MRCE) problem. Given a graph $G$ and a root node $v_0$, we wish to find a subset of vertices $S$ such that $S$ is connected, $S$ contains $v_0$ and the ratio $|N[S]|/|S|$ is maximized, where $N[S]$ denotes the closed neighborhood of $S$, that is, $N[S]$ contains all nodes in $S$ and all nodes with at least one neighbor in $S$. We prove that the problem is NP-hard even when the input graph $G$ is restricted to be a split graph. On the positive side, we demonstrate a polynomial time approximation scheme for split graphs. Furthermore, we present a $\frac{1}{6}(1-\frac{1}{e})$-approximation algorithm for general graphs based on techniques for the Budgeted Connected Domination problem [Khuller et al., SODA 2014]. Finally, we provide a polynomial-time algorithm for the special case of interval graphs.

Energy-parity objectives combine ω-regular with quantitative objectives of reward MDPs. The controller needs to avoid to run out of energy while satisfying a parity objective. We refute the common belief that, if an energy-parity objective holds almost-surely, then this can be realised by some finite memory strategy. We provide a surprisingly simple counterexample that only uses coBuchi conditions. We introduce the new class of bounded (energy) storage objectives that, when combined with parity objectives, preserve the finite memory property. Based on these, we show that almostsure and limit-sure energy-parity objectives, as well as almostsure and limit-sure storage parity objectives, are in NP ∩ coNP and can be solved in pseudo-polynomial time for energy-parity MDPs.

Parity games play an important role in model checking and synthesis. In their paper, Calude et al. have recently shown that these games can be solved in quasi-polynomial time. We show that their algorithm can be implemented efficiently: we use their data structure as a progress measure, allowing for a backward implementation instead of a complete unravelling of the game. To achieve this, a number of changes have to be made to their techniques, where the main one is to add power to the antagonistic player that allows for determining her rational move without changing the outcome of the game. We provide a first implementation for a quasi-polynomial algorithm, test it on small examples, and provide a number of side results, including minor algorithmic improvements, a quasi bi-linear complexity in the number of states and edges for a fixed number of colours, and matching lower bounds for the algorithm of Calude et al.

Several general search techniques such as genetic programming and simulated annealing have recently been investigated for synthesising programs from specifications of desired objective behaviours. In this context, these techniques explore the space of all candidate programs by performing local changes to candidates selected by means of a measure of their fitness w.r.t the desired objectives. Previous performance results advocated the use of simulated annealing over genetic programming for such problems. In this paper, we investigate the application of these techniques for the computation of deterministic strategies solving symbolic Discrete Controller Synthesis (DCS) problems, where a model of the system to control is given along with desired objective behaviours. We experimentally confirm that relative performance results are similar to program synthesis, and give a complexity analysis of our simulated annealing algorithm for symbolic DCS.

This paper studies optimal time-bounded control in a simple subclass of linear hybrid systems, which consists of one continuous variable and global constraints. Each state has a continuous cost attached to it, which is linear in the sojourn time, while a discrete cost is attached to each transition taken. We show the corresponding decision problem to be NP-complete and develop an FPTAS for finding an approximate solution. We have implemented a small prototype to compare the performance of these approximate and precise algorithms for this problem. Our results indicate that the proposed approximation schemes scale. Furthermore, we show that the same problem with infinite time horizon is in LOGSPACE.

Safety-critical systems need to maintain their functionality in the presence of multiple errors caused by component failures or disastrous environment events. We propose a game-theoretic foundation for synthesizing control strategies that maximize the resilience of a software system in defense against a realistic error model. The new control objective of such a game is called $k$ -resilience. In order to be $k$ -resilient, a system needs to rapidly recover from infinitely many waves of a small number of up to $k$ close errors provided that the blocks of up to $k$ errors are separated by short time intervals, which can be used by the system to recover. We first argue why we believe this to be the right level of abstraction for safety critical systems when local faults are few and far between. We then show how the analysis of $k$ -resilience problems can be formulated as a model-checking problem of a mild extension to the alternating-time $\mu$ -calculus (AMC). The witness for $k$ resilience, which can be provided by the model checker, can be used for providing control strategies that are optimal with respect to resilience. We show that the computational complexity of constructing such optimal control strategies is low and demonstrate the feasibility of our approach through an implementation and experimental results.

The bottleneck in the quantitative analysis of Markov chains and Markov decision processes against specifications given in LTL or as some form of nondeterministic Büchi automata is the inclusion of a determinisation step of the automaton under consideration. In this paper, we show that full determinisation can be avoided: subset and breakpoint constructions suffice. We have implemented our approach - both explicit and symbolic versions - in a prototype tool. Our experiments show that our prototype can compete with mature tools like PRISM.

Bounded-rate multi-mode systems are hybrid systems that can switch among a finite set of modes. Its dynamics is specified by a finite number of real-valued variables with mode-dependent rates that can vary within given bounded sets. Given an arbitrary piecewise linear trajectory, we study the problem of following the trajectory with arbitrary precision, using motion primitives given as bounded-rate multi-mode systems. We give an algorithm to solve the problem and show that the problem is co-NP complete. We further prove that the problem can be solved in polynomial time for multi-mode systems with fixed dimension. We study the problem with dwell-time requirement and show the decidability of the problem under certain positivity restriction on the rate vectors. Finally, we show that introducing structure to the multi-mode systems leads to undecidability, even when using only a single clock variable.

Concurrency theory suggests the use of fairness as a criterion for a reasonable execution: a transition or a process should not wait an unbounded amount of time to execute if it is enabled continuously (under weak fairness) or infinitely often (under strong fairness). Unlike multiprocessing, in actual concurrent systems one may rely on the physical nature of the system to act in a “fair” manner. However, in many realistic concurrent systems, performing the next transition may involve several smaller steps that can include negotiation and communication, and fairness can be hard to achieve. It is useful to be able to control the global fairness guaranteed by enforcing local constraints on processes. We define local fairness conditions and study their relationship with common notions of global fairness constraints.

We propose an extension to ATL ( alternating-time temporal logic ), called BSIL ( basic strategy-interaction logic ), for specifying collaboration among agents in a multiagent system. We show that BSIL is strictly more expressive than ATL + but incomparable with ATL * , GL ( game logic ), and AMC ( alternating μ-calculus ) in expressiveness. We show that a memoryful strategy is necessary for fulfilling a specification in BSIL. We establish that the BSIL model-checking problem is PSPACE-complete. However, BSIL model checking can be performed in time quadratic in the model for fixed formulas. The BSIL (and hence ATL + ) satisfiability is 2EXPTIME-complete. Finally, we report our experiment with a model checker for BSIL.

We study optimal equilibrium in turn based multiplayer mean-payoff games. Nash equilibrium are a standard way to define rational behaviour of different players in multi-player games. These equilibrium treat all players equally. We study settings where a leader has additional power over the game: she has the power to assign strategies to all participating players, including herself. We argue that a leader who assign the strategies, may not want to comply with the common restrictions imposed by Nash equilibrium. This setting provides the basis for the quantitative analysis of the distributed systems, where the leader can take the role of a controller or an adversary, while the other players form a rational environment. We show that the leader always has an optimal strategy in this setting, and that no Nash equilibrium can be superior to it. Finding this equilibrium is NP-complete and, for a fixed number of players, there is a polynomial time reduction to solving two player mean-payoff games.

The distributed synthesis problem of safety and reachability languages is known to be undecidable. In this article, we establish that this is the case for very simple languages, namely for safety and reachability specifications in the intersection of LTL and ACTL.

Model checking is a well-established technique for the formal verification of concurrent and distributed systems. In recent years, model checking has been extended and adapted for multi-agent systems, primarily to enable the formal analysis of belief–desire–intention systems. While this has been successful, there is a need for more complex logical frameworks in order to verify realistic multi-agent systems. In particular, probabilistic and real-time aspects, as well as knowledge, belief, goals, etc., are required. However, the development of new model checking tools for complex combinations of logics is both difficult and time consuming. In this article, we show how model checkers for the constituent temporal, probabilistic, and real-time logics can be re-used in a modular way when we consider combined logics involving different dimensions. This avoids the re-implementation of model checking procedures. We define a modular approach, prove its correctness, establish its complexity, and show how it can be used to describe existing combined approaches and define yet-unimplemented combinations. We also demonstrate the feasibility of our approach on a case study.

We study the time-bounded reachability problem for continuous time Markov decision processes (CTMDPs) and games (CTMGs). Existing techniques for this problem use discretization techniques to break time into discrete intervals, and optimal control is approximated for each interval separately. Current techniques provide an accuracy of O(\epsilon^2) on each interval, which leads to an infeasibly large number of intervals. We propose a sequence of approximations that achieve accuracies of O(\epsilon^3), O(\epsilon^4), and O(\epsilon^5), that allow us to drastically reduce the number of intervals that are considered. For CTMDPs, the resulting algorithms are comparable to the heuristic approach given by Buckholz and Schulz, while also being theoretically justified. All of our results generalise to CTMGs, where our results yield the first practically implementable algorithms for this problem. We also provide positional strategies for both players that achieve similar error bounds.

Linear-Time Temporal Logic (LTL) is one of the most influential logics for the specification and verification of reactive systems. An important selling point of LTL is its striking simplicity, which might be a reason why none of the many extensions suggested to LTL have gained the same influence. Interval based temporal logics like Interval Temporal Logic (ITL) are a more recent branch of temporal logics with their own niche of interesting applications. On first glance, interval based temporal logics very little resemble LTL and the spread of these logics beyond their niche is hampered by a seeming structural incompatibility with LTL. When competing for being applied on a larger scale, interval based temporal logics would fight a losing battle against a more established competitor with better complexity and mature tools. In this paper, we suggest to extend ITL to Pop Logic (PL) by introducing a simple pop operator that revokes the binding of the chop operation-very much like the popping operation in a stack-and show that LTL can be viewed as a syntactic subset of PL. This is a surprising twist: by strengthening the comparably exotic logic ITL slightly and by using the new pop and the old chop operator as primitive constructs, we obtain a logic for which LTL is a de-facto syntactic fragment. The power of this extension is that it can, by subsuming both interval and classic temporal logics, synthesise both concepts to a common framework. The charm of this extension is that PL does not sacrifice the simplicity that makes its sub-logics attractive.

In this paper we study the problem of minimising deterministic automata over finite and infinite words. Deterministic finite automata are the simplest devices to recognise regular languages, and deterministic \buchi, \cobuchi, and parity automata play a similar role in the recognition of $\omega$-regular languages. While it is well known that the minimisation of deterministic finite and weak automata is cheap, the complexity of minimising deterministic \buchi\ and parity automata has remained an open challenge. We establish the NP-completeness of these problems. A second contribution of this paper is the introduction of almost equivalence, an equivalence class for strictly between language equivalence for deterministic \buchi\ or \cobuchi\ automata and language equivalence for deterministic finite automata. Two finite automata are almost equivalent if they, when used as a monitor, provide a different answer only a bounded number of times in any run, and we call the minimal such automaton relatively minimal. Minimisation of DFAs, hyper-minimisation, relative minimisation, and the minimisation of deterministic \buchi\ (or \cobuchi) automata are operations of increasing reduction power, as the respective equivalence relations on automata become coarser from left to right. Besides being a natural equivalence relation for finite automata, almost equivalence is language preserving for weak automata, and can therefore also be viewed as a generalisation of language equivalence for weak automata to a more general class of automata. From the perspective of \buchi\ and \cobuchi\ automata, we gain a cheap algorithm for state-space reduction that also turns out to be beneficial for further heuristic or exhaustive state-space reductions put on top of it.

The precise complexity of complementing B\"uchi\ automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple -- it suffices to determinize them using a simple subset construction and to dualize the acceptance condition of the resulting automaton -- B\"uchi\ complementation is more involved. Indeed, the construction of an EXPTIME complementation procedure took a quarter of a century from the introduction of B\"uchi\ automata in the early $60$s, and stepwise narrowing the gap between the upper and lower bound to a simple exponent (of $(6e)^n$ for B\"uchi\ automata with $n$ states) took four decades. While the distance between the known upper ($O\big((0.96\,n)^n\big)$) and lower ($\Omega\big((0.76\,n)^n\big)$) bound on the required number of states has meanwhile been significantly reduced, an exponential factor remains between them. Also, the upper bound on the size of the complement automaton is not linear in the bound of its state space. These gaps are unsatisfactory from a theoretical point of view, but also because B\"uchi\ complementation is a useful tool in formal verification, in particular for the language containment problem. This paper proposes a B\"uchi\ complementation algorithm whose complexity meets, modulo a quadratic ($O(n^2)$) factor, the known lower bound for B\"uchi\ complementation. It thus improves over previous constructions by an exponential factor and concludes the quest for optimal B\"uchi\ complementation algorithms.

We present an automatic method for the synthesis of certificates for components in embedded real-time systems. A certificate is a small homomorphic abstraction that can transparently replace the component during model checking: if the verification with the certificate succeeds, then the component is guaranteed to be correct; if the verification with the certificate fails, then the component itself must be erroneous. We give a direct construction, based on a forward and backward reachability analysis of the timed system, and an iterative refinement process, which produces a series of successively smaller certificates. In our experiments, model checking the certificate is several orders of magnitude faster than model checking the original system.

We provide a uniform solution to the problem of synthesizing a finite-state distributed system. An instance of the synthesis problem consists of a system architecture and a temporal specification. The architecture is given as a directed graph, where the nodes represent processes (including the environment as a special process) that communicate synchronously through shared variables attached to the edges. The same variable may occur on multiple outgoing edges of a single node, allowing for the broadcast of data. A solution to the synthesis problem is a collection of finite-state programs for the processes in the architecture, such that the joint behavior of the programs satisfies the specification in an unrestricted environment. We define information forks, a comprehensive criterion that characterizes all architectures with an undecidable synthesis problem. The criterion is effective: for a given architecture with n processes and v variables, it can be determined in O(n/sup 2//spl middot/v) time whether the synthesis problem is decidable. We give a uniform synthesis algorithm for all decidable cases. Our algorithm works for all /spl omega/-regular tree specification languages, including the /spl mu/-calculus. The undecidability proof, on the other hand, uses only LTL or, alternatively, CTL as the specification language. Our results therefore hold for the entire range of specification languages from LTL/CTL to the /spl mu/-calculus.