CSL-LICS 2014 FULL AND FINAL PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. Energy games are a well-studied class of 2-player turn based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this.

We consider a generalization of energy games by replacing the finite game graph with an infinite game graph derived from a pushdown automaton (modelling recursion) or its subclass of a one-counter machine.

Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter machine and the energy is one-dimensional. On the other hand, every generalized energy game is undecidable: Energy games on one-counter machines with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional.

Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems.

ABSTRACT. Slot and van Emde Boas' invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is lambda-calculus a reasonable machine? Is there a way to measure the computational complexity of a lambda-term? This paper presents the first complete positive answer to this long-standing problem. Moreover, our answer is completely machine-independent and based over a standard notion in the theory of lambda-calculus: the length of a leftmost-outermost derivation to normal form is an invariant cost model. Such a theorem cannot be proved by directly relating lambda-calculus with Turing machines or random access machines, because of the size explosion problem: there are terms that in a linear number of steps produce an exponentially long output. The first step towards the solution is to shift to a notion of evaluation for which length and size of the output are linearly related. This is done by adopting the linear substitution calculus (LSC), a calculus of explicit substitutions modelled after linear logic proof nets and admitting a decomposition of leftmost-outermost derivations with the desired property. Thus, the LSC is invariant with respect to, say, random access machines. The second step is to show that LSC is invariant with respect to the lambda-calculus. The size explosion problem seems to imply that this is not possible: having the same notions of normal form, evaluation in the LSC is exponentially longer than in the lambda-calculus. We solve such an impasse by introducing a new form of shared normal form and shared reduction, deemed useful. Useful evaluation avoids those unsharing steps that only explicit the output without contributing to beta-redexes, i.e. the steps that cause the blow-up in size. The main technical contribution of the paper is indeed the definition of useful reductions and the thorough analysis of their properties.

ABSTRACT. Abstract--- We focus on (partial) functions that map input strings to a monoid such as the set of integers with addition and the set of output strings with concatenation. The notion of regularity for such functions has been defined using two-way finite-state transducers, (one-way) cost register automata, and MSO-definable graph transformations. In this paper, we give an algebraic and machine-independent characterization of this class analogous to the definition of regular languages by regular expressions. When the monoid is commutative, we prove that every regular function can be constructed from constant functions using the combinators of choice, split sum, and iterated sum, that are analogs of union, concatenation, and Kleene-*, respectively, but enforce unique (or unambiguous) parsing. Our main result is for the general case of non-commutative monoids, which is of particular interest for capturing regular string-to-string transformations for document processing. We prove that the following additional combinators suffice for constructing all regular functions: (1) the left-additive versions of split sum and iterated sum, which allow transformations such as string reversal; (2) sum of functions, which allows transformations such as copying of strings; and (3) function composition, or alternatively, a new concept of chained sum, which allows output values from adjacent blocks to mix.

The uploaded PDF is the concetation of the short and full versions of the paper.

ABSTRACT. We study the "approximability" of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to infinity. More specifically, for formulas in the fragments PLTL$_\Diamond$ and PLTL$_\Box$ of the Parametric Linear temporal Logic of Alur et al., we provide algorithms for computing the limit entropy as all parameters tend to ∞. As a consequence, we can decide the problem whether the limit entropy of a formula in one of the two fragments coincides with that of its time-unbounded transformation, obtained by replacing each occurrence of a time-bounded operator into its time-unbounded version. The algorithms proceed by translation of the two fragments of PLTL into two classes of discrete-time timed automata and analysis of their strongly-connected components.

ABSTRACT. Many important performance and reliability measures can be formalized as the accumulated values of weight functions. In this paper, we introduce an extension of linear time logic including past (LTL) with new operators that impose constraints on the accumulated weight along path fragments. The fragments are characterized by regular conditions formalized by deterministic finite automata (monitor DFA). This new logic covers properties expressible by several recently proposed formalisms. We study the model-checking problem for weighted transition systems, Markov chains and Markov decision processes with rational weights. While the general problem is undecidable, we provide algorithms and sharp complexity bounds for several sublogics that arise by restricting the monitoring DFA.

ABSTRACT. Graph databases make use of logics that combine traditional first-order features with navigation on paths, in the same way logics for model checking do. However, modern applications of graph databases impose a new requirement on the expressiveness of the logics: they need comparing labels of paths based on word relations (such as prefix, subword, or subsequence). This has led to the study of logics that extend basic graph languages with features for comparing labels of paths based on regular relations, or the strictly more powerful rational relations. The evaluation problem for the former logic is decidable (and even tractable in data complexity), but already extending this logic with such a common rational relation as subword or suffix turns evaluation undecidable.

In practice, however, it is rare to have the need for such powerful logics. Therefore, it is more realistic to study the complexity of less expressive logics that still allow comparing paths based on practically motivated rational relations. Here we concentrate on the most basic such languages, which extend graph pattern logics with path comparisons based only on suffix, subword or subsequence. We pinpoint the complexity of evaluation for each one of these logics, which shows that all of them are decidable in elementary time (NEXPTIME). Furthermore, the extension with suffix is even tractable in data complexity (but the other two are not). To obtain our results we establish a link between the evaluation problem for graph logics and two important problems in word combinatorics: word equations with regular constraints and square shuffling.

ABSTRACT. Desirable properties of a logic include decidability, and a model theory that inherits properties of first-order logic, such as interpolation and preservation theorems. It is known that the Guarded Fragment (GF) of first-order logic is decidable and satisfies some preservation properties from first-order model theory; however, it fails to have Craig interpolation. The Guarded Negation Fragment (GNF), a recently-defined extension, is known to be decidable and to have Craig interpolation. Here we give the first results on effective interpolation for extensions of GF. We provide an interpolation procedure for GNF whose complexity matches the doubly exponential upper bound for satisfiability of GNF. We show that the same construction gives not only Craig interpolation, but Lyndon interpolation and Relativized interpolation, which can be used to provide effective proofs of some preservation theorems. We provide upper bounds on the size of GNF interpolants for both GNF and GF input, and complement this with matching lower bounds.

ABSTRACT. This paper studies the discriminating power offered by higher-order concurrent languages, and contrasts this power with those offered by higher-order sequential languages (à la lambda-calculus) and by first-order concurrent languages (à la CCS). The concurrent higher-order languages that we focus on are Higher-Order pi-calculus (HOpi), which supports higher-order communication, and an extension of HOpi with passivation, a simple higher-order construct that allows one to obtain location-dependent process behaviours. The comparison is carried out by providing embeddings of first-order processes into the various languages, and then examining the resulting contextual equivalences induced on such processes. As first-order processes we consider both Labeled Transition Systems (LTSs) and Reactive Probabilistic Labeled Transition Systems (RPLTSs). The hierarchy of discriminating powers so obtained for RPLTSs is finer than that for LTSs; for instance, in the latter case, the additional discriminating power offered by passivation in concurrency is captured, in sequential languages, by the difference between the call-by-name and call-by-value evaluation strategies of an extended typed lambda-calculus.

