Belief-Desire-Intention (BDI) is a framework for modelling agents based on their beliefs, desires, and intentions. Plans are a central component of BDI agents, and define sequences of actions that an agent must undertake to achieve a certain goal. Existing approaches to plan generation often require significant manual effort, and are mainly focused on single-agent systems. As a result, in this work, we have developed a tool that automatically generates BDI plans using Alternating-Time Temporal Logic (ATL). By using ATL, the plans generated accommodate for possible competition or cooperation between the agents in the system. We demonstrate the effectiveness of the tool by generating plans for an illustrative game that requires agent collaboration to achieve a shared goal. We show that the generated plans allow the agents to successfully attain this goal.
Classic reachability games on graphs are zero-sum games, where the goal of one player, Eve, is to visit a vertex from a given target set, and that of other player, Adam, is to prevent this. Generalised reachability games, studied by Fijalkow and Horn, are a generalisation of reachability objectives, where instead of a single target set, there is a family of target sets and Eve must visit all of them in any order. In this work, we further study the complexity of solving two-player games on graphs with generalised reachability objectives. Our results are twofold: first, we provide an improved complexity picture for generalised reachability games, expanding the known tractable class from games in which all target sets are singleton to additionally allowing a logarithmic number of target sets of arbitrary size. Second, we study optimisation variants of generalised reachability with a focus on the size of the target sets. For these problems, we show intractability for most interesting cases. Particularly, in contrast to the tractability in the classic variant for singleton target sets, the optimisation problem is NP-hard when Eve tries to maximise the number of singleton target sets that are visited. Tractability can be recovered in the optimisation setting when all target sets are singleton by requiring that Eve pledges a maximum sized subset of target sets that she can guarantee to visit.
Chains of co-Buchi automata (COCOA) have recently been introduced as a new canonical model for representing arbitrary w-regular languages. They can be minimized in polynomial time and are hence an attractive language representation for applications in which normally, deterministic wautomata are used. While it is known how to build COCOA from deterministic parity automata, little is currently known about their relationship to automaton models introduced earlier than COCOA. In this paper, we analyze the conciseness of chains of co-Buchi automata. We show that even in the case that all automata in the chain are deterministic, chains of co-Buchi automata can be exponentially more concise than deterministic parity automata. We then answer the question if this conciseness is retained when performing Boolean operations (such as disjunction and conjunction) over COCOA by showing that there exist families of languages for which these operations lead to an exponential growth of the sizes of the automata. The families have the property that when representing them using deterministic parity automata, taking the disjunction or conjunction of them only requires a polynomial blow-up, which shows that Boolean operations over COCOA do not retain their conciseness in general.
This paper proposes appropriate sound and complete proof systems for algebraic structure over metric spaces by combining the development of Quantitative Equational Theories (QET) with the Enriched Lawvere Theories. We extend QETs to Metric Equational Theories (METs) where operations no longer have finite sets as arities (as in QETs and in the general theory of universal algebras), but arities are now drawn from countable metric spaces. This extension is inspired by the theory of Enriched Lawvere Theories which suggests that the arities of operations should be the 2,-presentable objects of the underlying 2,-accessible category. In this setting, the validity of terms in METs can no longer be guaranteed independently of the validity of equations, as it is the case with QET. We solve this problem, and adapt the sound and complete proof system for QETs to these more general METs, taking advantage of the specific structure of metric spaces.
In this paper, we study First Order Logic (FO) over (unordered) infinite trees and its connection with branching-time temporal logics. More specifically, we provide an automata-theoretic characterisation of FO interpreted over infinite trees. To this end, two different classes of hesitant tree automata are introduced and proved to capture precisely the expressive power of two branching time temporal logics, denoted cCTL(+/-)(p) and cCTL(f)(star), which are, respectively, a restricted version of counting CTL with past and counting CTL star over finite paths, both of which have been previously shown equivalent to FO over infinite trees. The two automata characterisations naturally lead to normal forms for the two temporal logics, and highlight the fact that FO can only express properties of the tree branches which are either safety or co-safety in nature.
We study provably correct and efficient instantiations of Sequential Monte Carlo (SMC) inference in the context of formal operational semantics of Probabilistic Programs (PPs). We focus on universal PPs featuring sampling from arbitrary measures and conditioning/reweighting in unbounded loops. We first equip Probabilistic Program Graphs (PPGs), an automata-theoretic description format of PPs, with an expectation-based semantics over infinite execution traces, which also incorporates trace weights. We then prove a finite approximation theorem that provides bounds to this semantics based on expectations taken over finite, fixed-length traces. This enables us to frame our semantics within a Feynman-Kac (FK) model, and ensures the consistency of the Particle Filtering (PF) algorithm, an instance of SMC, with respect to our semantics. Building on these results, we introduce VPF, a vectorized version of the PF algorithm tailored to PPGs and our semantics. Experiments conducted with a proof-of-concept implementation of VPF show very promising results compared to state-of- the-art PP inference tools.
This paper studies the complexity of determining whether a formula in the modal logics characterizing the nested-simulation semantics is characteristic for some process, which is equivalent to determining whether the formula is satisfiable and prime. The main results are that the problem of determining whether a formula is prime in the modal logic characterizing the 2-nested-simulation preorder is coNP-complete and is PSPACE-complete in the case of the n-nested-simulation preorder, when n>=3. This establishes that deciding characteristic formulae for the n-nested simulation semantics is PSPACE-complete, when n>=3. In the case of the 2-nested simulation semantics, that problem lies in the complexity class DP, which consists of languages that can be expressed as the intersection of one language in NP and of one in coNP.
We study rational synthesis problems for concurrent games with omega-regular objectives. Our model of rationality considers only pure strategy Nash equilibria that satisfy either a social welfare or Pareto optimality condition with respect to an omega-regular objective for each agent. This extends earlier work on equilibria in concurrent games, without consideration about their quality. Our results show that the existence of Nash equilibria satisfying social welfare conditions can be computed as efficiently as the constrained Nash equilibrium existence problem. On the other hand, the existence of Nash equilibria satisfying the Pareto optimality condition possibly involves a higher upper bound, except in the case of B & uuml;chi and Muller games, for which all three problems are in the classes P and PSPACE-complete, respectively.
We settle the complexity of satisfiability and model-checking for generalized HyperLTL with stuttering and contexts, an expressive logic for the specification of asynchronous hyperproperties. Such properties cannot be specified in HyperLTL, as it is restricted to synchronous hyperproperties. Nevertheless, we prove that satisfiability is Sigma(1)(1)-complete and thus not harder than for HyperLTL. On the other hand, we prove that model-checking is equivalent to truth in second-order arithmetic, and thus much harder than the decidable HyperLTL model-checking problem. The lower bounds for the model-checking problem hold even when only allowing stuttering or only allowing contexts.
Algorithmic analysis of Markov decision processes (MDP) and stochastic games (SG) in practice relies on value-iteration (VI) algorithms. Since basic VI does not provide guarantees on the precision of the result, variants of VI have been proposed that offer such guarantees. In particular, sound value iteration (SVI) not only provides precise lower and upper bounds on the result, but also converges faster in the presence of probabilistic cycles. Unfortunately, it is neither applicable to SG, nor to MDP with end components. In this paper, we extend SVI and cover both cases. The technical challenge consists mainly in proper treatment of end components, which require different handling than in the literature. Moreover, we provide several optimizations of SVI. Finally, we evaluate our prototype implementation experimentally to demonstrate its potential on systems with probabilistic cycles.
We consider games played on the transition graph of concurrent programs running under the Total Store Order (TSO) weak memory model. Games are frequently used to model the interaction between a system and its environment, in this case between the concurrent processes and the nondeterministic TSO buffer updates. In our formulation, the game is played by two players, who alternatingly make a move: The process player can execute any enabled instruction of the processes, while the update player takes care of updating the messages in the buffers that are between each process and the shared memory. We show that the reachability and safety problem of this game reduce to the analysis of single-process (non-concurrent) programs. In particular, they exhibit only finite-state behaviour. Because of this, we introduce different notions of fairness, which force the two players to behave in a more realistic way. Both the reachability and safety problem then become undecidable.
Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPAC[-complete; in particular, PSPAC[-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.
We study parallel algorithms for the minimization of Deterministic Finite Automata (DFAs). In particular, we implement four different massively parallel algorithms for DFA minimization on Graphics Processing Units (GPUs). Our results confirm the expectations that the algorithm with the theoretically best time complexity is not practically suitable to run on GPUs due to the large amount of resources needed. We empirically verify that parallel partition refinement algorithms from the literature perform better in practice, even though their time complexity is worse. Lastly, we introduce a novel algorithm based on partition refinement with an extra parallel partial transitive closure step and show that on specific benchmarks it has better run-time complexity and performs better in practice.
As business processes become increasingly complex, effectively modeling decision points, their likelihood, and resource consumption is crucial for optimizing operations. To address this challenge, this paper introduces a formal extension of the Business Process Model and Notation (BPMN) that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI. This extension is motivated by the growing emphasis on precise control within business process management, where carefully selecting decision pathways in repeated instances is crucial for conforming to certain standards of multiple resource consumption and environmental impacts. In this context we deal with the problem of synthesizing a strategy (if any) that guarantees that the expected impacts on repeated execution of the input process are below a given threshold. We show that this problem belongs to PSPACE complexity class; moreover we provide an effective procedure for computing a strategy (if present).
We present a type of epistemic logics that encapsulates both the dynamics of acquiring knowledge (knowing) and losing information (forgetting), alongside the integration of group knowledge concepts. Our approach is underpinned by a system of weighted models, which introduces an "epistemic skills" metric to effectively represent the epistemic abilities associated with knowledge update. In this framework, the acquisition of knowledge is modeled as a result of upskilling, whereas forgetting is by downskilling. Additionally, our framework allows us to explore the concept of "knowability," which can be defined as the potential to acquire knowledge through upskilling, and facilitates a nuanced understanding of the distinctions between epistemic de re and de dicto expressions. We study the computational complexity of model checking problems for these logics, providing insights into both the theoretical underpinnings and practical implications of our approach.
We introduce deterministic suffix-reading automata (DSA), a new automaton model over finite words. Transitions in a DSA are labeled with words. From a state, a DSA triggers an outgoing transition on seeing a word ending with the transition's label. Therefore, rather than moving along an input word letter by letter, a DSA can jump along blocks of letters, with each block ending in a suitable suffix. This feature allows DSAs to recognize regular languages more concisely, compared to DFAs. In this work, we focus on questions around finding a "minimal" DSA for a regular language. The number of states is not a faithful measure of the size of a DSA, since the transition-labels contain strings of arbitrary length. Hence, we consider total-size (number of states + number of edges + total length of transition-labels) as the size measure of DSAs. We start by formally defining the model and providing a DSA-to-DFA conversion that allows to compare the expressiveness and succinctness of DSA with related automata models. Our main technical contribution is a method to derive DSAs from a given DFA: a DFA-to-DSA conversion. We make a surprising observation that the smallest DSA derived from the canonical DFA of a regular language L need not be a minimal DSA for L. This observation leads to a fundamental bottleneck in deriving a minimal DSA for a regular language. In fact, we prove that given a DFA and a number k, the problem of deciding if there exists an equivalent DSA of total-size at most k is NP-complete.
Selecting the combination of security controls that will most effectively protect a system's assets is a difficult task. If the wrong controls are selected, the system may be left vulnerable to cyberattacks that can impact the confidentiality, integrity and availability of critical data and services. In practical settings, it is not possible to select and implement every control possible. Instead considerations, such as budget, effectiveness, and dependencies among various controls, must be considered to choose a combination of security controls that best achieve a set of system security objectives. In this paper, we propose a game-theoretic approach for selecting effective combinations of security controls based on expected attacker profiles and a set budget. The control selection problem is set up as a two-person zero-sum one-shot game. Valid control combinations for selection are generated using an algebraic formalism to account for dependencies among selected controls. We demonstrate the proposed approach on an illustrative financial system used in government departments under four different scenarios. The results illustrate how a security analyst can use the proposed approach to guide and support decision-making in the control selection activity when developing secure systems.
The synthesis of reactive systems aims for the automated construction of strategies for systems that interact with their environment. Whereas the synthesis approach has the potential to change the development of reactive systems significantly due to the avoidance of manual implementation, it still suffers from a lack of efficient synthesis algorithms for many application scenarios. The translation of the system specification into an automaton that allows for strategy construction (if a winning strategy exists) is nonelementary in the length of the specification in S1S and doubly exponential for LTL, raising the need of highly specialized algorithms. In this article, we present an approach on how to reduce this state space explosion in the construction of this automaton by exploiting a monotonicity property of specifications. For this, we introduce window counting constraints that allow for step-wise refinement or abstraction of specifications. In an iterative synthesis procedure, those window counting constraints are used to construct automata representing over- or under-approximations (depending on the counting constraint) of constraint-compliant behavior. Analysis results on winning regions of previous iterations are used to reduce the size of the next automaton, leading to an overall reduction of the state space explosion extent. We present the implementation results of the iterated synthesis for a zero-sum game setting as proof of concept. Furthermore, we discuss the current limitations of the approach in a zero-sum setting and sketch future work in non-zero-sum settings.
Jumping automata are finite automata that read their input in a non-sequential manner, by allowing a reading head to "jump" between positions on the input, consuming a permutation of the input word. We argue that allowing the head to jump should incur some cost. To this end, we propose three quantitative semantics for jumping automata, whereby the jumps of the head in an accepting run define the cost of the run. The three semantics correspond to different interpretations of jumps: the absolute distance semantics counts the distance the head jumps, the reversal semantics counts the number of times the head changes direction, and the Hamming distance measures the number of letter-swaps the run makes. We study these measures, with the main focus being the boundedness problem: given a jumping automaton, decide whether its (quantitative) languages is bounded by some given number k . We establish the decidability and complexity for this problem under several variants.
We study the advantages of reconfigurable communication interfaces vs fixed communication interfaces in the context of asynchronous automata. We study the extension of asynchronous (Zielonka) automata with reconfigurable communication interfaces. We show that it is possible to capture languages of automata with reconfigurable communication interfaces by automata with fixed communication interfaces. However, this comes at a cost of disseminating communication (and knowledge) to all agents in a system. Thus, the system is no longer behaving as a distributed system. We then show that this is unavoidable by describing a language in which every agent that uses a fixed communication interface either must be aware of all communication or become irrelevant.
