We investigate the decidability/complexity status of the model-checking problem for an ability-based logic expressing knowing how assertions and enriched with budget constraints. To do so, we introduce a new control-state reachability problem for complete vector addition systems with states where the transitions are labelled by letters from a finite alphabet. It is required that all runs labelled by a given word lead synchronously to the target control states. First, we show that the model-checking problem involving knowing how can be reduced to the new problem on VASS. Second, we establish Ack-completeness of both problems by properly adapting or using developments about well-structured transition systems, belief functions and length function theorems.
This paper proposes linear time algorithms for the Maximum Path Set (MPS) problem in undirected trees and arborescences. In the MPS problem, we are given a graph G = ( V, E ) and asked to find a maximum cardinality set of edges E' ⊆ E , such that G'= ( V, E' ) is a collection of vertex-disjoint paths. The MPS problem finds applications in a number of logistics domains. In [3], it was shown that this problem is NP-complete in general graphs. This paper demonstrates that the MPS problem is solvable in linear time in undirected trees. Additionally, we reduce the MPS problem to the b-matching problem, which in turn can be reduced to the Maximum Flow problem. From a polyhedral perspective, we design an integer program for the MPS problem in trees and prove that the constraint matrix of this formulation is totally unimodular. In other words, solving the linear programming relaxation provides an integral solution. We also design a linear time algorithm to solve the MPS problem in arborescences, which form a class of directed trees. Finally, we empirically analyze the various algorithms discussed in this paper.
We provide an overview of three projects that explore the idea of using coverage-guided fuzzing, a technique traditionally used for finding bugs in software, in unconventional domains: (1) efficiently solving SMT formulas that use floating-point constraints; (2) achieving fast SMT sampling for such formulas; and (3) simulating operational memory models. In each case, the idea is to reduce the problem at hand into a reachability problem: transforming a problem instance into a program equipped with a special error location, such that finding an input that reaches the error location equates to finding a solution to the problem instance. Coverage-guided fuzzing, which excels at mutating a corpus of inputs to achieve increasing statement coverage of a system under test, can then be used to search for an input that reaches the error location—i.e., for a solution to the problem instance. We hope this overview will inspire other researchers to consider recasting search problems into a reachability problem form where coverage-guided fuzzing may prove effective.
Reachability and mortality are fundamental problems in the study of hybrid dynamical systems. Reachability investigates whether a system can evolve from an initial state to a designated target state, while mortality asks whether the system inevitably halts or reaches a deadlock state under its given dynamics. In this work, we study these problems for two-dimensional restricted hierarchical piecewise constant derivative systems ( 2 -RHPCD), a class characterised by a hierarchical structure and piecewise-constant dynamics. We prove that both reachability and mortality are co-NP-hard for bounded 2 -RHPCD systems. In particular, our result resolves the open question posed in [4] concerning the complexity of the mortality problem for 2 -RHPCD systems.
We consider two reachability analysis methods for feedforward neural networks, which use star sets as datatype to store network states. While the first method is complete but computationally expensive, the second method offers better scalability by using over-approximations and thus sacrifying completeness. In this paper, we propose a counterexample-guided abstraction refinement (CEGAR) framework to combine the strengths of these two procedures, starting with the second method, and iteratively refining the over-approximation based on spurious counterexamples. Our algorithm is complete and it either certifies safety or it returns a counterexample as a proof of unsafety. We suggest multiple heuristics for the refinement and evaluate them experimentally, demonstrating that our CEGAR-based approach is more efficient than a previously proposed direct abstraction refinement method, and on some benchmarks, it significantly outperforms the exact method.
The problem of determining whether a word equation admits a solution whose lengths belong to some semilinear set is fundamental to the theory of string-solving. Despite this and connections to Hilbert’s Tenth Problem, its decidability has been open since 1968. We prove this problem decidable for the class of quadratic word equations in at most two unknowns. We use a novel technique recasting the problem as halfspace reachability in the matrix semigroup SA(n,ℕ) . We also look at word equations’ length abstractions: the sets of their solutions’ length-vectors. It is known that these need not be semilinear; with the above problem in mind we seek to understand their expressivity. We show that the length abstractions of quadratic word equations differ finitely from unions of arithmetic progressions. Tools for showing inexpressibility by regular and quadratic word equations result. Each relation definable in existential Presburger arithmetic with divisibility ( ) can be built from word equations’ length abstractions. Conversely, the length abstraction of Xw_1Y·=Yw_2X is shown -equidefinable with a certain vector reachability problem.
Computing the probability of reaching a set of goal states G in a discrete-time Markov chain (DTMC) is a core task of probabilistic model checking. We can do so by directly computing the probability mass of the set of all finite paths from the initial state to G; however, when refining counterexamples, it is also interesting to compute the probability mass of subsets of paths. This can be achieved by splitting the computation into path abstractions that calculate “local” reachability probabilities as shown by Ábrahám et al. in 2010. In this paper, we complete and extend their work: We prove that splitting the computation into path abstractions indeed yields the same result as the direct approach, and that the splitting does not need to follow the SCC structure. In particular, we prove that path abstraction can be performed along any finite sequence of sets of non-goal states. Our proofs proceed in a novel way by interpreting the DTMC as a structure on the free monoid on its state space, which makes them clean and concise. Additionally, we provide a compact reference implementation of path abstraction in PARI/GP.
The advent of transformers has in recent years led to powerful and revolutionary Large Language Models (LLMs). Despite this, our understanding on the capability of transformers is still meager. In this invited contribution, we recount the rapid progress in the last few years to the question of what transformers can do. In particular, we will see the integral role of logic and automata (also with some help from circuit complexity) in answering this question. We also mention several open problems at the intersection of logic, automata, verification and transformers.
In the game-theoretic approach to controller synthesis, we model the interaction between a system to be controlled and its environment as a game between these entities, and we seek an appropriate (e.g., winning or optimal) strategy for the system. This strategy then serves as a formal blueprint for a real-world controller. A common belief is that simple (e.g., using limited memory) strategies are better: corresponding controllers are easier to conceive and understand, and cheaper to produce and maintain. This invited contribution focuses on the complexity of strategies in a variety of synthesis contexts. We discuss recent results concerning memory and randomness, and take a brief look at what lies beyond our traditional notions of complexity for strategies.
In 2011, Fici and Lipták introduced prefix normal words. A binary word is prefix normal if it has no factor (substring) that contains more occurrences of the letter 1 than the prefix of the same length. Among the open problems regarding this topic are the enumeration of prefix normal words and efficient testing methods. We show a range of characteristics of prefix normal words. These include properties of factors that are responsible for a word not being prefix normal. With word chains and generators, we introduce new ways of relating words of the same length to each other.
The bandwidth of a timed language characterizes the quantity of information per time unit (with a finite observation precision ε ). Obese timed automata have an unbounded frequency of events and produce information at the maximal possible rate. In this article, we compute the bandwidth of any such automaton in the form ≈α /ε . Our approach reduces the problem to computing the best reward-to-time ratio in a weighted timed graph constructed from the given timed automaton, with weights corresponding to the entropy of auxiliary finite automata.
We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy—or shield—for Markov decision processes over continuous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and then solve a two-player safety game [9], which entails a number of algorithmically hard problems such as reachability for hybrid systems. The general philosophy of Uppaal Coshy is to approximate hard-to-obtain solutions using simulations. Our implementation is fully automatic and supports the expressive formalism of Uppaal models, which encompass stochastic hybrid automata. The precision of our partition-based approach benefits from using finer grids, which however are not efficient to store. We include an algorithm called Caap to efficiently compute a compact representation of a shield in the form of a decision tree, which yields significant reductions.
This paper studies the verification of almost-sure Büchi objectives in MDPs with a known, compositional structure based on string diagrams. In particular, we ask whether there is a strategy that ensures that a Büchi objective is almost-surely satisfied. We first show that proper exit sets—the sets of exits that can be reached within a component without losing locally—together with the reachability of a Büchi state are a sufficient and necessary statistic for the compositional verification of almost-sure Büchi objectives. The number of proper exit sets may grow exponentially in the number of exits. We define two algorithms: (1) A straightforward bottom-up algorithm that computes this statistic in a recursive manner to obtain the verification result of the entire string diagram and (2) a polynomial-time iterative algorithm which avoids computing all proper exit sets by performing iterative strategy refinement.
We consider a variant of reachability in Vector Addition Systems (VAS) dubbed box reachability, whereby a vector v∈ℕ^d is box-reachable from 0 in a VAS 𝒱 if 𝒱 admits a path from 0 to v that not only stays in the positive orthant (as in the standard VAS semantics), but also stays below v , i.e., within the “box” whose opposite corners are 0 and v . Our main result is that for two-dimensional VAS, the set of box-reachable vertices almost coincides with the standard reachability set: the two sets coincide for all vectors whose coordinates are both above some threshold W. We also study properties of box-reachability, exploring the differences and similarities with standard reachability. Technically, our main result is proved using powerful machinery from convex geometry.
Elementary Object Systems (EOSs) are a model in the nets-within-nets (NWNs) paradigm, where tokens in turn can host standard Petri nets. We study the complexity of the reachability problem of EOSs when subjected to non-deterministic token losses. It is known that this problem is equivalent to the coverability problem with no lossiness of conservative EOSs (cEOSs). We precisely characterize cEOS coverability into the framework of data nets, whose tokens carry data from an infinite domain. Specifically, we show that cEOS coverability is equivalent to the coverability of an interesting fragment of data nets that extends beyond ν PN (featuring globally fresh name creation), yet remains less expressive than Unordered Data Nets (featuring lossy name creation as well as powerful forms of whole-place operations and broadcasts). This insight bridges two apparently orthogonal approaches to PN extensions, namely data nets and NWNs. At the same time, it enables us to analyze cEOS coverability taking advantage of known results on data nets. As a byproduct, we immediately get that the complexity of cEOS coverability lies between F_ω 2 and F_ω ^ω , two classes beyond Primitive Recursive.
We present a method for constructing discrete abstractions for discrete-time, continuous-state systems. Related approaches construct a discrete bisimulation, which leaves little room for non-determinism in the outputs and quickly leads to highly complex models since all concrete behavior is covered. Our approach is to relax these requirements and build a satisficing solution: a discrete abstraction that is deterministic, robust, and as complete as possible under the given parameters. This allows us to balance granularity and computational feasibility. We leverage linearization and linear feedback control to extend the approach from globally contractive systems to systems with contractive cycles. The resulting abstraction directly induces a supervisor policy. The approach is illustrated with numerical experiments and has potential applications in various domains where system safety and reversibility are essential.
We present a theory of rewriting a word into a given target language. We show that the natural notion of equivalence between corrections as sequences of edit operations can be captured syntactically by means of a rather simple rewrite system. Completeness relies on a normal form for corrections that is then also used to develop a notion of minimality for corrections. This is not based on edit distance between words and languages but on a subsequence order on corrections, capturing the intuitive notion of doing a minimal number of rewriting steps. We show that the number of minimal corrections is always finite, and that they are computable for context-free languages.
Logically constrained term rewrite systems are useful models of not only sequential but also concurrent programs. We have proposed a framework to soundly reduce starvation freedom of a concurrent program to an all-path reachability problem of the corresponding logically constrained term rewrite system, where process fairness is not considered. In this paper, we show a disproof criterion for starvation freedom and then extend the framework to starvation freedom under process fairness.
We study the problem of computing the reachable principals of the simulation preorder and the reachable blocks of simulation equivalence. Following a theoretical investigation of this problem, which highlights a sharp contrast with the already settled case of bisimulation, we design algorithms to solve this problem by leveraging the idea of interleaving reachability and simulation computation while possibly avoiding the computation of all the reachable states or the whole simulation preorder. In particular, we put forward a symbolic algorithm processing state partitions and, in turn, relations between their blocks, which is suited for processing infinite-state systems.
This paper introduces Semi-Linear Integer Vector Addition Systems with Resets (SVASR). A SVASR is a labeled transition system in which the states are finite-dimensional integer-valued vectors and which transitions from one state to another by applying an orthogonal projection followed by a translation drawn from a semi-linear set. We give a polynomial-time reduction of SVASR reachability to that of Integer Vector Addition Systems with Resets. We then consider the use of SVASRs for over-approximating the reachability relation of transition systems in which the transition relation is a semi-linear set. We show that any semi-linear transition system has a "best" SVASR that simulates its behavior, called its SVASR-reflection. The dimension of the SVASR-reflection of a semi-linear transition system T with states is exponential in the number of states; however, we show that the over-approximate reachability induced by T's SVASR-reflection can be computed in polynomial time.
