Abstract To mitigate the state explosion problem in model checking, abstraction techniques provide sound but typically incomplete approximations of a system’s behaviour. While complete abstractions eliminate false alarms, they are often impractical—or even uncomputable—due to their high computational cost. We introduce semi-completeness, a relaxed notion of completeness that retains sufficient precision to capture a system’s behaviour over relevant regions of the domain. Building on this, we develop abstraction refinement algorithms that compute semi-complete abstractions without incurring the cost of full completeness. Furthermore, we present an algorithm that interleaves abstraction refinement with fixed-point computations—specifically reachability analysis. This achieves semi-completeness on-the-fly, without requiring prior knowledge of the region of interest, such as the reachable states. We demonstrate the effectiveness of our approach on fragments of the $$\mu $$ μ -calculus, showing that our abstractions preserve the validity of formulae over all reachable states.

We present a Myhill-Nerode style characterization for languages recognized by one-clock deterministic timed automata ( $$1$$ -DTA). Although there is only one clock, distinct automata may reset it differently along the same word. This adds a significant challenge in the search for a canonical automaton. Our characterization is based on a new perspective of $$1$$ -DTAs in terms of “half-integral” words that they accept, along with the reset information encoded by them We apply our results to develop $$\mathsf {L^*}$$ style algorithms that learn the canonical $$1$$ -DTA.

Abstract Hyperproperties are properties over sets of traces (or runs) of a system, as opposed to properties of just one trace. They were introduced in 2010 and have been much studied since, in particular via an extension of the temporal logic LTL called HyperLTL. Most verification efforts for HyperLTL are restricted to finite-state systems, usually defined as Kripke structures. In this paper we study hyperproperties for an important class of infinite-state systems. We consider population protocols, a popular distributed computing model in which arbitrarily many identical finite-state agents interact in pairs. Population protocols are a good candidate for studying hyperproperties because the main decidable verification problem, well-specification, is a hyperproperty. We first show that even for simple (monadic) formulas, HyperLTL verification for population protocols is undecidable. We then turn our attention to immediate observation population protocols, a simpler and well-studied subclass of population protocols. We show that verification of monadic HyperLTL formulas without the next operator is decidable in 2-EXPSPACE, but that all extensions make the problem undecidable.

Lower bounds provide essential insights into the minimal computational resources required for algorithm execution. This paper focuses on logical theories, a domain where estimating resources is particularly difficult, and provides a novel, fully-automated method for computing lower bounds on memory usage, serving as a proxy for the computational resources required to perform logical reasoning. Specifically, the paper focuses on computing lower bounds on the size of the minimal deterministic finite automaton that encodes the solution set of a given Presburger arithmetic (also known as linear integer arithmetic) formula. The lower bounds are accompanied by independently verifiable certificates which also support a union-like operation that can be used to increase the computed bounds.We conducted an extensive empirical evaluation of our method using over 5 000 formulae from the quantifier-free fragment of Presburger arithmetic, sourced from the SMT-LIB repository. The results show that our method often produces lower bounds that are close to the actual size of the minimal deterministic finite automaton. Moreover, it succeeds in computing non-trivial bounds even for instances that are out of reach (by several orders of magnitude) for the existing state-of-the-art automata-based tools for solving Presburger arithmetic.

We investigate the problem of computing the reachable blocks of the simulation equivalence and its natural counterpart for the simulation preorder, referred to as the reachable simulation problem . Through a theoretical investigation of this problem, we unveil a sharp contrast with the already settled case of bisimulation equivalence. Then, we design algorithms to solve the reachable simulation 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. Specifically, we propose algorithms achieving different guarantees on the precision of the output, and a symbolic algorithm that operates on state partitions and relations between their blocks, which is particularly well-suited for processing infinite-state systems.

The well-known Nerode equivalence for finite words plays a fundamental role in our understanding of the class of regular languages. The equivalence leads to the Myhill-Nerode theorem and a canonical automaton, which in turn, is the basis of several automata learning algorithms. A Nerode-like equivalence has been studied for various classes of timed languages. In this work, we focus on timed automata with integer resets. This class is known to have good automata-theoretic properties and is also useful for practical modeling. Our main contribution is a Nerode-style equivalence for this class that depends on a constant K. We show that the equivalence leads to a Myhill-Nerode theorem and a canonical one-clock integer-reset timed automaton with maximum constant K. Based on the canonical form, we develop an Angluin-style active learning algorithm whose query complexity is polynomial in the size of the canonical form.

