Abstract In a seminal work, Gibbons and Korach [9] studied the complexity of deciding whether an observed sequence of reads and writes of a multi-threaded program admits a sequentially consistent interleaving. They showed the problem to be $$\textsf{NP}$$ NP -hard even under strong syntactic restrictions. More recently, Chakraborty et al. [6] considered the problem for weak memory models and proved that $$\textsf{NP}$$ NP -hardness remains even when the number of threads, the number of memory locations, and the value domain are all bounded. In this paper we revisit the problem for the release-acquire variants of the C11 memory model. Our main positive result is that consistency testing can be done in polynomial-time when each memory location is written by at most one thread (multiple readers are allowed). Notably, this restriction is already $$\textsf{NP}$$ NP -hard for the model of sequential consistency. We complement our upper bound with tight hardness results: we show the problem to be $$\textsf{NP}$$ NP -hard when two threads may write to the same location; furthermore, allowing three writers per location rules out $$2^{o(k)}\cdot n^{\mathcal {O}(1)}$$ 2 o ( k ) · n O ( 1 ) algorithms under the Exponential Time Hypothesis, where k denotes the number of threads, and n the number of memory operations.

Abstract We study the problem of synthesizing programs from non-linear real arithmetic () specifications. Existing techniques, such as syntax-guided synthesis (), fail to synthesize programs when the specification is unrealizable . We argue this is unsatisfactory in many situations, and aim to synthesize programs from arbitrary specifications, such that for any input, the synthesized program either produces outputs satisfying the specification or reports non-existence of any such output. To avoid rounding errors inherent in floating-point arithmetic, we restrict our programs to work on rational inputs and outputs. We first show that our variant of the synthesis problem is as hard as a long-standing open problem in number theory, and that synthesizing loop-free programs from arbitrary NRA specifications with rational inputs and outputs is impossible in general. Second, we present a sound and complete synthesis algorithm for the case where the specification involves a single output variable. We also show that for realizable specifications, a program generated by for (real inputs and outputs) serves as a solution to our problem, where inputs and outputs are rationals. Third, we provide a sound (but necessarily incomplete) synthesis algorithm for the general case of specifications. We have implemented our approach in a prototype tool called that solves many benchmarks beyond the reach of state-of-the-art SyGuS tools, even when we render the specifications realizable.

The translation of Metric Interval Temporal Logic (MITL) to timed automata is a topic that has been extensively studied. A key challenge here is the conversion of future modalities into equivalent automata. Typical conversions equip the automata with a guess-and-check mechanism to ascertain the truth of future modalities. Guess-and-check can be naturally implemented via alternation. However, since timed automata tools do not handle alternation, existing methods perform an additional step of converting the alternating timed automata into timed automata. This de-alternation step proceeds by an intricate finite abstraction of the space of configurations of the alternating automaton. Recently, a model of generalized timed automata (GTA) has been proposed. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. We provide a new concise translation from MITL to GTA. In particular, for the timed until modality, our translation offers an exponential improvement w.r.t. the state-of-the-art. Thanks to this conversion, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. Due to the presence of future clocks, there is no finite time-abstract bisimulation (region equivalence) for GTAs, whereas liveness algorithms for timed automata crucially rely on the presence of the finite region equivalence. As our second contribution, we provide a new zone-based algorithm for checking Buchi non-emptiness in GTAs, which circumvents this fundamental challenge.

Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to reactive synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. An important result by Dartois et al. shows that composition of two-way transducers enjoy a polynomial composition when the underlying transducer is reversible, that is, if they are both deterministic and co-deterministic. This is a major improvement over general deterministic two-way transducers, for which composition causes a doubly exponential blow-up in the size of the inputs in general. Moreover, they show that reversible two-way transducers have the same expressiveness as deterministic two-way transducers. However, the question of expressiveness of reversible transducers over infinite words is still open. In this article, we introduce the class of reversible two-way transducers over infinite words and show that they enjoy the same expressive power as deterministic two-way transducers over infinite words. This is done through a non-trivial, effective construction inducing a single exponential blow-up in the set of states. Further, we also prove that composing two reversible two-way transducers over infinite words incurs only a polynomial complexity, thereby providing foundations for efficient procedure for composition of transducers over infinite words.

Abstract Quantifier Elimination (QE) concerns finding a quantifier-free formula that is semantically equivalent to a quantified formula in a given logic. For the theory of non-linear arithmetic over reals (NRA), QE is known to be computationally challenging. In this paper, we show how QE over NRA can be solved approximately and efficiently in practice using a Boolean combination of constraints in the linear arithmetic over reals (LRA). Our approach works by approximating the solution space of a set of NRA constraints when all real variables are bounded. It combines adaptive dynamic gridding with application of Handelman’s Theorem to obtain the approximation efficiently via a sequence of linear programs (LP). We provide rigorous approximation guarantees, and also proofs of soundness and completeness (under mild assumptions) of our algorithm. Interestingly, our work allows us to bootstrap on earlier work (viz. [38]) and solve quantified SMT problems over a combination of NRA and other theories, that are beyond the reach of state-of-the-art solvers. We have implemented our approach in a preprocessor for Z3 called POQER. Our experiments show that POQER+Z3EG outperforms state-of-the-art SMT solvers on non-trivial problems, adapted from a suite of benchmarks.

