Complexity of two-variable Dependence Logic and IF-Logic

Decidability of Definability

We show decidability of this problem for all structures Gamma that have a first-order definition in an ordered homogeneous structure Delta with a finite language whose age is a Ramsey class and determined by finitely many forbidden substructures. Examples for structures Gamma with this property are the order of the rationals, the random graph, the homogeneous universal poset, the random tournament, all homogeneous universal C-relations, and many more. We also obtain decidability of the problem when we replace primitive positive definability by existential positive, or existential definability. Our proof makes use of universal algebraic and model theoretic concepts, Ramsey theory, and a recent characterization of Ramsey classes in topological dynamics.

The Computational Meaning of Probabilistic Coherence Spaces

Computing Optimal Coverability Costs in Priced Timed Petri Nets

real-valued clock. Transition arcs are labeled with time intervals,

which specify constraints on the ages of tokens.

Our cost model assigns token storage costs per time unit to places,

and firing costs to transitions.

We study the cost to reach a given control-state.

In general, a cost-optimal run may not exist. However,

we show that the infimum of the costs is computable.

Listings and logics

Furthermore, we show that the existence of a listing of the L-subsets of TAUT is equivalent to the existence of an almost space optimal algorithm for TAUT. To obtain this result we have to derive a space version of a theorem of Levin on optimal inverters.

Noncomputable conditional distributions

Nevertheless, probabilistic inference has proven remarkably successful in practice, even in infinite-dimensional continuous settings. We prove several results giving general conditions under which conditional distributions are computable. In the discrete or dominated setting, under suitable computability hypotheses, conditional distributions are computable. Likewise, conditioning in abstract topological settings is a computable operation, in the presence of certain additional structure, such as independent absolutely continuous noise.

The Complexity of Verifying Ground Tree Rewrite Systems

with the ability to spawn new subthreads that

are hierarchically structured.

In this paper, we study the following problems over GTRS:

(1) model checking EF-logic, (2)

weak bisimilarity checking against finite systems, and (3) strong bisimilarity

checking against finite systems. Although they are all known to be decidable,

we show that problems (1) and (2) have nonelementary complexity, whereas

problem (3) is shown to be in $\coNEXP$ by finding a syntactic fragment of EF

whose model checking complexity is complete for $\P^\NEXP$.

The same problems are studied

over a more general but decidable extension of GTRS

called regular GTRS (RGTRS), where regular rewriting is allowed. Over RGTRS

we show that all three problems have nonelementary complexity.

We also apply our techniques to problems over PA-processes, a well-known class

of infinite systems in Mayr's PRS (Process Rewrite Systems) hierarchy. For

example,

strong bisimilarity checking of PA-processes against finite systems is shown

to be in

$\coNEXP$, yielding a first elementary upper bound for this problem.

Qualitative Tree Languages

First, we relaxe the notion of accepting run by allowing a negligible set (in the sense of measure theory) of non-accepting branches. In this qualitative setting, a tree is accepted by the automaton if there exists a run over this tree in which almost every branch is accepting. This leads to a new class of tree languages, qualitative tree languages. This class enjoys many good properties: closure under union and intersection (but not under complement), emptiness is decidable in polynomial time, strong relation with Markov decision process.

The second one, is by replacing the existential quantification — a tree is accepted if there exists some accepting run over the input tree — by a probabilistic quantification — a tree is accepted if almost every run over the input tree is accepting. For the run, we may use either classical acceptance or qualitative acceptance. In particular, for the latter, when equipped with a Büchi condition, we show that it leads to a class of probabilistic automata on infinite trees enjoying a decidable emptiness problem. To our knowledge, this is the first positive result for a class of probabilistic automaton over infinite trees.

A tetrachotomy for positive first-order logic without equality

of first-order logic over a fixed, finite structure D. This problem may be seen as a

natural generalisation of the quantified constraint satisfaction problem QCSP(D). We obtain