ABSTRACT. We introduce a domain-theoretic framework for continuous-time, continuous-state stochastic processes. The laws of stochastic processes are embedded into the space of maximal elements of the normalised probabilistic power domain on the space of continuous interval-valued functions endowed with the relative Scott topology. We use the resulting $\omega$-continuous bounded complete dcpo to define partial stochastic processes and characterise their computability. For a given continuous stochastic process, we show how its domain-theoretic, i.e., finitary, approximations can be constructed, whose least upper bound is the law of the stochastic process. As a main result, we apply our methodology to Brownian motion. We construct a partial Wiener measure and show that the Wiener measure is computable within the domain-theoretic framework.

ABSTRACT. Regular cost functions provide a quantitative extension of regular languages that retains most of their important properties, such as expressive power and decidability, at least over finite and infinite words and over finite trees. Much less is known over infinite trees.

We consider cost functions over infinite trees defined by an extension of weak monadic second-order logic with a new fixed-point-like operator. We show this logic to be decidable, improving previously known decidability results for cost logics over infinite trees. The proof relies on an equivalence with a form of automata with counters called quasi-weak cost automata, as well as results about converting two-way alternating cost automata to one-way alternating cost automata.

ABSTRACT. The modal $\mu$-calculus, introduced by Dexter Kozen in 1981, is among the best known temporal logics studied in the theory of verification. Despite 30 years of continuous efforts, the exact complexity of its model checking problem remains elusive, and the question whether the problem can be solved in polynomial time is still unsolved.

Most work in the literature uses a game- or automata theoretic approach by reducing the model checking problem to the problem of solving parity games, a two-player game in which the formula and the transition system is combined into a single game arena.

In this paper we take a different route and study the model checking problem directly, keeping the formula and the transition system separate. This allows us to develop logical tools which manipulate the formula only and thereby studying the problem within the framework of parameterized complexity. This approach has been very successful for first- or monadic second-order logic, for instance in the work on algorithmic meta theorems.

As the main logical result of this paper we develop decomposition- or splitter-theorems for the modal $\mu$-calculus in the style of Feferman-Vaught theorems for FO and MSO. In particular, we show that if a transition system $M$ is composed of the union of two systems $M_1 \cup M_2$, then the truth of $L_\mu$-formulas at a node in $M$ essentially only depends on the truth of suitable formulas in the two systems $M_1$ and $M_2$. This result even applies to the much more general case where we allow additional edges in $M$ which start in $M_1$ and end in $M_2$.

As an algorithmic consequence we get that $L_\mu$ model-checking is fixed-parameter tractable on various classes of transition systems such as transition systems of bounded directed path width and bounded Kelly-width. To the best of our knowledge, these are among the first FPT-results for $L_\mu$ that do not follow immediately from tractability of monadic second-order logic.

ABSTRACT. We introduce parameterized communicating automata (PCA) as a model of systems where finite-state processes communicate through FIFO channels. Unlike classical communicating automata, a given PCA can be run on any network topology of bounded degree. The topology is thus a parameter of the system. We provide various Büchi-Elgot-Trakhtenbrot theorems for PCA, which roughly read as follows: Given a logical specification \phi and a class of topologies T, there is a PCA that is equivalent to \phi on all topologies from T. We give uniform constructions which allow us to instantiate T with concrete classes such as pipelines, ranked trees, grids, rings, etc. The proofs build on a locality theorem for first-order logic due to Schwentick and Barthelmann, and they exploit concepts from the non-parameterized case, notably a result by Genest, Kuske, and Muscholl.

ABSTRACT. Weighted automata are a conservative quantitative extension of finite automata that enjoys applications, e.g., in language processing and speech recognition. Their expressive power, however, appears to be limited when they are applied to more general structures than words, such as graphs. To address this drawback, weighted automata have recently been generalized to weighted pebble walking automata, which proved useful as a tool for the specification and evaluation of quantitative properties over words and nested words. In this paper, we establish the expressive power of weighted pebble walking automata in terms of transitive closure logic, lifting a similar result by Engelfriet and Hoogeboom from the boolean case to a quantitative setting. This result applies to a general class of graphs that subsumes all the aforementioned classes.

ABSTRACT. Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for equivalences of different kinds of systems. Even before Milner introduced and applied such methods in his work on CCS, Hopcroft and Karp used up-to techniques to check equivalence of deterministic automata.

In this work, we prove the soundness of such techniques in an abstract fibrational setting building on the seminal work of Hermida and Jacobs. To do this in a modular way we generalise Pous and Sangiorgi's notion of \emph{compatibility}. This allows us to systematically prove the soundness of up-to techniques, not only for bisimilarity but for a large class of coinductive predicates modeled as coalgebras. By tuning the parameters of our framework, we obtain novel proof techniques for unary predicates and nominal automata, a variant of the GSOS rule format for similarity, and a new categorical treatment of weak bisimilarity.

ABSTRACT. We study the problem of checking whether an existential sentence (that is, a first-order sentence in prefix form built using existential quantifiers and all Boolean connectives) is true in a finite partially ordered set (in short, a poset). A poset is a reflexive, antisymmetric, and transitive digraph. The problem encompasses the fundamental embedding problem of finding an isomorphic copy of a poset as an induced substructure of another poset.

The expression complexity of existential logic is NP-hard on posets; thus we investigate structural properties of posets yielding conditions for fixed-parameter tractability when the problem is parameterized by the sentence. We identify width as a central structural property (the width of a poset is the maximum size of a subset of pairwise incomparable elements); our main algorithmic result is that model checking existential logic on classes of finite posets of bounded width is fixed-parameter tractable. We observe a similar phenomenon in classical complexity, where we prove that the isomorphism problem is polynomial-time tractable on classes of posets of bounded width; this settles an open problem in order theory.

We surround our main algorithmic result with complexity results on less restricted, natural neighboring classes of finite posets, establishing its tightness in this sense. We also relate our work with (and demonstrate its independence of) fundamental fixed-parameter tractability results for model checking on digraphs of bounded degree and bounded clique-width.

ABSTRACT. We study the qualitative and quantitative zero-reachability problem in probabilistic multi-counter systems. We identify the undecidable variants of the problems, and then we concentrate on the remaining two cases. In the first case, when we are interested in the probability of all runs that visit zero in some counter, we show that the qualitative zero-reachability is decidable in time which is polynomial in the size of a given pMC and doubly exponential in the number of counters. Further, we show that the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 in time which is polynomial in log(eps), exponential in the size of a given pMC, and doubly exponential in the number of counters. In the second case, we are interested in the probability of all runs that visit zero in some counter different from the last counter. Here we show that the qualitative zero-reachability is decidable and SquareRootSum-hard, and the probability of all zero-reaching runs can be effectively approximated up to an arbitrarily small given error eps > 0 (these result applies to pMC satisfying a suitable technical condition that can be verified in polynomial time). The proof techniques invented in the second case allow to construct counterexamples for some classical results about ergodicity in stochastic Petri nets.

