Abstract: The languages of infinite timed words accepted by timed automata are traditionally defined using Büchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting states. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.

Abstract: During the last decades, classical models in language theory have been extended by control mechanisms defined by monoids.  We study which monoids cause the extensions of context-free grammars, finite automata, or finite state transducers to exceed the capacity of the original model.  Furthermore, we investigate when, in the extended automata model, the nondeterministic variant differs from the deterministic one in capacity.  We show that all these conditions are in fact equivalent and present an algebraic characterization. In particular, the open question of whether every language generated by a valence grammar over a finite monoid is context-free is provided with a positive answer.

Abstract: One-counter MDPs (OC-MDPs) and one-counter simple stochastic games (OC-SSGs) are 1-player, and 2-player turn-based zero-sum, stochastic games played on the transition graph of classic one-counter automata (equivalently, pushdown automata with a 1-letter stack alphabet). A key objective for the analysis and verification of these games is the {\em termination} objective, where  the players aim  to maximize (minimize, respectively) the probability of hitting counter value $0$, starting at a given control state and given counter value. Recently \cite{BBEKW10,BBE10}, we studied {\em qualitative} decision problems (``is the optimal termination value  = 1?'')  for OC-MDPs (and OC-SSGs) and showed them to be decidable in P-time (in NP$\cap$coNP, respectively). However, {\em quantitative} decision and approximation problems (``is the optimal termination value $\geq p$'', or ``approximate the termination value within $\epsilon$'') are far more challenging.  This is so in part because  optimal strategies may not exist, and even when they do exist they can have a highly non-trivial structure. It thus remained open even whether any of these quantitative termination problems are computable. In this paper we show that all quantitative {\em approximation} problems for the termination value for OC-MDPs and OC-SSGs are computable.  Specifically, given a OC-SSG, and given $\epsilon > 0$, we can compute a value $v$ that approximates the value of the OC-SSG termination game within additive error $\epsilon$, and furthermore we can compute $\epsilon$-optimal strategies for both players in the game. A key ingredient in our proofs is a subtle   martingale, derived from solving certain LPs that we can associate with a maximizing OC-MDP. An application of Azuma's inequality on these martingales yields a computable bound for the ``wealth'' at which a ``rich person's strategy'' becomes $\epsilon$-optimal for OC-MDPs.

Abstract: This paper investigates the time-bounded version of the reachability problem for hybrid automata. This problem asks whether a given hybrid automaton can reach a given target location within B time units, where B is a given bound. We prove that, unlike the classical reachability problem, the timed-bounded version is decidable on rectangular hybrid automata if only nonnegative rates are allowed. This class is of practical interest as it subsumes for example the class of stopwatch automata. We also show that the problem becomes undecidable if either diagonal constraints or both negative and positive rates are allowed.

Abstract: We add, to the common combination of a WHILE-language and a Hoare-style program logic, a constant dt that represents an infinitesimal (i.e. infinitely small) value. The outcome is a framework for modeling and verification of hybrid systems: hybrid systems exhibit both continuous and discrete dynamics and getting them right is a pressing challenge. We rigorously define the semantics of programs in the language of nonstandard analysis, on the basis of which the program logic is shown to be sound and relatively complete.

Abstract:              Verification of the source code of a probabilistic system by means of an explicit-state model-checker is challenging. In most cases, the probabilistic model-checker will run out of memory due to the infamous state space explosion problem. We introduce the notion of a progress measure for such a model-checker. The progress measure returns a number in the interval [0, 1]. This number captures the amount of progress the model-checker has made towards verifying a particular linear-time property. The larger the number, the more progress the model-checker has made. We prove that the progress measure provides a lowerbound of the measure of the set of execution paths that satisfy the property. We also show how to compute the progress measure for checking a particular class of linear-time properties, namely invariants. Keywords: probabilistic model-checking, progress measure, line

Abstract: On every n-long input, every two-way finite automaton (2FA) can reverse its head O(n) times before halting. A "2FA with few reversals" is an automaton where this number is only o(n). For every h, we exhibit a language that requires Ω(2^h) states on every deterministic 2FA with few reversals, but only h states on a nondeterministic 2FA with few reversals.