a tetrachotomy for arbitrary finite domains: each problem is either in L, is NP-complete,

is co-NP-complete or is Pspace-complete. Moreover, its complexity is characterised algebraically

in terms of the presence or absence of specific surjective hyper-endomorphisms; and, logically,

in terms of relativisation properties with respect to positive equality-free sentences.

We prove that the meta-problem, to establish for a specific D into which of the four

classes the related problem lies, is NP-hard.

Formalizing Randomized Matching Algorithms

Temporal Specifications with Accumulative Values

We introduce and investigate the extension of temporal logics with quantitative atomic assertions, aiming for a general and flexible framework for quantitative-oriented specifications.

In the heart of quantitative objectives lies the accumulation of values along a computation. It is either the accumulated summation, as with

the energy objectives, or the accumulated average, as with the mean-payoff objectives. We investigate the extension of temporal logics with the

{\em prefix-accumulation assertions\/} $\Sum(v) \geq c$ and $\Avg(v) \geq c$, where $v$ is a numeric variable of the system, $c$ is a constant

rational number, and $\Sum(v)$ and $\Avg(v)$ denote the accumulated sum and average of the values of $v$ from the beginning of the computation

up to the current point of time. We also allow the {\em path-accumulation assertions\/} $\LimInfAvg(v)\geq c$ and $\LimSupAvg(v)\geq c$,

referring to the average value along an entire computation.

We study the border of decidability for extensions of various temporal logics. In particular, we show that extending the fragment of CTL that has only the EX, EF, AX, and AG temporal modalities by prefix-accumulation assertions and extending LTL with path-accumulation assertions, result in temporal logics whose model-checking problem is decidable. The extended logics allow to significantly extend the currently known energy and mean-payoff objectives. Moreover, the prefix-accumulation assertions may be refined with ``controlled-accumulation'', allowing, for example, to specify constraints on the average waiting time between a request and a grant.

On the negative side, we show that the fragment we point to is, in a sense, the maximal logic whose extension with prefix-accumulation assertions permits a decidable model-checking procedure. Extending a temporal logic that has the EG or EU modalities, and in particular CTL and LTL, makes the problem undecidable.

Continuous Random Variables

domain, as an alternative to Jones and Plotkin's probabilistic

powerdomain. While no known Cartesian-closed category is stable

under the latter, we show that the so-called thin CRVs define a strong

monad on the Cartesian-closed category of bc-domains. The Jones and

Plotkin semantics of higher-order probabilistic programs occurs as a

form of extensional collapse of our new semantics in terms of thin

CRVs, preserving observational equivalence. We apply this to solve

a recent problem posed by M. Escard\'o [note: proof not complete as

of Tuesday, Jan 04, 13h; claim may be removed from final

submission]. Thin CRVs arose from the study of the second author's

(layered) Hoare indexed valuations, and we also make the connection

apparent.

Powermonads and Tensoring Unranked Effects

concepts such as monads or, essentially equivalently, (large)

Lawvere theories are a well-established tool for modelling generic

side-effects. An important issue in this context are combination

mechanisms for such algebraic effects, which allow for the modular

design of programming languages and verification logics. The most

basic combination operators are sum and tensor: while the sum of

effects is just their non-interacting union, the tensor imposes

commutation of effects. However, for effects with unbounded arity,

such as continuations or unbounded non-determinism, it is not a

priori clear whether these combinations actually exist in all

cases. Here, we introduce the class of uniform effects, which

includes unbounded non-determinism and continuations, and prove that

the tensor does always exist if one of the component effects is

uniform, thus in particular improving on previous results on

tensoring with continuations. We then treat the case of (unbounded)

non-determinism in more detail, and give an order-theoretic

characterization of effects for which tensoring with non-determinism

is conservative, thus enabling non-deterministic arguments for

deterministic programs such as a generic version of the