ABSTRACT. Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on graphs with omega-regular objectives. In this paper, we study the algorithmic properties of this concept for such games. We settle the exact complexity of natural decision problems on the set of strategies that survive iterated elimination of dominated strategies. As a byproduct of our construction, we obtain automata which recognize all the possible outcomes of such strategies.

ABSTRACT. We give a characterization, with respect a large class of models of untyped lambda-calculus, of those models which are fully abstract for head normalization, i.e., whose equational theory is H*. An extensional K-model D is fully abstract if and only if it is hyperimmune, i.e., non-well founded chains of elements of D cannot be captured by any recursive function.

ABSTRACT. We show that the satisfiability problem for the "symbolic heap" fragment of separation logic with general inductively defined predicates - which includes most fragments employed in program verification - is *decidable*. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its "base", that exactly characterises its satisfiability.

A complexity analysis of our decision procedure shows that it runs, in the worst case, in exponential time. In fact, we show that the satisfiability problem for our inductive predicates is EXPTIME-complete (by reduction from the succinct circuit value problem), and becomes NP-complete when the maximum arity over all predicates is bounded by a constant.

Finally, we provide an implementation of our decision procedure, and analyse its performance both on a synthetically generated set of test formulas, and on a second test set harvested from the separation logic literature. For the large majority of these test cases, our tool reports times in the low milliseconds.

ABSTRACT. We consider two-player non zero-sum infinite duration games played on weighted graphs. We extend the notion of secure equilibrium introduced by Chatterjee et al., from the Boolean setting to this quantitative setting. As for the Boolean setting, our notion of secure equilibrium refines the classical notion of Nash equilibrium. We prove that secure equilibria always exist in a large class of weighted games which includes common measures like sup, inf, lim sup, lim inf, mean-payoff, and discounted sum. Moreover we show that it is possible to synthesize such strategy profiles that are finite-memory and use few memory. Finally, we prove that the constrained existence problem for secure equilibria is decidable for sup, inf, lim sup, lim inf and mean-payoff measures. Our solutions rely on new results for zero-sum quantitative games with lexicographic objectives that are interesting on their own right.

ABSTRACT. We prove that the bisimulation-invariant fragment of weak monadic second-order logic (WMSO) is equivalent to the fragment of the modal $\mu$-calculus where the application of the least fixpoint operator $\mu x.\varphi$ is restricted to formulas $\varphi$ that are continuous in $x$. Our proof is automata-theoretic in nature; in particular, we introduce a class of automata characterizing the expressive power of WMSO over tree models of arbitrary branching degree. The transition map of these automata is defined in terms of a logic $\olque$ that is the extension of first-order logic with a generalized quantifier $\qu$, where $\qu x. \phi$ means that there are infinitely many objects satisfying $\phi$. An important part of our work consists of a model-theoretic analysis of $\olque$.

ABSTRACT. Behavioural symmetry is introduced into concurrent games. It expresses when plays are essentially the same. A characterization of strategies on games with symmetry is provided. This leads to a bicategory of strategies on games with symmetry. Symmetry helps allay the perhaps overly-concrete nature of games and strategies, and shares many mathematical features with homotopy. In the presence of symmetry we can consider monads for which the monad laws do not hold on the nose but do hold up to symmetry. This broadening of the concept of monad has a dramatic effect on the types concurrent games can support and allows us, for example, to recover the replication needed to express and extend traditional game semantics.

ABSTRACT. The deterministic transitive closure operator allows to express many natural properties of a binary relation, including being a linear order, a tree, a forest or a partial function. It makes it a potentially attractive ingredient of computer science formalisms. In this paper we consider the extension of the two-variable fragment of first-order logic by the deterministic transitive closure of a single binary relation, and prove that the satisfiability and finite satisfiability problems for the obtained logic are decidable and \ExpSpace-complete. This contrasts with the undecidability of two-variable logic with the deterministic transitive closures of several binary relations, known before. We also consider the class of universal first-order formulas in prenex form. Its various extensions by deterministic closure operations were earlier considered by other authors, leading to both decidability and undecidability results. We examine this scenario in more details.

ABSTRACT. The standard proof theory for logics with equality and fixpoints suffers from limitations of the sequent calculus, where reasoning is separated from computational tasks such as unification or rewriting. We propose in this paper an extension of the calculus of structures, a deep inference formalism, that supports incremental and contextual reasoning with equality and fixpoints in the setting of linear logic. This system allows deductive and computational steps to mix freely in a continuum which integrates smoothly into the usual versatile rules of multiplicative-additive linear logic in deep inference.

ABSTRACT. We study first-order model checking, by which we refer to the problem of deciding whether or not a given first-order sentence is satisfied by a given finite structure. In particular, we aim to understand on which sets of sentences this problem is tractable, in the sense of parameterized complexity theory. To this end, we define the notion of a graph-like sentence set, which definition is inspired by previous work on first-order model checking in which the permitted connectives and quantifiers were restricted. Our main theorem is the complete tractability classification of such graph-like sentence sets, which is (to our knowledge) the first complexity classification theorem concerning a class of sentences that has no restriction on the connectives and quantifiers. To present and prove our classification, we introduce and develop a novel complexity-theoretic framework which is built on parameterized complexity and includes new notions of reduction.

ABSTRACT. We study the problem of conjunctive query evaluation over classes of queries; this problem is formulated here as the relational homomorphism problem over a class of structures A, wherein each instance must be a pair of structures such that the first structure is an element of A.

We present a comprehensive complexity classification of these problems, which strongly links graph-theoretic properties of A to the complexity of the corresponding homomorphism problem. In particular, we define a binary relation on graph classes and completely describe the resulting hierarchy given by this relation. This binary relation is defined in terms of a notion which we call graph deconstruction and which is a variant of the well-known notion of tree decomposition. We then use this graph hierarchy to infer a complexity hierarchy of homomorphism problems which is comprehensive up to a computationally very weak notion of reduction, namely, a parameterized version of quantifier-free reductions. In doing so, we obtain a significantly refined complexity classification of homomorphism problems, as well as a unifying, modular, and conceptually clean treatment of existing complexity classifications.

We then present and develop the theory of Ehrenfeucht-Fra\"{i}ss\'{e}-style pebble games which solve the homomorphism problems where the cores of the structures in A have bounded tree depth; as a fruit of this development, we characterize the homomorphism problems solvable in logarithmic space. Finally, we use our framework to classify the complexity of model checking existential sentences having bounded quantifier rank.

