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 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 ...
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 ...
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 ...
Report of the Jury for the 2014 Ackermann Award.
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.
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 ...
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 ...
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 ...
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., ...
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 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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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. ...
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 ...
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. ...
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 ...
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 ...
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 ...
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, ...
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 ...
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 ...
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. ...
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 ...
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 ...
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 ...
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 ...
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 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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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, ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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 ...
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-...
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 ...
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 ...
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 ...
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 ...
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 ...