# ICALP 2011 Accepted Papers with Abstracts for Track B: Logic, Semantics, Automata  and Theory of Programming

Christos Kapoutsis. Nondeterminism is Essential in Small 2FAs with Few Reversals
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.
Probabilistic Bisimulation and Simulation Algorithms by Abstract Interpretation
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.
Stefan Kiefer, Andrzej Murawski, Joel Ouaknine, James Worrell and Lijun Zhang. On Stabilization in Herman's Algorithm
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.
Kohei Suenaga and Ichiro Hasuo. Programming with Infinitesimals: A While-Language for Hybrid System Modeling
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.
Tomas Brazdil, Stefan Kiefer, Antonin Kucera and Ivana Hutarova Varekova. Runtime Analysis of Probabilistic Programs with Unbounded Recursion
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.
Simone Bova, Hubie Chen and Matt Valeriote. Generic Expression Hardness Results for Primitive Positive Formula Comparison
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.
Isomorphism of regular trees and words
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.
Martin Delacourt. Rice's theorem for mu-limit sets of cellular automata
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.
A Fragment of ML Decidable by Visibly Pushdown Automata
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) log- ical 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.
Regular Languages of Words Over Countable Linear Orderings
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.
Guarded negation
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.
Matthew Anderson, Dieter Van Melkebeek, Nicole Schweikardt and Luc Segoufin. Locality of queries definable in invariant first-order logic  with arbitrary built-in predicates
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.
Relating Computational Effects by TT-Lifting
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.
Constructing differential categories and deconstructing categories of games
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.
Modular Markovian Logic
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.
On the capabilities of grammars, automata, and transducers controlled by monoids
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
Emptiness and Universality Problems in Timed Automata with Positive Frequency
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.
Automata-based CSL model checking
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.
Michael Benedikt, Gabriele Puppis and Cristian Riveros. The cost of traveling between languages
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.
Liveness-preserving atomicity abstraction
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.
Thomas Brihaye, Laurent Doyen, Gilles Geeraerts, Joël Ouaknine, Jean-François Raskin and James Worrell. On Reachability for Hybrid Automata over Bounded Time
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.
Multiply-Recursive Upper Bounds with Higman’s Lemma
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.
Buechi Automata can have Smaller Quotients
Abstract: We study novel simulation-like preorders for quotienting nondeterministic Buechi automata. We deﬁne ﬁxed-word delayed simulation, a new preorder coarser than delayed simulation. We argue that ﬁxed-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 ﬁxed-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 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
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.
Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes
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.
Ahmed Bouajjani, Roland Meyer and Eike Moehlmann. Deciding robustness against total store ordering
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.
Diana Fischer and Lukasz Kaiser. Model Checking the Quantitative mu-Calculus on Linear Hybrid 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.
Tomas Brazdil, Vaclav Brozek, Kousha Etessami and Antonin Kucera. Approximating the termination value of One-counter MDPs and Stochastic Games
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.
Franck Van Breugel and Xin Zhang. A Progress Measure for Explicit-State Probabilistic Model-Checkers
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 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