ABSTRACT. Labelled Markov chains (LMCs) are widely used in probabilistic verification, speech recognition, computational biology, and many other fields. Checking two LMCs for equivalence is a classical problem subject to extensive studies, while the total variation distance provides a natural measure for the ``inequivalence'' of two LMCs: it is the maximum difference between probabilities that the LMCs assign to the same event.

In this paper we develop a theory of the total variation distance between two LMCs, with emphasis on the algorithmic aspects: (1) we provide a polynomial-time algorithm for determining whether two LMCs have distance 1, i.e., whether they can almost always be distinguished; (2) we provide an algorithm for approximating the distance with arbitrary precision; and (3) we show that the threshold problem, i.e., whether the distance exceeds a given threshold, is NP-hard and hard for the square-root-sum problem. We also make a connection between the total variation distance and Bernoulli convolutions.

ABSTRACT. We present a second-order calculus with coercion constraints that generalizes our previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions and equi-recursive types. This allows to present in a uniform way many type system features that had previously been studied separately: type containment, bounded and instance-bounded polymorphism, which are already encodable with parametric coercion abstraction, and ML-style but second-order subtyping constraints. Our framework allows for a clear separation of language constructs with and without computational content. We also distinguish coherent coercions that are fully erasable from potentially incoherent coercions that must suspend the evaluation---and enable the encoding of GADTs. Technically, type coercions that witness subtyping relations between types are replaced by a more expressive notion of typing coercions that witness subsumption relations between typings, e.g. pairs composed of a typing environment and a type. Our calculus is equipped with a strong notion of reduction that allows reduction under abstractions---but we also introduce a form of weak reduction as reduction cannot proceed under incoherent type abstractions. Type soundness is proved by adapting the step-indexed semantics technique to strong reduction strategies, moving indices inside terms so as to control the reduction steps internally.

ABSTRACT. We incept synchronization into the most concrete model of Girard’s Geometry of Interaction, namely token ma- chines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling synchronization points, and a multi-token abstract machine model for it. Interestingly, a correctness criterion ensures the absence of deadlock, this way linking logical and operational properties in a novel way.

ABSTRACT. We construct quasipolynomial-size proofs of the propositional pigeonhole principle in the deep inference system KS, addressing an open problem raised in previous works and matching the best known upper bound for the more general class of monotone proofs.

We make significant use of monotone formulae computing boolean threshold functions, an idea previously considered in works of Atserias et al. The main construction, monotone proofs witnessing the symmetry of such functions, makes use of an implementation of merge-sort in the design of proofs in order to tame the structural behaviour of atoms, and so the complexity of normalisation. Proof transformations from previous work on atomic flows are then employed to yield appropriate proofs in KS.

As further results we show that our constructions can be applied to provide quasipolynomial-size proofs of the Parity principle and the Generalised Pigeonhole principle, and n^(O(log log n))-size proofs of the weak pigeonhole principle, thereby also improving the best known bounds for monotone proofs.

ABSTRACT. We show that first-order separation logic restricted to two variables and to separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result without such syntactic restrictions. So, two variables suffice for capturing second-order logic and we do so by using only separating implication, which requires a non-trivial update to known proof techniques. As a by-product, we identify the smallest fragment of separation logic known to be undecidable, namely first-order separation logic with one record field, two variables, and no separating conjunction.

ABSTRACT. In Girard's original presentation, proof structures of Linear Logic are hypergraphs whose hyperedges are labeld by logical rules and vertices represent the connections between these logical rules. Presentations of proof structures based on interaction nets have the same kind of graphical flavour. Other presentations of proof structures use terms instead of graphs or hypergraphs. The atomic ingredient of these terms are variables related by axiom links. However, the correctness criteria developped so far are adapted to the graphical presentations of proof structures and not to their term-based presentations. We propose a new correctnes criterion for constant-free Multiplicative Linear Logic with Mix which applies to a coherence space structure that a term-based proof structure induces on the set of its variables in a straightforward way.

ABSTRACT. We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control, PerD0L systems for short. These systems give rise to a class of one-sided infinite sequences, called PerD0L words. We construct a PerD0L word with exponential subword complexity, thereby answering a question raised by (Lepisto 1993) on the existence of such words. We solve another open problem concerning the decidability of the first-order theories of PerD0L words (Muchnik, Pritykin, Semenov 2009); we show it is already undecidable whether a certain letter occurs in a PerD0L word. This stands in sharp contrast to the situation for D0L words (purely morphic words), which are known to have at most quadratic subword complexity, and for which the monadic theory is decidable.

ABSTRACT. A common theme in the study of logics over finite structures is adding auxiliary predicates to enhance expressiveness and convey additional information. Examples include adding an order or arithmetic for capturing complexity classes, or the power of real-life declarative languages. A recent trend is to add a data-value comparison relation to words, trees, and graphs, for capturing modern data models such as XML and graph databases.

Such additions often result in the loss of good properties of the underlying logic. Our goal is to show that such a loss can be avoided if we use pattern-based logics, standard in XML and graph data querying. The essence of such logics is that auxiliary relations are tested locally with respect to other relations in the structure. These logics are shown to admit strong versions of Hanf and Gaifman locality theorems, which are used to prove a homomorphism preservation theorem, and a decidability result for the satisfiability problem. We discuss applications of these results to pattern logics over data forests, and consequently to querying XML data.

ABSTRACT. Algebraic structures abound in programming languages. The starting point for this paper is the following theorem: (first-order) algebraic signatures can themselves be described as free algebras for a (second-order) algebraic theory of substitution. Transporting this to the realm of programming languages, we investigate a computational metalanguage based on the theory of substitution, demonstrating that substituting corresponds to jumping in an abstract machine. We use the theorem to give an interpretation of a programming language with arbitrary algebraic effects into the metalanguage with substitution/jumps.

ABSTRACT. Applications increasingly derive functionality from sensitive personal information, forcing developers who wish to preserve some notion of privacy or confidentiality to reason about partial information leakage. New definitions of privacy and confidentiality, such as differential privacy, address this by offering precise statements of acceptable disclosure that are useful in common settings. However, several recent published accounts of flawed implementations have surfaced, highlighting the need for verification techniques.

In this paper, we pose the problem of model-counting satisfiability, and show that a diverse set of privacy and confidentiality verification problems can be reduced to instances of it. In this problem, constraints are placed on the outcome of model-counting operations, which occur over formulas containing parameters. The object is to find an assignment to the parameters that satisfies the model-counting constraints, or to demonstrate unsatisfiability.