Fisher-Ladner encoding of control operators.

Concurrent strategies

polarities distinguish the moves of Player and Opponent. A total map of polarized event structures into $A$ can be understood as a pre-strategy in a game $A$---the map ensures that Player and Opponent respect the constraints of the game. Following Joyal, a pre-strategy from a game $A$ to a game $B$ is understood as a pre-strategy in a composite game got by setting the dual game of $A$, reversing the roles of Player and Opponent, in parallel with $B$. From this general scheme concurrent strategies---pre-strategies for which copy-cat strategies behaves as an identity w.r.t.~composition of pre-strategies---are characterized as those pre-strategies which satisfy the two conditions of receptivity and innocence. It is shown how (bi)categories of stable spans, certain profunctors, Berry's stable functions, and certain sequential algorithms arise as sub(bi)categories of concurrent games. It is indicated how the results can be adapted to other models such as asynchronous transition systems and Mazurkiewicz trace languages, which leads to a brief comparison with related work.

Languages of Dot-Depth One over Infinite Words

finite words, this class of languages corresponds to the Boolean

closure of Sigma1 of the first level of the quantifier alternation

hierarchy of first-order logic FO[<,+1,min,max]. We give a decidable

characterization of the Boolean closure of Sigma1[<,+1,min]

over infinite words; here, the max-predicate is void.

Our characterization is a combination of Knast's algebraic property

for dot-depth one and a topological condition. This yields decidability

of the problem whether a given regular omega-language has

dot-depth one.

Our approach considers finite and infinite words simultaneously. We

prove decidable characterizations for the Boolean closure of

Sigma1[<,+1,min] as well as for the Boolean closure of

Sigma1[<,+1,min,max] over finite and infinite words. In this

setting, the max-predicate can be used for distinguishing between

finite and infinite words. Hence, our result on infinite words can be

obtained as a corollary.

This paper is self-contained and we give full proofs. In particular,

a new combinatorial proof of Knast's Theorem concerning languages of

dot-depth one over finite words is included.

Ackermannian and Primitive-Recursive Bounds with Dickson's Lemma

We propose a new analysis of the length of bad sequences over (N^k,<=), improving on earlier results and providing upper bounds that are essentially tight. This analysis is complemented by a "user guide" explaining through practical examples how to easily derive complexity upper bounds from Dickson's Lemma.

The Ultimate Undecidability Result for the Halpern-Shoham Logic

This is surprising as this, apparently very simple, logic is decidable over dense orders and its reflexive variant is known to be decidable over discrete structures.

Our result subsumes a lot of previous negative results for the discrete case, like the undecidability for ABE, BD, ADB, AAbarD, and so on.

Game semantics for good general references

denotational model for RefML, a paradigmatic higher-order programming

language combining call-by-value evaluation and general references in

the style of ML. Our model is built using game semantics. In contrast

to the previous model by Abramsky, Honda and McCusker, it provides a

faithful account of reference types, and the full abstraction result

does not rely on the availability of spurious constructs of reference

type (bad variables). This is the first proper denotational model of

this kind, preceded only by the trace model recently proposed by Laird.

A type system for complexity flow analysis

To our knowledge, this is the first type system for an imperative language, which provides a complete characterization of polynomial time functions.

Computational Complexity of Quantum Satisfiability

We introduce the weak and strong satisfiability problem for quantum logic formulas; and show both NP-complete in dimension two as well.

For higher-dimensional spaces R^d and C^d with d>2 fixed, on the other hand, we show the problem to be complete for the nondeterministic Blum-Shub-Smale model of real computation.

This provides a unified view on both Turing and real BSS complexity theory;

and adds (a perhaps more natural and combinatorially flavoured) one to the still sparse list of NP_R-complete problems, mostly pertaining to real algebraic geometry.

Our proofs rely on (a careful examination of) works by John von Neumann as well as contributions by Hagge et.al (2005,2007,2009).