Abstract: We study novel simulation-like preorders for quotienting nondeterministic Buechi automata. We define fixed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that fixed-word simulation is the coarsest forward simulation-like preorder which can be used for quotienting Buechi automata, thus improving our understanding of the limits of quotienting. Also, we show that computing fixed-word simulation is PSPACE-complete. On the practical side, we introduce proxy simulations, which are novel polynomial-time computable preorders sound for quotienting. In particular, delayed proxy simulation induce quotients that can be smaller by an arbitrarily large factor than direct backward simulation. We derive proxy simulations as the product of a theory of refinement transformers: A refinement transformer maps preorders non-decreasingly, preserving certain properties. We study under which general conditions refinement transformers are sound for quotienting.

Abstract: We consider restrictions of first-order logic and of fixpoint logic in which all occurrences of negation are required to be guarded by an atomic predicate.   In terms of expressive power, the logics in question, called GNFO and GNFP, extend the guarded fragment of first-order logic and guarded least fixpoint logic, respectively. They also extend the recently introduced unary negation fragments of first-order logic and of least fixpoint logic. We show that the satisfiability problem for GNFO and for GNFP is 2ExpTime-complete, both on arbitrary structures and on finite structures. We also study the complexity of the associated model checking problems. Finally, we show that GNFO and GNFP are not only computationally well behaved, but also model theoretically: we show that GNFO and GNFP have the tree-like model property and that GNFO has the finite model property, and we characterize the expressive power of GNFO in terms of invariance for an appropriate notion of bisimulation.

Abstract: We introduce Modular Markovian Logic (MML) for compositional continuous-time and continuous-space Markov processes. MML combines operators specific to stochastic logics with operators that reflect the modular structure of the semantics, similar to those used by spatial and separation logics.We present a complete Hilbert-style axiomatization for MML, prove the small model property and analyze the relation between the stochastic bisimulation and the logical equivalence relation induced by MML on models.

Abstract: We study the expression complexity of two basic problems involving the comparison of primitive positive formulas: equivalence and containment. We give two generic hardness results for the studied problems, and discuss evidence that they are optimal and yield, for each of the problems, a complexity trichotomy.

Abstract:   We propose a new approach to analysing higher-order recursive   schemes.  Many results in the literature use automata models   generalising pushdown automata, most notably higher-order pushdown   automata with collapse (CPDA). Instead, we propose to use the   Krivine machine model. Compared to CPDA, this model is closer to   lambda-calculus, and incorporates nicely many invariants of   computations, as for example the typing information. The usefulness   of the proposed approach is demonstrated with new proofs of two   central results in the field: the decidability of the local and   global model checking problems for higher-order schemes with respect   to the mu-calculus.

Abstract: Cellular automata are a parallel and synchronous computing model, made of infinitely many finite automata updating according to the same local rule. Rice's theorem states that any nontrivial property over computable functions is undecidable. It has been adapted by Kari to limit sets of cellular automata, that is the set of configurations that can be reached arbitrarily late. This paper proves a new Rice theorem for $\mu$-limit sets, which are sets of configurations often reached arbitrarily late.

Abstract: We show how to calculate the number of edits per character needed to convert a string in one regular language to a string in another language. Our algorithm makes use of a local determinization procedure  applicable to a subclass of distance automata. We then show how to  calculate the same property when the editing needs to be done in streaming fashion, by a finite state transducer, using a reduction to mean-payoff games. Finally, we determine when the optimal editor can be approximated by a streaming editor -- the construction here makes use of a combination of games and distance automata.

Abstract: We consider first-order formulas over relational structures which, in addition to the symbols in the relational schema, may use a binary relation interpreted as a linear order over the elements of the structures, and arbitrary numerical predicates (including addition and multiplication) interpreted over that linear order. We require that for each fixed interpretation of the initial relational schema, the validity of the formula is independent of the particular interpretation of the linear order and its associated numerical predicates. We refer to such formulas as Arb-invariant first-order.                                        Our main result shows a Gaifman locality theorem: two tuples of a structure with n elements, having the same neighborhood up to distance (\log n)^{\omega(1)}, cannot be distinguished by Arb-invariant first-order formulas. When restricting attention to word structures, we can achieve the same quantitative strength for Hanf locality: Arb-invariant first-order formulas cannot distinguish between two words having the same neighborhoods up to distance (\log n)^{\omega(1)}.  In both cases we show that our bounds are tight.                                     Our proof exploits the close connection between Arb-invariant first-order formulas and the complexity class AC^0, and hinges on the tight lower bounds for parity on constant-depth circuits.