We present a logic for expressing these problems, and a theory that defines the semantics of this logic. We develop an abstract decision procedure for model-counting satisfiability problems fashioned after CDCL-based SMT procedures, encapsulating functionality specific to the underlying logic in which counting occurs in a small set of black-box routines similar to those required of theory solvers in SMT. We describe an implementation of this procedure for linear-integer arithmetic, as well as an effective strategy for generating lemmas. We conclude by applying our decision procedure to the verification of privacy properties over programs taken from a well-known privacy-preserving compiler, demonstrating its ability to find flaws or prove correctness sometimes in a matter of seconds.

ABSTRACT. The hypergraph duality problem DUAL is defined as follows: given two simple hypergraphs G and H, decide whether H consists precisely of all minimal transversals of G (in which case we say that G is the dual of H). This problem is equivalent to decide whether two given non-redundant DNFs are dual. While it is well-known that DUAL can be decided in time n^{o(log n)), the precise complexity of this problem has been open problem for over 20 years. The "guess-and-check" complexity class GC(f(n),C) contains all problems that after a nondeterministic guess of O(f(n)) bits can be decided (checked) in complexity class C. It is known that non-DUAL, the complement of DUAL, is in GC(log^2 n, PTIME) and it was more recently shown that DUAL lies in DSPACE[log^2 n]. It was conjectured that non-DUAL is in GC(log^2 n, LOGSPACE).

In this paper we prove this conjecture and actually place the non-DUAL problem into the complexity class GC(log^2 n, TC_0) which is contained in GC(log^2 n, LOGSPACE). Wh here refer to the logtime-uniform version of TC_0, which corresponds first order logic augmented by majority quantifiers (also known as FOM). We achieve the latter bound in two steps. First we develop a new nondeterministic algorithm for DUAL that exploits, and slightly modifies, existing problem decomposition methods and uses only O(log^2 n) nondeterministic bits. We then proceed by a logical analysis, that allows us to formulate the deterministic part in FOM, i.e., in first order logic with majority quantifiers. Putting these results together yields the desired upper bound GC(log^2 n, TC_0). In summary, we have derived an improved upper bound for DUAL via logical methods.

ABSTRACT. Certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests. We show how to axiomatically extend KAT with this feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

ABSTRACT. We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first system is a direct adaptation of the sequent calculus to the deep inference setting, and we provide a procedure for cut elimination, similar to the one from the sequent calculus, using on non-local rewriting. The second system is the symmetric completion of the first, as normally given in deep inference for logics with DeMorgan duality: each inference rule has a dual rule, cut being dual to the identity axiom. We prove a generalisation of cut elimination, that we call symmetric normalisation, where all rules dual to standard ones are permuted up in the derivation. The result is a decomposition theorem having cut elimination and interpolation as corollaries.

ABSTRACT. Event structures are a model of concurrency with a natural game-theoretic interpretation, which was initially given in terms of zero-sum games only. This paper studies an extension of such games to include a much wider class of game types and solution concepts. The extension permits modelling scenarios where, for instance, cooperation or independent goal-driven behaviour of computer agents is desired. Specifically, we define non-zero-sum games on event structures, and give full characterisations---existence and completeness results---of the kinds of games, payoff sets, and strategies for which Nash equilibria and subgame perfect Nash equilibria always exist. The game semantics of various logics and systems are outlined to illustrate the power of this framework.

ABSTRACT. It is shown that for any fixed $i>0$, the $\Sigma_{i+1}$-fragment of Presburger arithmetic, \emph{i.e.}, its restriction to $i+1$ quantifier alternations beginning with an existential quantifier, is complete for $\Sigma^{\text{EXP}}_{i}$, the $i$-th level of the weak EXP hierarchy. This result completes the computational complexity landscape for Presburger arithmetic, a line of research which dates back to the seminal work by Fischer \& Rabin in 1974. The second part of the paper applies some techniques developed in the first part in order to establish bounds on sets of naturals definable in the $\Sigma_1$-fragment of Presburger arithmetic: given a $\Sigma_1$-formula $\Phi(x)$, it is shown that the set of solutions is an ultimately periodic set whose period can be doubly-exponentially bounded from below and above.

ABSTRACT. Ground Tree Rewrite Systems with State are known to have an undecidable control state reachability problem. Taking inspiration from the recent introduction of scope-bounded multi-stack pushdown systems, we define Senescent Ground Tree Rewrite Systems. These are a restriction of ground tree rewrite systems with state such that nodes of the tree may no longer be rewritten after having witnessed an a priori fixed number of control state changes. As well as generalising scope-bounded multi-stack pushdown systems, we show --- via reductions to and from reset Petri-nets --- that these systems have an Ackermann-complete control state reachability problem. However, reachability of a regular set of trees remains undecidable.

ABSTRACT. We provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+MOD_m) on the class C_d of all finite structures of degree at most d: For each FO+MOD_m-sentence that is preserved under homomorphisms (extensions) on C_d, a C_d-equivalent existential-positive (existential) FO-sentence can be constructed in 4-fold (6-fold) exponential time. For FO-sentences, the algorithm has 3-fold (5-fold) exponential time complexity. This is complemented by lower bounds showing that for FO-sentences a 3-fold exponential blow-up of the computed existential-positive (existential) sentence is unavoidable.

Furthermore, we show that for an input FO-formula, a C_d-equivalent Feferman-Vaught decomposition can be computed in 3-fold exponential time. We also provide a matching lower bound.

ABSTRACT. MLL proof equivalence is the problem of deciding whether two proofs in multiplicative linear logic are related by a series of inference permutations. It is also known as the word problem for star-autonomous categories. Previous work has shown the problem to be equivalent to a rewiring problem on proof nets, which are not canonical for full MLL due to the presence of the two units. Drawing from recent work on reconfiguration problems, in this paper it is shown that MLL proof equivalence is PSPACE-complete, using a reduction from Nondeterministic Constraint Logic. An important consequence of the result is that the existence of a satisfactory notion of proof nets for MLL with units is ruled out (under current complexity assumptions).

ABSTRACT. We describe the construction of an abstract lattice from a given Buchi automata. The abstract lattice is finite and has the following key properties. (i) There is a Galois connection between the (infinite) lattice of languages of finite and infinite words over a given alphabet. (ii) The abstraction is faithful with respect to acceptance by the automaton. (iii) Least fixpoints and w-iterations (but not in general greatest fixpoints) can be computed on the level of the abstract lattice.

This allows one to develop an abstract interpretation capable of checking whether finite and infinite traces of a (recursive) program are accepted by a policy automaton. It is also possible to cast this analysis in the form of a type and effect system with the effects being elements of the abstract lattice.

While the resulting decidability and complexity results are known (regular model checking for pushdown systems) the abstract lattice provides a new point of view and enables smooth integration with data types, objects, higher-order functions which are best handled with abstract interpretation or type systems.

We demonstrate this by generalising our type-and-effect systems to object-oriented programs and higher-order functions.

