Computer Science Logic 2015
Berlin, 7-10 September 2015
Technische Universität Berlin

Thursday, 10 September 2015

9:00 Markus Lohrey
Markus Lohrey
Temporal logics with local constraints
Show abstract

Recent decidability results on the satisfiability problem for temporal logics, in particular LTL, CTL* and ECTL*, with constraints over external structures like the integers with the order or infinite trees are surveyed in this paper.

10:00 Dmitriy Traytel A Coalgebraic Decision Procedure for WS1S
Show abstract

Weak monadic second-order logic of one successor (WS1S) is a simple and natural formalism to specify regular properties. WS1S is decidable, although the decision procedure's complexity is non-elementary. Typically, decision procedures for WS1S exploit the logic-automaton connection, i.e. they escape the simple and natural formalism by translating formulas into equally expressive regular structures such as finite automata, regular expressions, or games. In this work, we devise a coalgebraic decision procedure for WS1S that stays within the logical world by directly operating on formulas. The key operation is the derivative of a formula, modeled after Brzozowski's derivatives of regular expressions. The presented decision procedure has been formalized and proved correct in the interactive proof assistant Isabelle.

10:30 Coffee break (Room H 3005)
11:00 Thomas Brihaye, Véronique Bruyère, Noémie Meunier, Jean-Francois Raskin
Thomas Brihaye, Véronique Bruyère, Noémie Meunier, Jean-Francois Raskin
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability
Show abstract

We study n-player turn-based games played on a finite directed graph. For each play, the players have to pay a cost that they want to minimize. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. We also study natural variants of SPE, named weak (resp. very weak) SPE, where players who deviate cannot use the full class of strategies but only a subclass with a finite number of (resp. a unique) deviation step(s).

Our results are threefold. Firstly, we characterize in the form of a Folk theorem the set of all plays that are the outcome of a weak SPE. Secondly, for the class of quantitative reachability games, we prove the existence of a finite-memory SPE and provide an algorithm for computing it (only existence was known with no information regarding the memory). Moreover, we show that the existence of a constrained SPE, i.e. an SPE such that each player pays a cost less than a given constant, can be decided. The proofs rely on our Folk theorem for weak SPEs (which coincide with SPEs in the case of quantitative reachability games) and on the decidability of MSO logic on infinite words. Finally with similar techniques, we provide a second general class of games for which the existence of a (constrained) weak SPE is decidable.

11:30 Felix Klein, Martin Zimmermann What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
Show abstract

We investigate determinacy of delay games with Borel winning conditions, infinite-duration two-player games in which one player may delay her moves to obtain a lookahead on her opponent's moves.

First, we prove determinacy of such games with respect to a fixed evolution of the lookahead. However, strategies in such games may depend on information about the evolution. Thus, we introduce different notions of universal strategies for both players, which are evolution-independent, and determine the exact amount of information a universal strategy needs about the history of a play and the evolution of the lookahead to be winning. In particular, we show that delay games with Borel winning conditions are determined with respect to universal strategies. Finally, we consider decidability problems, e.g., "Does a player have a universal winning strategy for delay games with a given winning condition?", for omega-regular and omega-context-free winning conditions.

12:00 Fabio Mogavero, Giuseppe Perelli Binding Forms in First-Order Logic
Show abstract

Aiming to pinpoint the reasons behind the decidability of some complex extensions of modal logic, we propose a new classification criterion for sentences of first-order logic, which is based on the kind of binding forms admitted in their expressions, i.e., on the way the arguments of a relation can be bound to a variable. In particular, we describe a hierarchy of four fragments focused on the Boolean combinations of these forms, showing that the less expressive one is already incomparable with several first-order limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel model-theoretic technique, that our logic enjoys the finite-model property, Craig's interpolation, and Beth's definability. Furthermore, the associated model-checking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively.

12:30 Lunch break
14:00 David Baelde, Amina Doumane, Alexis Saurin
David Baelde, Amina Doumane, Alexis Saurin
Least and Greatest Fixed Points in Ludics
Show abstract

Various logics have been introduced in order to reason over (co)inductive specifications and, through the Curry-Howard correspondence, to study computation over inductive and coinductive data. The logic mu-MALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.

In this paper, we investigate the semantics of mu-MALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.

We provide mu-MALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in mu-MALL).

