Nondeterminism is Essential in Small 2FAs with Few Reversals

Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation

On Stabilization in Herman's Algorithm

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.

Programming with Infinitesimals: A While-Language for Hybrid System Modeling

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.

Runtime Analysis of Probabilistic Programs with Unbounded Recursion

Generic Expression Hardness Results for Primitive Positive Formula Comparison

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.

Isomorphism of regular trees and words

Rice's theorem for mu-limit sets of cellular automata

A Fragment of ML Decidable by Visibly Pushdown Automata

Regular Languages of Words Over Countable Linear Orderings

Guarded negation

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.

Locality of queries definable in invariant first-order logic with arbitrary built-in predicates

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.

Relating Computational Effects by TT-Lifting

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.

Constructing differential categories and deconstructing categories of games

Modular Markovian Logic

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.

On the capabilities of grammars, automata, and transducers controlled by monoids

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.

Emptiness and Universality Problems in Timed Automata with Positive Frequency

Automata-based CSL model checking

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.

The cost of traveling between languages

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.

Liveness-preserving atomicity abstraction

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.

On Reachability for Hybrid Automata over Bounded Time

Multiply-Recursive Upper Bounds with Higman’s Lemma

Buechi Automata can have Smaller Quotients

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 reﬁnement transformers: A reﬁnement transformer maps preorders non-decreasingly, preserving certain properties. We study under which general conditions reﬁnement transformers are sound for quotienting.

On the Semantics of Markov Automata

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.

Krivine machines and higher-order schemes

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.

Deciding robustness against total store ordering

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.

Model Checking the Quantitative mu-Calculus on Linear Hybrid Systems

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.

Approximating the termination value of One-counter MDPs and Stochastic Games

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.

A Progress Measure for Explicit-State Probabilistic Model-Checkers

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 num-

ber 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