ABSTRACT. Girard's Geometry of Interaction (GoI) is interaction-based semantics of linear logic proofs and, via suitable translations, of functional programs in general. Its mathematical cleanness identifies essential structures in computation; moreover its use as a compilation technique from programs to state-based machines has been worked out by Mackie, Ghica and others. In this paper, we take Abramsky's idea of resumption-based GoI and develop it systematically into a generic framework that accounts for computational effects (nondeterminism, probability, exception, global states, interactive I/O, etc.). The framework is categorical: algebraic operations provide an interface to computational effects (following Plotkin and Power); the framework is built on the categorical axiomatization of GoI by Abramsky, Haghverdi and Scott; and, by use of the coalgebraic formalization of component calculus, the framework describes explicit construction of state machines as interpretations of functional programs. The obtained models are shown to be sound with respect to equations between algebraic operations, as well as to Moggi's standard equations for the computational lambda calculus. The construction is illustrated by concrete examples.

ABSTRACT. We consider the problem of characterizing isomorphisms of types, or equivalently constructive cardinality of sets, in simultaneous presence of disjoint unions, Cartesian products, and exponentials. Mostly relying on classic results concerning polynomials with exponentiation that have not been used in our context, we derive: that the usual finite axiomatization known as High School Identities (HSI) is complete for a significant subclass of types; that it is decidable for that subclass when two types are isomorphic; that, for the whole of the set of types, a recursive extension of the axioms of HSI exists that is complete; and that, for the whole of the set of types, the question whether two types are isomorphic is decidable, that is, at least when base types are to be interpreted by finite sets. We also point out certain related open problems.

ABSTRACT. Functional Reactive Programming (FRP) is an approach to streaming data with a pure functional semantics as time-indexed values. In previous work, we showed that Linear-time Temporal Logic (LTL) can be used as a type system for discrete-time FRP, and that functional reactive primitives perform two roles: as combinators for building streams of data, and as proof rules for constructive LTL. In this paper, we add a third role, by showing that FRP combinators can be used to define streams of types, and that these functional reactive types can be viewed both as a constructive temporal logic, and as the types for functional reactive programs. As an application of functional reactive types, we show that past-time LTL (pLTL) can be extended with FRP to get a logic pLTL+FRP. This logic is expressed as streams of boolean expressions, and so bounded satisfiability of pLTL can be translated to Satisfiability Modulo Theory (SMT). Thus, pLTL+FRP can be used as a constraint language for problems which mix properties of data with temporal properties.

ABSTRACT. This paper presents a formal characterisation of safety and liveness properties à la Alpern and Schneider for fully probabilistic systems. As for the classical setting, it is established that any (probabilistic tree) property is equivalent to a conjunction of a safety and liveness property. A simple algorithm is provided to obtain such property decomposition for flat probabilistic CTL (PCTL). A safe fragment of PCTL is identified that provides a sound and complete characterisation of safety properties. For liveness properties, we provide two PCTL fragments, a sound and a complete one. We show that safety properties only have finite counterexamples, whereas liveness properties have none. We compare our characterisation for qualitative properties with the one for branching time properties by Manolios and Trefler, and present sound and complete PCTL fragments for characterising the notions of strong safety and absolute liveness by Sistla.

ABSTRACT. The last two decades have witnessed significant advances in the investigation of algorithmic randomness, such as Martin-Lof randomness, of infinite strings. In spite of much work, research on randomness of infinite strings has excluded the investigation of algorithmic randomness for infinite algebraic structures. The main obstacle in introducing algorithmic randomness for infinite structures is that many classes of infinite structures lack measure. In this paper, we overcome this obstacle by proposing a limited amount of finiteness conditions on various classes of infinite structures. These conditions will enable us to introduce measure and, as a consequence, reason about algorithmic randomness. Our classes include finitely generated universal algebras, connected graphs and tress of bounded degree, and monoids. For all these classes one can introduce algorithmic randomness concepts and prove existence of random structures.

ABSTRACT. We investigate the size of first-order rewritings of conjunctive queries over OWL 2 QL ontologies of depth 1 and 2 by means of hypergraph programs computing Boolean functions. Both positive and negative results are obtained. Conjunctive queries over ontologies of depth 1 have polynomial-size nonrecursive datalog rewritings; tree-shaped queries have quadratic positive existential rewritings; however, in the worst case, positive existential rewritings can only be of superpolynomial size. Positive existential and nonrecursive datalog rewritings of queries over ontologies of depth 2 suffer an exponential blowup in the worst case, while first-order rewritings are superpolynomial unless NP \subseteq P/poly. We also analyse rewritings of tree-shaped queries over arbitrary ontologies and observe that the query entailment problem for such queries is fixed-parameter tractable.

ABSTRACT. We study deterministic computability over sets with atoms. We characterize those alphabets for which Turing machines with atoms determinize. To this end, the determinization problem is expressed as a Constraint Satisfaction Problem, and a characterization is obtained from deep results in CSP theory. As an application to Descriptive Complexity Theory, within a substantial class of relational structures including Cai-F\"urer-Immerman graphs, we precisely characterize those subclasses where the logic IFP+C captures order-invariant polynomial time computation.

ABSTRACT. We present the first method for reasoning about temporal logic properties of higher-order, infinite-data programs. By distinguishing between the finite traces and infinite traces in the specification, we obtain rules that permit us to reason about the temporal behavior of program parts via a type-and-effect system, which is then able to compose these facts together to prove the overall target property of the program. The type system alone is strong enough to derive many temporal safety properties, for example when using refinement types and temporal effects. We also show how existing techniques can be used as oracles to provide liveness information (e.g. termination) about program parts and that the type-and-effect system can combine this information with temporal safety information to derive nontrivial temporal properties. Our work has application toward verification of higher-order software, as well as modular strategies for procedural programs.

ABSTRACT. Two graphs are Hanf-equivalent with respect to radius r if there is a bijection between their vertex sets which preserves the isomorphism types of the vertices' neighbourhoods of radius r. For r=1 this means that the graphs have the same degree sequence.

In this paper we relate Hanf-equivalence to the graph-theoretical concept of subgraph equivalence. To make this concept applicable to graphs that are not necessarily connected, we first generalise the notion of the radius of a connected graph to general graphs in a suitable way, which we call the generalised radius. We say that two graphs G and H are subgraph-equivalent up to generalised radius r if for all graphs S of generalised radius r, the number of induced subgraphs isomorphic to S in G is the same as the number of such subgraphs in H.

We prove that Hanf-equivalence with respect to radius r is equivalent to subgraph-equivalence up to generalised radius r, thereby relating the purely logical and the graph-theoretical concepts in a very strong way.

The notion of subgraph-equivalence up to order s is defined accordingly, where all graphs S of order at most s are taken into account. As a corollary we obtain that Hanf-equivalence with respect to radius r implies subgraph-equivalence up to order s, provided that r is of size at least 3s/4. In particular, this implies that two graphs which are Hanf-equivalent with respect to radius r satisfy the same purely existential first-order sentences of quantifier rank r.