In this work, we consider two sets I and O of bounded integer variables, modeling the inputs and outputs of a program. Given a specification Post, which is a Boolean combination of linear or polynomial inequalities with real coefficients over I ∪ O, our goal is to synthesize the weakest possible pre-condition Pre and a program P satisfying the Hoare triple {Pre}P{Post}. We provide a novel, practical, sound and complete algorithm, inspired by Farkas’ Lemma and Handelman’s Theorem, that synthesizes both the program P and the pre-condition Pre over a bounded integral region. Our approach is exact and guaranteed to find the weakest pre-condition. Moreover, it always synthesizes both P and Pre as linear decision lists. Thus, our output consists of simple programs and pre- conditions that facilitate further static analysis. We also provide experimental results over benchmarks showcasing the real-world applicability of our approach and considerable performance gains over the state-of-the-art.1

Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness. In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the G-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata.

Abstract In this paper, we consider a model of generalized timed automata (GTA) with two kinds of clocks, history and future, that can express many timed features succinctly, including timed automata, event-clock automata with and without diagonal constraints, and automata with timers. Our main contribution is a new simulation-based zone algorithm for checking reachability in this unified model. While such algorithms are known to exist for timed automata, and have recently been shown for event-clock automata without diagonal constraints, this is the first result that can handle event-clock automata with diagonal constraints and automata with timers. We also provide a prototype implementation for our model and show experimental results on several benchmarks. To the best of our knowledge, this is the first effective implementation not just for our unified model, but even just for automata with timers or for event-clock automata (with predicting clocks) without going through a costly translation via timed automata. Last but not least, beyond being interesting in their own right, generalized timed automata can be used for model-checking event-clock specifications over timed automata models.

Event-clock automata are a well-known subclass of timed automata which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for event-clock automata. A main reason for this is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied in [Gilles Geeraerts et al., 2011; Gilles Geeraerts et al., 2014], where the authors also proposed a solution using zone extrapolations. In this paper, we propose an alternative zone-based algorithm, using simulations for finiteness, to solve the reachability problem for event-clock automata. Our algorithm exploits the 𝒢-simulation framework, which is the coarsest known simulation relation for reachability, and has been recently used for advances in other extensions of timed automata.

A timed network is a parallel composition of timed automata synchronizing on common actions. We develop a methodology that allows to use partial-order methods when solving the reachability problem for timed networks. It is based on a local-time semantics proposed by [Bengtsson et al. 1998]. A new simulation based abstraction of local-time zones is proposed. The main technical contribution is an efficient algorithm for testing subsumption between local-time zones with respect to this abstraction operator. The abstraction is not finite for all networks. It turns out that, under relatively mild conditions, there is no finite abstraction for local-time zones that works for arbitrary timed networks. To circumvent this problem, we introduce a notion of a bounded-spread network. The spread of a network is a parameter that says how far the local times of individual processes need to diverge. For bounded-spread networks, we show that it is possible to use subsumption and partial-order methods at the same time.

The class of regular transformations has several equivalent characterizations such as functional MSO transductions, deterministic two-way transducers, streaming string transducers, as well as regular transducer expressions (RTE).

We present first-order (FO) and monadic second-order (MSO) logics with predicates ‘between’ and ‘neighbour’ that characterise the class of regular languages that are closed under the reverse operation and its subclasses. The ternary between predicate bet(x, y, z) is true if the position y is strictly between the positions x and z. The binary neighbour predicate N(x, y) is true when the the positions x and y are adjacent. It is shown that the class of reversible regular languages is precisely the class definable in the logics MSO(bet) and MSO(N). Moreover the class is definable by their existential fragments EMSO(bet) and EMSO(N), yielding a normal form for MSO formulas. In the first-order case, the logic FO(bet) corresponds precisely to the class of reversible languages definable in FO(<). Every formula in FO(bet) is equivalent to one that uses at most 3 variables. However the logic FO(N) defines only a strict subset of reversible languages definable in FO(+1). A language-theoretic characterisation of the class of languages definable in FO(N), called locally-reversible threshold-testable (LRTT), is given. In the second part of the paper we show that the standard connections that exist between MSO and FO logics with order and successor predicates and varieties of finite semigroups extend to the new setting with the semigroups extended with an involution operation on its elements. The case is different for FO(N) where we show that one needs an additional equation that uses the involution operator to characterise the class. While the general problem of characterising FO(N) is open, an equational characterisation is shown for the case of neutral letter languages.

We investigate a zone based approach for the reachability problem in timed automata. The challenge is to alleviate the size explosion of the search space when considering networks of timed automata working in parallel. In the timed setting this explosion is particularly visible as even different interleavings of local actions of processes may lead to different zones. Salah et al. in 2006 have shown that the union of all these different zones is also a zone. This observation was used in an algorithm which from time to time detects and aggregates these zones into a single zone. We show that such aggregated zones can be calculated more efficiently using the local time semantics and the related notion of local zones proposed by Bengtsson et al. in 1998. Next, we point out a flaw in the existing method to ensure termination of the local zone graph computation. We fix this with a new algorithm that builds the local zone graph and uses abstraction techniques over (standard) zones for termination. We evaluate our algorithm on standard examples. On various examples, we observe an order of magnitude decrease in the search space. On the other examples, the algorithm performs like the standard zone algorithm.