We finally investigate the problem over INdefinite finite dimensions and relate it to NONcommutative semialgebraic geometry.

Isomorphisms of types in the presence of higher-order references

First steps in synthetic guarded domain theory: step-indexing in the topos of trees

study the internal dependently-typed higher-order logic of S and show

that S models two modal operators, on predicates and types, which

serve as guards in recursive definitions of terms, predicates, and

types. In particular, we show how to solve recursive type equations

involving dependent types. We propose that the internal logic of S

provides the right setting for the synthetic construction of abstract

versions of step-indexed models of programming languages and program

logics. As an example, we show how to construct a model of a

programming language with higher-order store and recursive types

entirely inside the internal logic of S.

A decidable two-way logic on data words

Imperative Programs as Proofs via Game Semantics

What's decidable about Halpern and Shoham's interval logic? The maximal fragment ABBL

This paper is a contribution towards the complete classification of HS fragments. Different combinations of Allen's interval relations begins (B), meets (A), and later (L), and their inverses Abar, Bbar, and Lbar, have been considered in the literature.

We know from previous work that the combination ABBbarAbar is decidable over finite linear orders and undecidable everywhere else. We extend these results by showing that ABBbarLbar is decidable over the class of all (resp., dense, discrete) linear orders, and that it is maximal w.r.t decidability over these classes: adding any other interval modality immediately leads to undecidability.

Semantics of Higher-Order Quantum Computation via Geometry of Interaction

paradigm. While much of its current study employs low-level formalisms

such as quantum circuits, several high-level languages/calculi have

been recently proposed aiming at structured quantum programming. The

current work contributes to the semantical study of such high-level

quantum languages, by providing interaction-based semantics of a

functional quantum programming language---it is based on linear lambda

calculus and equipped with features like the $!$ modality and

recursion. We prove soundness and adequacy of our semantics. The

construction of our model is by a series of standard techniques taken

from the semantics of classical computation as well as from process

theory, namely: 1) monads with an order structure as models for

branching, used in the coalgebraic study of state-based systems; 2)

Girard's Geometry of Interaction, categorically formulated by

Abramsky, Haghverdi and Scott, providing interaction-based, game-like

semantics for linear logic and computation; and 3) the realizability

technique that turns an (untyped) combinatorial algebra into a

categorical model of a typed calculus. The mathematical genericity of

these techniques---mostly due to their categorical formulation---is

exploited for our move from classical to quantum.

Two Views on Multiple Mean Payoff Objectives in Markov Decision Processes

We consider two different objectives, namely, expectation and satisfaction

objectives.

Given an MDP with k reward functions, in the expectation objective the goal is to maximize the expected value, and in the satisfaction objective the goal is to maximize the probability of runs such that the limit-average value stays above a given vector.

We show that under the expectation objective, in contrast to the single-objective case, both randomization and memory are necessary for strategies, and we show that finite-memory randomized strategies are sufficient. We show that under the satisfaction objective, in contrast to the single-objective case, randomization is necessary for strategies, and we show that randomized memoryless strategies are sufficient for epsilon-approximation, for all epsilon>0. We show that the decision problems for both expectation and satisfaction objectives can be solved in polynomial time and the trade-off curve (Pareto curve) can be epsilon-approximated in time polynomial in the size of the MDP and 1/epsilon, and exponential in the number of reward functions, for all epsilon>0.

Our results also reveal flaws in an earlier paper ("Markov Decision Processes with multiple Long-Run Average Objectives", FSTTCS 2007) for MDPs with multiple mean-payoff functions under the expectation objective, correct the flaws and obtain improved results.

Linear Dependent Types and Relative Completeness

Separation Logic in the Presence of Garbage Collection

verification of heap-manipulating programs. However, it has been

applied almost exclusively in language settings where either memory is

managed manually or the issue of memory management is ignored

altogether. In this paper, we present a variant of separation logic,