ABSTRACT. We study the complexity of reachability problems on branching extensions of vector addition systems, which allows us to derive new non-elementary complexity bounds for fragments and variants of propositional linear logic. We show that provability in the multiplicative exponential fragment is non-elementary already in the affine case, and match this lower bound for the full propositional affine linear logic, proving its Tower-completeness. We also show that provability in propositional contractive linear logic is Ackermann-complete.

ABSTRACT. We investigate the existence of certain types of equilibria (Nash, $\varepsilon$-Nash, subgame perfect, $\varepsilon$-subgame perfect) in infinite sequential games with real-valued payoff functions depending on the class of payoff functions (continuous, upper semi-continuous, Borel) and whether the game is zero-sum. Our results hold for games with two or up to countably many players.

Several of these results are corollaries of stronger results that we establish about equilibria in infinite sequential games with some weak conditions on the occurring preference relations. We also formulate an abstract equilibrium transfer result about games with compact strategy spaces and open preferences. Finally, we consider a dynamical improvement rule for infinite sequential games with continuous payoff functions.

ABSTRACT. This paper studies the boundedness and termination problems for vector addition systems equipped with one stack. We introduce an algorithm, inspired by the Karp & Miller algorithm, that solves both problems for the larger class of well-structured pushdown systems. We show that the worst-case running time of this algorithm is hyper-Ackermannian for pushdown vector addition systems. For the upper bound, we introduce the notion of bad nested words over a well-quasi-ordered set, and we provide a general scheme of induction for bounding their lengths. We derive from this scheme a hyper-Ackermannian upper bound for the length of bad nested words over vectors of natural numbers. For the lower bound, we exhibit a family of pushdown vector addition systems with finite but large reachability sets (hyper-Ackermannian).

ABSTRACT. This paper describes a framework for game semantics combining operational and denotational accounts. The operational part is given by a transition system in which the set of permitted actions changes over time, as described by the rules of a game. The denotational part is given by a ``transfer'' between games, which describes a way of operating on strategies. The agreement between the two is given by a relation called a ``stepped bisimulation''. The framework is illustrated by an example of substitution within a lambda-calculus.

ABSTRACT. Many verification problems can be reduced to refinement verification. However, existing work on verifying refinement of concurrent programs either fails to prove the preservation of termination, allowing a diverging program to trivially refine any programs, or is difficult to apply in compositional thread-local reasoning. In this paper, we first propose a new simulation technique, which establishes termination-preserving refinement and is a congruence with respect to parallel composition. Then we give a proof theory for the simulation, which is the first Hoare-style concurrent program logic supporting termination-preserving refinement proofs. We show two key applications of our logic, i.e., verifying linearizability and lock-freedom together for fine-grained concurrent objects, and verifying full correctness of optimizations of concurrent algorithms.

ABSTRACT. Homotopy type theory is an extension of Martin-L\"of type theory with principles inspired by category theory and homotopy theory. With these extensions, type theory can be used to construct proofs of homotopy-theoretic theorems, in a way that is very amenable to computer-checked proofs in proof assistants such as Coq and Agda. In this paper, we give a computer-checked construction of \emph{Eilenberg-MacLane spaces}. For an abelian group $G$, an Eilenberg-MacLane space $K(G,n)$ is a space (type) whose $n^{th}$ homotopy group is G, and whose homotopy groups are trivial otherwise. These spaces are a basic tool in algebraic topology; for example, they can be used to build spaces with specified homotopy groups, and to define the notion of cohomology with coefficients in $G$. Their construction in type theory is an illustrative example, which ties together many of the constructions and methods that have been used in homotopy type theory so far.

ABSTRACT. We investigate efficient view maintenance for MSO-definable queries over trees or, more precisely, efficiently enumerating answers of MSO-definable queries over words and trees which are subject to local updates. For words we exhibit an algorithm that uses an O(n) preprocessing phase and enumerates answers with O(log n) delay between them. When the word is updated, the algorithm can avoid repeating expensive preprocessing and restart the enumeration phase within O(log n) time. For trees, our algorithm uses O(n) preprocessing time, enumerates answers with O(log^2 n) delay, and can restart enumeration within O(log^2 n) time after receiving an update to the tree. This significantly improves the cost of recomputing the answers of a query from scratch.

ABSTRACT. Modify the Blum-Shub-Smale model of computation replacing the permitted computational primitives (the real field operations) with any finite set B of real functions semialgebraic over the rationals. Consider the class of boolean decision problems that can be solved in polynomial time in the new model by machines with no machine constants. How does this class depend on B? We prove that it is always contained in the class obtained for B = {+, −, ×}. Moreover, if B is a set of continuous semialgebraic functions containing + and −, and such that arbitrarily small numbers can be computed using B, then we have the following dichotomy: either our class is P or it coincides with the class obtained for B = {+, −, ×}.

ABSTRACT. The equational theory of monadic recursion schemes is known to be decidable by the result of S\'enizergues on the decidability of the problem of DPDA equivalence. In order to capture some properties of the domain of computation, we augment equations with certain hypotheses. This preserves the decidability of the theory, which we call \emph{simple implicational theory}. The asymptotically fastest algorithm known for deciding the equational theory, and also for deciding the simple implicational theory, has running time that is non-elementary. We therefore consider a restriction of the properties about schemes to check: instead of arbitrary equations $f \equiv g$ between schemes, we focus on propositional Hoare assertions $\{p\}f\{q\}$, where $f$ is a scheme and $p, q$ are tests. Such Hoare assertions have a straightforward encoding as equations. We investigate the \emph{Hoare theory} of monadic recursion schemes, that is, the set of valid implications whose conclusions are Hoare assertions and whose premises are of a certain simple form. We present a sound and complete Hoare-style calculus for this theory. We also show that the Hoare theory can be decided in exponential time, and that it is complete for this class.

ABSTRACT. We are interested in the constructive interpretation of reasoning by contrapositive in classical logic, or, in other words, of an involutive negation.

We first review the impossibility of an involutive negation in the call-by-name lambda-C calculus: we conclude that it is a defect of the evaluation strategy, which makes captured stacks undistinguishable from continuations.

Then we introduce extensional and untyped calculi for both of classical sequent calculus and classical natural deduction with connectives for an involutive negation. The involutivity is achieved using focalisation and polarisation, which allow us to implement the idea that captured stacks, unlike continuations, can be inspected. Falsity is given a computational interpretation by delimiting control.

This establishes a formulae-as-types correspondence between the involutive negation in proof theory and a notion of high-level access to the stack theorised by Felleisen and Clements. This allows us to explain the isomorphism we have between not-forall and exists-not.