Abstract We define novel algorithms for the inclusion problem between two visibly pushdown languages of infinite words, an EXPTime -complete problem. Our algorithms search for counterexamples to inclusion in the form of ultimately periodic words i.e. words of the form $$uv^{\omega }$$ u v ω where $$u$$ u and $$v$$ v are finite words. They are parameterized by a pair of quasiorders telling which ultimately periodic words need not be tested as counterexamples to inclusion without compromising completeness. The pair of quasiorders enables distinct reasoning for prefixes and periods of ultimately periodic words thereby allowing to discard even more words compared to using the same quasiorder for both. We put forward two families of quasiorders: the state-based quasiorders based on automata and the syntactic quasiorders based on languages. We also implemented our algorithm and conducted an empirical evaluation on benchmarks from software verification.

Abstract We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSpace-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called Forklift, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870

We introduce an algorithmic framework to decide whether inclusion holds between languages of infinite words over a finite alphabet. Our approach falls within the class of Ramsey-based methods and relies on a least fixpoint characterization of ω-languages leveraging ultimately periodic infinite words of type uv^ω, with u a finite prefix and v a finite period of an infinite word. We put forward an inclusion checking algorithm between Büchi automata, called BAInc, designed as a complete abstract interpretation using a pair of well-quasiorders on finite words. BAInc is quite simple: it consists of two least fixpoint computations (one for prefixes and the other for periods) manipulating finite sets (of pairs) of states compared by set inclusion, so that language inclusion holds when the sets (of pairs) of states of the fixpoints satisfy some basic conditions. We implemented BAInc in a tool called BAIT that we experimentally evaluated against the state-of-the-art. We gathered, in addition to existing benchmarks, a large number of new case studies stemming from program verification and word combinatorics, thereby significantly expanding both the scope and size of the available benchmark set. Our experimental results show that BAIT advances the state-of-the-art on an overwhelming majority of these benchmarks. Finally, we demonstrate the generality of our algorithmic framework by instantiating it to the inclusion problem of Büchi pushdown automata into Büchi automata.

We provide new insights on the determinization and minimization of tree automata using congruences on trees. From this perspective, we study a Brzozowski's style minimization algorithm for tree automata. First, we prove correct this method relying on the following fact: when the automata-based and the language-based congruences coincide, determinizing the automaton yields the minimal one. Such automata-based congruences, in the case of word automata, are defined using pre and post operators. Now we extend these operators to tree automata, a task that is particularly challenging due to the reduced expressive power of deterministic top-down (or equivalently co-deterministic bottom-up) automata. We leverage further our framework to offer an extension of the original result by Brzozowski for word automata. Comment: 47 pages, 2 figures

We study the language inclusion problem L 1 ⊆ L 2 , where L 1 is regular or context-free. Our approach relies on abstract interpretation and checks whether an overapproximating abstraction of L 1 , obtained by approximating the Kleene iterates of its least fixpoint characterization, is included in L 2 . We show that a language inclusion problem is decidable whenever this overapproximating abstraction satisfies a completeness condition (i.e., its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e., it guarantees termination of least fixpoint computations). This overapproximating abstraction of languages can be defined using quasiorder relations on words, where the abstraction gives the language of all the words “greater than or equal to” a given input word for that quasiorder. We put forward a range of such quasiorders that allow us to systematically design decision procedures for different language inclusion problems, such as regular languages into regular languages or into trace sets of one-counter nets, and context-free languages into regular languages. In the case of inclusion between regular languages, some of the induced inclusion checking procedures correspond to well-known state-of-the-art algorithms, like the so-called antichain algorithms. Finally, we provide an equivalent language inclusion checking algorithm based on a greatest fixpoint computation that relies on quotients of languages and, to the best of our knowledge, was not previously known.

In this work, we define a framework of automata constructions based on quasiorders over words to provide new insights on the class of residual automata. We present a new residualization operation and a generalized double-reversal method for building the canonical residual automaton for a given language. Finally, we use our framework to offer a quasiorder-based perspective on NL*, an online learning algorithm for residual automata. We conclude that quasiorders are fundamental to residual automata as congruences are to deterministic automata.

We show how to infer deterministic cache replacement policies using off-the-shelf automata learning and program synthesis techniques. For this, we construct and chain two abstractions that expose the cache replacement policy of any set in the cache hierarchy as a membership oracle to the learning algorithm, based on timing measurements on a silicon CPU. Our experiments demonstrate an advantage in scope and scalability over prior art and uncover two previously undocumented cache replacement policies.

