CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)

Full Citation in the ACM Digital Library

SESSION: Invited speakers

Trade-off analysis meets probabilistic model checking

Probabilistic model checking (PMC) is a well-established and powerful method for the automated quantitative analysis of parallel distributed systems. Classical PMC-approaches focus on computing probabilities and expectations in Markovian models ...

Abstract interpretation: past, present and future

Abstract interpretation is a theory of abstraction and constructive approximation of the mathematical structures used in the formal description of complex or infinite systems and the inference or verification of their combinatorial or undecidable ...

TUTORIAL SESSION: Invited tutorials

Understanding biology through logic

The complexity in biology is staggering. Biological processes involve many components performing complicated interactions. Moreover, they are organized in hierarchies spanning multiple levels going from individual genes and proteins to signalling ...

Computer-checked mathematics: a formal proof of the odd order theorem

The Odd Order Theorem is a landmark result in finite group theory, due to W. Feit and J. G. Thompson [1], which states that every finite group of odd order is solvable. It is famous for its crucial role in the classification of finite simple groups, for ...

SESSION: Award citations

The Ackermann award 2014

Report of the Jury for the 2014 Ackermann Award.

Citations for the test-of-time award from 1994

Two awards were made in 2014 to honor outstanding papers from the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS '94) held in Paris, France, July 4-7, 1994.

SESSION: Contributed papers

Infinite-state energy games

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

Beta reduction is invariant, indeed

Slot and van Emde Boas' weak invariance thesis states that reasonable machines can simulate each other within a polynomially overhead in time. Is λ-calculus a reasonable machine? Is there a way to measure the computational complexity of a λ-term? This ...

Regular combinators for string transformations

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

Asymptotic behaviour in temporal logic

We study the "approximability" of unbounded temporal operators with time-bounded operators, as soon as some time bounds tend to ∞. More specifically, for formulas in the fragments PLTL and PLTL of the Parametric Linear Temporal Logic of Alur et al., ...

Weight monitoring with linear temporal logic: complexity and decidability

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

Graph logics with rational relations: the role of word combinatorics

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

Effective interpolation and preservation in guarded logics

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

On the discriminating power of passivation and higher-order interaction

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 λ-calculus) and by first-order concurrent languages (à la CCS). The ...

A domain-theoretic approach to Brownian motion and general continuous stochastic processes

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

Two-way cost automata and cost logics over infinite trees

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

Decomposition theorems and model-checking for the modal μ-calculus

We prove a general decomposition theorem for the modal μ-calculus Lμ in the spirit of Feferman and Vaught's theorem for disjoint unions. In particular, we show that if a structure (i.e., transition system) is composed of two substructures M1 and M2 plus ...

Logic for communicating automata with parameterized topology

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

Logical characterization of weighted pebble walking automata

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, especially when they are applied to ...

Coinduction up-to in a fibrational setting

Bisimulation up-to enhances the coinductive proof method for bisimilarity, providing efficient proof techniques for checking properties of different kinds of systems. We prove the soundness of such techniques in a fibrational setting, building on the ...

Model checking existential logic on partially ordered sets

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

Zero-reachability in probabilistic multi-counter automata

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

The complexity of admissibility in Omega-regular games

Iterated admissibility is a well-known and important concept in classical game theory, e.g. to determine rational behaviors in multi-player matrix games. As recently shown by Berwanger, this concept can be soundly extended to infinite games played on ...

On the characterization of models of H

We give a characterization, with respect to a large class of models of untyped λ-calculus, of those models that 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 ...

A decision procedure for satisfiability in separation logic with inductive predicates

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

Secure equilibria in weighted games

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

Weak MSO: automata and expressiveness modulo bisimilarity

We prove that the bisimulation-invariant fragment of weak monadic second-order logic (WMSO) is equivalent to the fragment of the modal μ-calculus where the application of the least fixpoint operator μp.ϕ is restricted to formulas ϕ that are continuous ...

Symmetry in concurrent games

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 bi-category of strategies on games with symmetry. Symmetry ...

Decidability of weak logics with deterministic transitive closure

The deterministic transitive closure operator, added to languages containing even only two variables, allows to express many natural properties of a binary relation, including being a linear order, a tree, a forest or a partial function. This makes it a ...

Equality and fixpoints in the calculus of structures

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

The tractability frontier of graph-like first-order query sets

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

One hierarchy spawns another: graph deconstructions and the complexity classification of conjunctive queries

We study the problem of conjunctive query evaluation relative to a class of queries; this problem is formulated here as the relational homomorphism problem relative to a class of structures A, wherein each instance must be a pair of structures such that ...

On the total variation distance of labelled Markov chains

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

System F with coercion constraints

We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...

The geometry of synchronization

We graft synchronization onto Girard's Geometry of Interaction in its most concrete form, namely token machines. This is realized by introducing proof-nets for SMLL, an extension of multiplicative linear logic with a specific construct modeling ...

On the pigeonhole and related principles in deep inference and monotone systems

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

Expressive completeness of separation logic with two variables and no separating conjunction

We show that first-order separation logic with one record field restricted to two variables and the separating implication (no separating conjunction) is as expressive as weak second-order logic, substantially sharpening a previous result. Capturing ...

A new correctness criterion for MLL proof nets