ABSTRACT. To ensure consistency and decidability of type checking, proof assistants impose a requirement of productivity on corecursive definitions. In this paper we investigate a type-based alternative to the existing syntactic productivity checks of Coq and Agda, using a combination of guarded recursion and quantification over clocks. This approach was developed by Atkey and McBride in the simply typed setting, here we extend it to a calculus with dependent types. Building on previous work on the topos-of-trees model we construct a model of the calculus using a family of presheaf toposes, each of which can be seen as a multi-dimensional version of the topos-of-trees. As part of the model construction we must solve the coherence problem for modelling dependent types in locally cartesian closed categories simulatiously in a whole family of locally cartesian closed categories. We do this by embedding all the categories in a large one and applying a recent approach to the coherence problem due to Streicher and Voevodsky.

ABSTRACT. We study two refinements of the linear π-calculus that ensure deadlock freedom (the absence of stable states with pending linear communications) and lock freedom (the eventual completion of pending linear communications). The main feature of both type systems is a new form of channel polymorphism that affects their accuracy in a significant way: they are the first of their kind that can deal with recursive processes communicating in cyclic network topologies.

ABSTRACT. Context semantics is a tool inspired by Girard' s geometry of interaction. It has had many applications from study of optimal reduction to proofs of complexity bounds. However, context semantics have been defined only on lambda-calculus and linear logic. In order to study other languages, in particular languages with more primitives (built-in arithmetics, pattern matching,…) we define a context semantics for a broader framework: interaction nets. These are a well-behaved class of graph rewriting systems. Here, two applications are explored. First, we define a notion of weight, based on context semantics paths, which bounds the length of reduction of nets. This could be used to prove strong complexity bounds for interaction net systems. Then, we define a denotational semantics for a large class of interaction net systems.

ABSTRACT. Gabbay's separation theorem is a fundamental result for linear temporal logic (LTL). We show that separating a restricted class of LTL formulas, called anchored LTL, is elementary if and only if the translation from LTL to the linear temporal logic with only future temporal connectives is elementary. To prove this result, we define a canonical separation for LTL, and establish a correspondence between a canonical separation of anchored LTL formulas and the omega-automata that recognize these formulas. The canonical separation of anchored LTL formulas has two further applications. First, we constructively prove that the safety closure of any LTL property is an LTL property, thus proving the decomposition theorem for LTL: every LTL formula is equivalent to the conjunction of a safety LTL formula and a liveness LTL formula. Second, we characterize safety, liveness, absolute liveness, stable, and fairness properties in LTL. Our characterization is effective: We reduce the problem of deciding whether an LTL formula defines any of these properties to the validity problem for LTL.

ABSTRACT. Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we prove that this technique can be generalized to answer the same question for regular languages of infinite words.

ABSTRACT. We consider the two-variable fragment of first-order logic with counting quantifiers, subject to the stipulation that a single distinguished binary predicate be interpreted as an equivalence. We show that the satisfiability and finite satisfiability problems for this logic are both NExpTime-complete.

ABSTRACT. In this paper, we present a modern reformulation of the Dialectica interpretation based on the linearized version of De Paiva. Contrarily to Gödel's original translation which translated HA into system T, our presentation applies on untyped λ-terms and features nicer proof-theoretical properties.

In the Curry-Howard perspective, we show that the computational behaviour of this translation can be accurately described by the explicit stack manipulation of the Krivine abstract machine, thus giving it a direct-style operational explanation.

Finally, we give direct evidence that supports the fact our presentation is quite relevant, by showing that we can apply it to the dependently-typed system CCω almost without any adaptation. This answers the question of the validity of Dialectica-like constructions in a dependent setting.

ABSTRACT. We introduce type-checking games, which are omega-regular games over Boehm trees, determined by a type of the Kobayashi-Ong intersection type system. These games are a higher-type extension of parity games over trees, determined by an alternating parity tree automaton. However, in contrast to these games over trees, the "game boards" of our type-checking games are composable, using the composition of Boehm trees. Moreover the winner of a composite game is completely determined by the respective winners of the component games.

To our knowledge, type-checking games give the first compositional analysis of higher-order model checking, or the model checking of trees generated by recursion schemes. We study a higher-type analogue of higher order model checking, namely, the problem to decide the winner of a type-checking game over the Boehm tree generated by a lambda-Y-term. We introduce a new type system and use it to prove that the problem is decidable.

On the semantic side, we develop a novel arena game model for type-checking games, which is a cartesian closed category equipped with parametric monad and comonad that themselves form a parametrised adjunction.

ABSTRACT. Two-player games on graphs provide the mathematical foundation for the study of reactive systems. In the quantitative framework, an objective assigns a value to every play, and the goal of player 1 is to minimize the value of the objective. In this framework, there are two relevant synthesis problems to consider: the quantitative analysis problem is to compute the minimal (or infimum) value that player 1 can assure, and the boolean analysis problem asks whether player 1 can assure that the value of the objective is at most r (for a given threshold r). Mean-payoff expression games are played on a multidimensional weighted graph. An atomic mean-payoff expression objective is the mean-payoff value (the long-run average weight) of a certain dimension, and the class of mean-payoff expressions is the closure of atomic mean-payoff expressions under the algebraic operations of max, min, numerical complement and sum. In this work, we study for the first time the strategy synthesis problems for games with robust quantitative objectives, namely, games with mean-payoff expression objectives. While in general, optimal strategies for these games require infinite-memory, in synthesis we are typically interested in the construction of a finite-state system. Hence, we consider games in which player 1 is restricted to finite-memory strategies, and our main contribution is as follows. We prove that for mean-payoff expressions, the quantitative analysis problem is computable, and the boolean analysis problem is inter-reducible with Hilbert's tenth problem over rationals --- a fundamental long-standing open problem in computer science and mathematics.

ABSTRACT. First-order logic captures a vast number of computational problems on graphs. We study the time complexity of deciding graph properties definable by first-order sentences with $k$ variables. The trivial algorithm for this problem runs in $O(n^k)$ time on $n$-node graphs (the big-O hides the dependence on $k$).

Answering a question of Miki Ajtai, we give the first algorithms running faster than the trivial algorithm, in the general case of arbitrary first-order sentences and arbitrary graphs. One algorithm runs in $O(n^{k-3+\omega)} \leq O(n^{k-0.627})$ time for all $k \geq 3$, where $\omega < 2.373$ is the $n \times n$ matrix multiplication exponent. By applying fast rectangular matrix multiplication, the algorithm can be improved further to run in $O(n^{k-1+o(1)})$ time, for all $k \geq 9$. Finally, we observe that the exponent of $k-1$ is optimal, under the hypothesis that CNF satisfiability with $n$ variables and $m$ clauses cannot be solved in $(2-\epsilon)^n \cdot \poly(m)$ time for some $\epsilon > 0$.