We present an algorithm for searching regular expression matches in compressed text. The algorithm reports the number of matching lines in the uncompressed text in time linear in the size of its compressed version. We define efficient data structures that yield nearly optimal complexity bounds and provide a sequential implementation -zearch- that requires up to 25% less time than the state of the art.

In this work we use a framework of finite-state automata constructions based on equivalences over words to provide new insights on the relation between well-known methods for computing the minimal deterministic automaton of a language.

Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.

Parikh's Theorem states that every context-free grammar (CFG) is equivalent to some regular CFG when the ordering of symbols in the words is ignored. The same is not true for the so-called weighted CFGs, which additionally assign a weight to each grammar rule. If the result holds for a given weighted CFG G, we say that G satisfies the Parikh property. We prove constructively that the Parikh property holds for every weighted nonexpansive CFG. We also give a decision procedure for the property when the weights are over the rationals.

Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points.

Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODC 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates. In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.

We characterize the complexity of the safety verification problem for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem when processes are modeled by finite-state machines, pushdown machines, and Turing machines. The problem is coNP-complete when all processes are finite-state machines, and is PSPACE-complete when they are pushdown machines. The complexity remains coNP-complete when each Turing machine is allowed boundedly many interactions with the register. Our proofs use combinatorial characterizations of computations in the model, and in the case of pushdown systems, some language-theoretic constructions of independent interest. Our results are surprising, because parameterized verification problems on slight variations of our model are known to be undecidable. For example, the problem is undecidable for finite-state machines operating with synchronization primitives, and already for two communicating pushdown machines. Thus, our results show that a robust, decidable class can be obtained under the assumptions of anonymity and asynchrony.

Population protocols [Angluin et al., PODC, 2004] are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets.

We investigate the problem of verifying the absence of zeno executions in a hybrid system. A zeno execution is one in which there are infinitely many discrete transitions in a finite time interval. The presence of zeno executions poses challenges towards implementation and analysis of hybrid control systems. We present a simple transformation of the hybrid system which reduces the non-zenoness verification problem to the termination verification problem, that is, the original system has no zeno executions if and only if the transformed system has no non-terminating executions. This provides both theoretical insights and practical techniques for non-zenoness verification. Further, it also provides techniques for isolating parts of the hybrid system and its initial states which do not exhibit zeno executions. We illustrate the feasibility of our approach by applying it on hybrid system examples.

Pattern-based verification checks the correctness of program executions that follow a given pattern , a regular expression over the alphabet of program transitions of the form w 1 * … w n * . For multithreaded programs, the alphabet of the pattern is given by the reads and writes to the shared storage. We study the complexity of pattern-based verification for multithreaded programs with shared counters and finite variables. While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs (even without counters), we show that pattern-based verification is NP-complete for both classes, even in the presence of counters. We then conduct a multiparameter analysis to study the complexity of the problem on its three natural parameters (number of threads+counters+variables, maximal size of a thread, size of the pattern) and on two parameters related to thread structure (maximal number of procedures per thread and longest simple path of procedure calls). We present an algorithm that for a fixed number of threads, counters, variables, and pattern size solves the verification problem in st O ( lsp + ⌈ log ( pr +1) ⌉) time, where st is the maximal size of a thread, pr is the maximal number of procedures per thread, and lsp is the longest simple path of procedure calls.

A class of languages C is perfect if it is closed under Boolean operations and the emptiness problem is decidable. Perfect language classes are the basis for the automata-theoretic approach to model checking: a system is correct if the language generated by the system is disjoint from the language of bad traces. Regular languages are perfect, but because the disjointness problem for context-free languages is undecidable, no class containing them can be perfect. In practice, verification problems for language classes that are not perfect are often under-approximated by checking if the property holds for all behaviors of the system belonging to a fixed subset. A general way to specify a subset of behaviors is by using bounded languages. A class of languages C is perfect modulo bounded languages if it is closed under Boolean operations relative to every bounded language, and if the emptiness problem is decidable relative to every bounded language. We consider finding perfect classes of languages modulo bounded languages. We show that the class of languages accepted by multi-head pushdown automata are perfect modulo bounded languages, and characterize the complexities of decision problems. We also show that bounded languages form a maximal class for which perfection is obtained. We show that computations of several known models of systems, such as recursive multi-threaded programs, recursive counter machines, and communicating finite-state machines can be encoded as multi-head pushdown automata, giving uniform and optimal underapproximation algorithms modulo bounded languages.