In Girard's original presentation, proof structures of Linear Logic are hypergraphs whose hyperedges are labeled by logical rules and vertices represent the connections between these logical rules. Presentations of proof structures based on interaction ...

On periodically iterated morphisms

We investigate the computational power of periodically iterated morphisms, also known as D0L systems with periodic control; we call them PerD0L systems for short. These systems give rise to a class of one-sided infinite sequences, called PerD0L words. ...

Pattern logics and auxiliary relations

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

Substitution, jumps, and algebraic effects

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

Satisfiability modulo counting: a new approach for analyzing privacy properties

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

Achieving new upper bounds for the hypergraph duality problem through logic

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

KAT + B!

It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of ...

Symmetric normalisation for intuitionistic logic

We present two proof systems for implication-only intuitionistic logic in the calculus of structures. The first is a direct adaptation of the standard sequent calculus to the deep inference setting, and we describe a procedure for cut elimination, ...

Equilibria of concurrent games on event structures

Event structures form a canonical model of concurrent behaviour which has a natural game-theoretic interpretation. This game-based interpretation was initially given for zero-sum concurrent games. This paper studies an extension of such games on event ...

Subclasses of presburger arithmetic and the weak EXP hierarchy

It is shown that for any fixed i > 0, the Σi+1-fragment of Presburger arithmetic, i.e., its restriction to i + 1 quantifier alternations beginning with an existential quantifier, is complete for ΣiEXP, the i-th level of the weak EXP hierarchy, an ...

Senescent ground tree rewrite systems

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 push-down systems, we define Senescent Ground Tree Rewrite Systems. ...

Preservation and decomposition theorems for bounded degree structures

We provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+MODm) on the class Cd of all finite structures of degree at most d: For each FO+MODm-sentence that is preserved under ...

No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete

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 *-autonomous categories. Previous work has shown the problem ...

Abstract interpretation from Büchi automata

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 it and the (infinite) lattice of languages of finite and ...

Memoryful geometry of interaction: from coalgebraic components to algebraic effects

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

Axioms and decidability for type isomorphism in the presence of sums

We consider the problem of characterizing isomorphisms of types, or, equivalently, constructive cardinality of sets, in the simultaneous presence of disjoint unions, Cartesian products, and exponentials. Mostly relying on results about polynomials with ...

Functional reactive types

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

Probably safe or live

This paper presents a formal characterisation of safety and liveness properties 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 ...

A quest for algorithmically random infinite structures

The last two decades have witnessed significant advances in the investigation of algorithmic randomness, such as Martin-Löf randomness, of infinite strings. In spite of much work, research on randomness of infinite strings has excluded the investigation ...

On the succinctness of query rewriting over shallow ontologies

We investigate the succinctness problem for conjunctive query rewritings over OWL 2QL ontologies of depth 1 and 2 by means of hypergraph programs computing Boolean functions. Both positive and negative results are obtained. We show that, over ontologies ...

Turing machines with atoms, constraint satisfaction problems, and descriptive complexity

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

Local temporal reasoning

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

On Hanf-equivalence and the number of embeddings of small induced subgraphs

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

Non-elementary complexities for branching VASS, MELL, and extensions

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

Infinite sequential games with real-valued payoffs

We investigate the existence of certain types of equilibria (Nash, ε-Nash, subgame perfect, ε-subgame perfect) in infinite sequential games with real-valued payoff functions depending on the class of payoff functions (continuous, upper semi-continuous, ...

Hyper-Ackermannian bounds for pushdown vector addition systems

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

Transition systems over games

We describe a framework for game semantics combining operational and denotational accounts. A game is a bipartite graph of "passive" and "active" positions, or a categorical variant with morphisms between positions.

The operational part of the framework ...

Compositional verification of termination-preserving refinement of concurrent programs

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

Eilenberg-MacLane spaces in homotopy type theory

Homotopy type theory is an extension of Martin-Löf 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 ...

MSO queries on trees: enumerating answers under updates

We investigate efficient view maintenance for MSO-definable queries over trees or, more precisely, efficient enumeration of answers to MSO-definable queries over words and trees which are subject to local updates. For words we exhibit an algorithm that ...

On the computing power of +, -, and ×

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

On the Hoare theory of monadic recursion schemes

The equational theory of monadic recursion schemes is known to be decidable by the result of Sénizergues on the decidability of the problem of DPDA equivalence. In order to capture some properties of the domain of computation, we augment equations with ...

Formulae-as-types for an involutive negation

Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access ...

A type theory for productive coprogramming via guarded recursion

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

Deadlock and lock freedom in the linear π-calculus

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

On context semantics and interaction nets

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. Yet, context semantics have been defined only on λ-calculus and linear logic.

In ...

Anchored LTL separation

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

Separating regular languages with first-order logic

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

Logics with counting and equivalence

We consider the two-variable fragment of first-order logic with counting, 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 ...

A functional functional interpretation

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

Compositional higher-order model checking via ω-regular games over Böhm trees

We introduce type-checking games, which are ω-regular games over Böhm 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 ...

Finite-memory strategy synthesis for robust multidimensional mean-payoff objectives

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

Faster decision of first-order graph properties

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 in prenex normal form with k variables. The trivial algorithm for this problem ...