GCSL, for reasoning about low-level programs that interface to a

garbage collector. In contrast to prior work by Calcagno et al., our

model of GCSL (1) permits reasoning about programs that use internal

pointers and address arithmetic, (2) supports logical variables that

range over pointers, and (3) straightforwardly validates the ``frame''

rule, as well as a standard interpretation of separation-logic

assertions. Essential to our approach is the technique (due

originally to McCreight et al.) of distinguishing between ``logical''

and ``physical'' states, which enables us to insulate the logic from

the physical reality that pointer ``values'' may be moved and/or

deallocated by the garbage collector.

Forcing as a program transformation

Ultrametric Semantics of Reactive Programs

programming using ultrametric spaces and nonexpansive maps, which

provides a natural Cartesian closed generalization of causal stream

functions and guarded recursive definitions. We define a type theory

corresponding to this semantics and show that it satisfies

normalization. Finally, we show how reactive programs written in this

language may be implemented efficiently using an imperatively updated

dataflow graph and give a higher-order separation logic proof that

this low-level implementation is correct with respect to the

high-level semantics.

Automata with group actions

The Dichotomy for Conservative Constraint Satisfaction Problems Revisited

One of the main achievements in this direction is a result of Bulatov (LICS'03) confirming the dichotomy conjecture for conservative CSPs, that is, CSPs over constraint languages containing all unary relations.

Unfortunately, the proof is very long and complicated, and therefore hard to understand even for a specialist.

This paper provides a short and transparent proof.

Proof nets for additive linear logic with units

This paper provides canonical, graphical representations of the categorical morphisms, yielding a novel solution to this decision problem. Starting with (a modification of) existing proof nets, due to Hughes and Van Glabbeek, for additive linear logic without units, canonical forms are obtained by graph rewriting. The rewriting algorithm is remarkably simple. As a decision procedure for term equality it matches the known complexity of the problem. A main technical contribution of the paper is the substantial correctness proof of the algorithm.

COQ MTU : a higher-order type theory with a predicative hierachy of universes parameterized by a decidable first-order theory

Regular Repair of Specifications

Rigorous Approximated Determinization of Weighted Automata

input word to a numerical value. Applications of weighted

automata include formal verification of quantitative properties, as

well as text, speech, and image processing. Many of these applications

require the WFAs to be deterministic, or work substantially better

when the WFAs are deterministic. Unlike NFAs, which can always be

determinized, not all WFAs have an equivalent deterministic weighted

automaton (DWFA). In \cite{Moh97}, Mohri describes a determinization

construction for a subclass of WFA. He also describes a property of

WFAs (the {\em twins property}), such that all WFA that satisfy the

twins property are determinizable and the algorithm terminates on them.

Unfortunately, many natural WFA do not satisfy the twins property and

cannot be determinized using Mohri's algorithm.

In this paper we study {\em approximated determinization\/} of WFAs.

We describe an algorithm that, given a WFA $\A$ and an

approximation factor $t > 1$, constructs a DWFA $\A'$ that {\em $t$-

determinizes\/} $\A$. Formally, for all words $w \in \Sigma^*$, the

value of $w$ in $\A'$ is at least its value in $\A$ and at most $t$

times its value in $\A$. Our construction involves two new ideas:

attributing states in the subset construction by both upper and lower

residues, and collapsing attributed subsets whose residues can be

tightened.

The larger the approximation factor is, the more attributed subsets we

can collapse. Thus, $t$-determinization is helpful not only for WFAs that

cannot be determinized, but also in cases determinization is possible

but results in automata that are too big to handle. In addition,

$t$-determinization is useful for reasoning about the competitive

ratio of online algorithms. We also describe a property (the {\em $t$-twins property}) and use it in order to characterize $t$-determinizable WFAs.

Finally, we describe a polynomial algorithm for deciding whether a

given WFA has the $t$-twins property.