Abstract: The computational complexity of the isomorphism problem for regular trees, regular linear orders, and regular words is analyzed. A tree is regular if it is isomorphic to the prefix order on a regular language. In case regular languages are represented by NFAs (DFAs), the isomorphism problem for regular trees turns out to be EXPTIME-complete (resp. P-complete). In case the input automata are acyclic NFAs (acyclic DFAs), the corresponding trees are (succinctly represented) finite trees, and the isomorphism problem turns out to be PSPACE-complete (resp. P-complete). A linear order is regular if it is isomorphic to the lexicographic order on a regular language. A polynomial time algorithm for the isomorphism problem for regular linear orders (and even regular words, which generalize the latter) given by DFAs is presented. This solves an open problem by Esik and Bloom.

Abstract: Sequential consistency (sc) is the classical model for shared memory concurrent programs. It corresponds to the interleaving semantics where the order of actions issued by a component is preserved. For performance reasons, modern processors adopt relaxed memory models that may execute actions out of order. We address the issue of deciding robustness of a program against the popular total store ordering (tso) memory model, i.e., we check whether the behaviour under tso coincides with the expected sc semantics. We prove that this problem is decidable and only PSPACE-complete. Surprisingly, we detect violations to robustness on pairs of sc computations, without consulting the tso model.

Abstract: We develop an algebraic model suitable for recognizing languages of words indexed by countable linear orderings. We prove that this notion of recognizability is effectively equivalent to definability in monadic second-order (MSO) logic. This reproves in particular the decidability of MSO logic over the rationals with order. Our proof also implies the first known collapse result for MSO logic over countable linear orderings.

Abstract:   Markov automata describe systems in terms of events which may be   nondeterministic, may occur probabilistically, or may be subject to   time delays. We define a novel notion of weak bisimulation for such   systems and prove that this provides both a sound and complete proof   methodology for a natural extensional behavioural equivalence   between such systems, a generalisation of reduction barbed   congruence, the well-known touchstone equivalence for a large   variety of process description languages.

Abstract: Modern concurrent algorithms are usually encapsulated in libraries, and complex algorithms are often constructed using libraries of simpler ones. We present the first theorem that allows harnessing this structure to give compositional liveness proofs to concurrent algorithms and their clients. We show that, while proving a liveness property of a client using a concurrent library, we can soundly replace the library by another one related to the original library by a generalisation of a well-known notion of linearizability. We apply this result to show formally that lock-freedom, an often-used liveness property of non-blocking algorithms, is compositional for linearizable libraries, and provide an example illustrating our proof technique.

Abstract: For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996. The presented decision procedure, however, has exponential complexity. In this paper, we propose an effective approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect  to the CSL property to be checked. We present a measure-preservation theorem allowing us to reduce the problem to a transient analysis on stratified CTMCs. The corresponding probability can then be approximated in polynomial time (using uniformization). This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preservation theorem can be used to ensure the decidability for general CTMCs.

Abstract: We develop a new analysis for the length of controlled bad sequences in well-quasi-orderings based on Higman's Lemma. This leads to tight multiply-recursive upper bounds that readily apply to several verification algorithms for well-structured systems.

Abstract: In this work, we consider the model-checking problem for a quantitative extension of the modal mu-calculus on a class of hybrid systems. Qualitative model checking has been proved decidable and implemented for several classes of systems, but this is not the case for quantitative questions, which arise naturally in this context. Recently, quantitative formalisms that subsume classical temporal logics and additionally allow to measure interesting quantitative phenomena were introduced. We show how a powerful quantitative logic, the quantitative mu-calculus, can be model-checked with arbitrary precision on initialised linear hybrid systems. To this end, we develop new techniques for the discretisation of continuous state spaces based on a special class of strategies in model-checking games and show decidability of a class of counter-reset games that may be of independent interest.