14:30 Michele Pagani, Flavien Breuvart
Michele Pagani, Flavien Breuvart
Modelling Coeffects in the Relational Semantics of Linear Logic
Show abstract

Various typing system have been recently introduced giving a parametric version of the exponential modality of linear logic, e.g. \cite{GhicaS14,BrunelGMZ14}. The parameters are taken from a semi-ring, and allow to express coeffects -- i.e. specific requirements of a program with respect to the environment (availability of a resource, some prerequisite of the input, etc.).

We show that all these systems can be interpreted in the relational category (\Rel) of sets and relations. This is possible because of the notion of multiplicity semi-ring, introduced in \cite{CarraroES10} and allowing a great variety of exponential comonads in \Rel. The interpretation of a particular typing system corresponds then to give a suitable notion of stratification of the exponential comonad associated with the semi-ring parametrising the exponential modality.

15:00 Thomas Ehrhard, Shahin Amini On Classical PCF, Linear Logic and the MIX rule
Show abstract

We study a classical version of PCF from a semantical point of view. We define a general notion of model based on categorical models of Linear Logic, in the spirit of earlier work by Girard, Regnier and Laurent. We give a concrete example based on the relational model of Linear Logic, that we present as a non-idempotents intersection type system, and we prove an Adequacy Theorem using ideas introduced by Krivine. Following Danos and Krivine, we also consider an extension of this language with a MIX construction introducing a form of must non-determinism; in this language, a program of type integer can have more than one value (or no value at all, raising an error). We propose a refinement of the relational model of classical PCF in which programs of type integer are single valued; this model rejects the MIX syntactical constructs (and the MIX rule of Linear Logic).

15:30 Coffee break (Room H 3005)
16:00 Emanuel Kieronski, Antti Kuusisto Uniform One-Dimensional Fragments with One Equivalence Relation
Show abstract

The uniform one-dimensional fragment U1 of first-order logic was introduced recently as a natural generalization of the two-variable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIME-complete satisfiability problem. In this paper we investigate two restrictions of U1 that still contain FO2. We call these logics RU1 and SU1, or the restricted and strongly restricted uniform one-dimensional fragments. We introduce Ehrenfeucht-Fraisse games for the logics and prove that while SU1 and RU1 are expressively equivalent, they are strictly contained in U1. Furthermore, we consider extensions of the logics SU1, RU1 and U1 with unrestricted use of a single built-in equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIME-complete for SU1(E) and 2NEXPTIME-complete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1.

16:30 Charles Paperman
Charles Paperman
Finite-Degree Predicates and Two-Variable First-Order Logic
Show abstract

We consider two-variable first-order logic on finite words with a fixed number of quantifier alternations. We show that all languages with a neutral letter definable using the order and finite-degree predicates are also definable with the order predicate only. From this result we derive the separation of the alternation hierarchy of two-variable logic on this signature. Replacing finite-degree by arbitrary numerical predicates in the statement would entail a long standing conjecture on the circuit complexity of the addition function. Thus, this result can be viewed as a uniform version of this circuit lower bound.

17:00 Witold Charatonik, Piotr Witkowski
Witold Charatonik, Piotr Witkowski
Two-variable Logic with Counting and a Linear Order
Show abstract

We study the finite satisfiability problem for the two-variable fragment of the first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of two linear orders (in presence of two other binary symbols). In the case of one linear order it is NEXPTIME-complete, even in presence of the successor relation. Surprisingly, the complexity of the problem explodes when we add one binary symbol more: C2 with one linear order and its successor, in presence of other binary predicate symbols, is decidable, but it is as expressive (and as complex) as Vector Addition Systems.

17:30 Jacques Duparc, Kevin Fournier, Szczepan Hummel On Unambiguous Regular Tree Languages of Index (0,2)
Show abstract

We investigate the infinite tree languages recognized by unambiguous parity automata whose priorities range from 0 to 2. We show that they are topologically far more involved than the deterministic ones. We do so by providing operations that generate a family $(A_{\alpha})_{\alpha<\varphi_2(0)}$ of unambiguous automata such that:

  1. it respects the strict Wadge ordering: $\alpha<\beta$ if and only if $A{\alpha}<_W A_{\beta}$.

  2. Its length ($\varphi_2(0)$) is the first fixpoint of the ordinal function that itself enumerates all fixpoints of the ordinal exponentiation $x\mapsto \omega^{x}$.