Asynchronous programming is a ubiquitous systems programming idiom for managing concurrent interactions with the environment. In this style, instead of waiting for time-consuming operations to complete, the programmer makes a non-blocking call to the operation and posts a callback task to a task buffer that is executed later when the time-consuming operation completes. A cooperative scheduler mediates the interaction by picking and executing callback tasks from the task buffer to completion (and these callbacks can post further callbacks to be executed later). Writing correct asynchronous programs is hard because the use of callbacks, while efficient, obscures program control flow. We provide a formal model underlying asynchronous programs and study verification problems for this model. We show that the safety verification problem for finite-data asynchronous programs is expspace-complete. We show that liveness verification for finite-data asynchronous programs is decidable and polynomial-time equivalent to Petri net reachability. Decidability is not obvious, since even if the data is finite-state, asynchronous programs constitute infinite-state transition systems: both the program stack for an executing task and the task buffer of pending calls to tasks can be potentially unbounded. Our main technical constructions are polynomial-time, semantics-preserving reductions from asynchronous programs to Petri nets and back. The first reduction allows the use of algorithmic techniques on Petri nets for the verification of asynchronous programs, and the second allows lower bounds on Petri nets to apply also to asynchronous programs. We also study several extensions to the basic models of asynchronous programs that are inspired by additional capabilities provided by implementations of asynchronous libraries and classify the decidability and undecidability of verification questions on these extensions.

We investigate the problem asking whether the intersection of a context-free language (CFL) and a Petri net language (PNL) is empty. Our contribution to solve this long-standing problem which relates, for instance, to the reachability analysis of recursive programs over unbounded data domain, is to identify a class of CFLs called the finite-index CFLs for which the problem is decidable. The k-index approximation of a CFL can be obtained by discarding all the words that cannot be derived within a budget k on the number of occurrences of non-terminals. A finite-index CFL is thus a CFL which coincides with its k-index approximation for some k. We decide whether the intersection of a finite-index CFL and a PNL is empty by reducing it to the reachability problem of Petri nets with weak inhibitor arcs, a class of systems with infinitely many states for which reachability is known to be decidable. Conversely, we show that the reachability problem for a Petri net with weak inhibitor arcs reduces to the emptiness problem of a finite-index CFL intersected with a PNL.

Pattern-based verification checks the correctness of the program executions that follow a given pattern, a regular expression over the alphabet of program transitions of the form w1* ... wn*. For multithreaded programs, the alphabet of the pattern is given by the synchronization operations between threads. We study the complexity of pattern-based verification for abstracted multithreaded programs in which, as usual in program analysis, conditions have been replaced by nondeterminism (the technique works also for boolean programs). While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs, we show that pattern-based verification is NP-complete for both classes. We then conduct a multiparameter analysis in which we study the complexity in the number of threads, the number of procedures per thread, the size of the procedures, and the size of the pattern. We first show that no algorithm for pattern-based verification can be polynomial in the number of threads, procedures per thread, or the size of the pattern (unless P=NP). Then, using recent results about Parikh images of regular languages and semilinear sets, we present an algorithm exponential in the number of threads, procedures per thread, and size of the pattern, but polynomial in the size of the procedures.

Asynchronous or 'event-driven' programming is a popular technique to efficiently and flexibly manage concurrent interactions. In these programs, the programmer can post tasks that get stored in a task buffer and get executed atomically by a non-preemptive scheduler at a future point. We give a decision procedure for the fair termination property of asynchronous programs. The fair termination problem asks, given an asynchronous program and a fairness condition on its executions, does the program always terminate on fair executions? The fairness assumptions rule out certain undesired bad behaviors, such as where the scheduler ignores a set of posted tasks forever, or where a non-deterministic branch is always chosen in one direction. Since every liveness property reduces to a fair termination property, our decision procedure extends to liveness properties of asynchronous programs. Our decision procedure for the fair termination of asynchronous programs assumes all variables are finite-state. Even though variables are finite-state, asynchronous programs can have an unbounded stack from recursive calls made by tasks, as well as an unbounded task buffer of pending tasks. We show a reduction from the fair termination problem for asynchronous programs to fair termination problems on Petri Nets, and our main technical result is a reduction of the latter problem to Presburger satisfiability. Our decidability result is in contrast to multithreaded recursive programs, for which liveness properties are undecidable. While we focus on fair termination, we show our reduction to Petri Nets can be used to prove related properties such as fair nonstarvation (every posted task is eventually executed) and safety properties such as boundedness (find a bound on the maximum number of posted tasks that can be in the task buffer at any point).