Abstract: We study the runtime in probabilistic programs with unbounded recursion. As underlying formal model for such programs we use probabilistic pushdown automata (pPDA) which exactly correspond to recursive Markov chains. We show that every pPDA can be transformed into a stateless pPDA (called ``pBPA'') whose runtime and further properties are closely related to those of the original pPDA. This result substantially simplifies the analysis of runtime and other pPDA properties. We prove that for every pPDA the probability of performing a long run decreases exponentially in the length of the run, if and only if the expected runtime in the pPDA is finite. If the expectation is infinite, then the probability decreases ``polynomially''. We show that these bounds are asymptotically tight. Our tail bounds on the runtime are generic, i.e., applicable to any probabilistic program with unbounded recursion. An intuitive interpretation is that in pPDA the runtime is exponentially unlikely to deviate from its expected value.

Abstract: We consider the problem of establishing a relationship between two monadic semantics of the lambda_c-calculus extended with algebraic operations. We show that two monadic semantics of any program are related if the relation includes value relations and is closed under the algebraic operations in the lambda_c-calculus.

Abstract: We present an abstract construction for building differential categories useful to model resource sensitive calculi,  and we apply it to categories of games. In one instance, we recover a category previously used to give a fully abstract model of a nondeterministic imperative language. The construction exposes the differential structure already present in this model. A second instance corresponds to a new Cartesian differential  category of games. We give a model of a Resource PCF in this category and show that it enjoys the finite definability property. Comparison with a relational semantics reveals that the latter also possesses this property and is fully abstract.

Abstract: We show how probabilistic bisimulation equivalence and simulation preorder, namely the main behavioural relations on probabilistic nondeterministic processes, can be characterized by abstract interpretation. Indeed, both bisimulation and simulation can be obtained as domain completions of partitions and preorders, viewed as abstractions, w.r.t. a pair of concrete functions that encode a probabilistic LTS. As a consequence, this approach provides a general framework for designing algorithms for computing probabilistic bisimulation and simulation. Notably, (i) we show that the standard probabilistic bisimulation algorithm by Baier et al. can be viewed as an instance of such a framework and (ii) we design a new efficient probabilistic simulation algorithm that improves the state of the art.

Abstract: The simply-typed, call-by-value language, RML, may be viewed as a canonical restriction of Standard ML to ground-type references, augmented by a "bad variable" construct in the sense of Reynolds. By a short type, we mean a type of order at most 2 and arity at most 1. We consider the fragment of (finitary) RML, RML_OStr, consisting of terms-in-context such that (i) the term has a short type, and (ii) every argument type of the type of each free variable is short. RML_OStr is surprisingly expressive; it includes several instances of (in)equivalence in the literature that are challenging to prove using methods based on (state-based) logical relations. We show that it is decidable whether a given pair of RML_OStr terms-in-context is observationally equivalent. Using the fully abstract game semantics of RML, our algorithm reduces the problem to the language equivalence of visibly pushdown automata. When restricted to terms in canonical form, the problem is EXPTIME-complete.

Abstract: Herman's algorithm is a synchronous randomized protocol for achieving self-stabilization in a token ring consisting of N processes. The interaction of tokens makes the dynamics of the protocol very difficult to analyze. In this paper we study the expected time to stabilization in terms of the initial configuration. It is straightforward that the algorithm achieves stabilization almost surely from any initial configuration, and it is known that the worst-case expected time to stabilization (with respect to the initial configuration) is Theta(N^2). Our first contribution is to give an upper bound of 0.64 N^2 on the expected stabilization time, improving on previous upper bounds and reducing the gap with the best existing lower bound.  We also introduce an asynchronous version of the protocol, showing a similar O(N^2) convergence bound in this case. Assuming that errors arise from the corruption of some number k of bits, where k is fixed independently of the size of the ring, we show that the expected time to stabilization is O(N). This reveals a hitherto unknown and highly desirable property of Herman's algorithm: it recovers quickly from bounded errors. We also show that if the initial configuration arises by resetting each bit independently and uniformly at random, then stabilization is significantly faster than in the worst case.