Thursday, 10 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  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 secondorder 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 nonelementary. Typically, decision procedures for WS1S exploit the logicautomaton 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, JeanFrancois Raskin 
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability
Show abstract We study nplayer turnbased 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 wellknown notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE wellsuited 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 finitememory 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, infiniteduration twoplayer 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 evolutionindependent, 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 omegaregular and omegacontextfree winning conditions. 

12:00  Fabio Mogavero, Giuseppe Perelli 
Binding Forms in FirstOrder 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 firstorder 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 firstorder limitations proposed in the literature, as the guarded and unary negation fragments. We also prove, via a novel modeltheoretic technique, that our logic enjoys the finitemodel property, Craig's interpolation, and Beth's definability. Furthermore, the associated modelchecking and satisfiability problems are solvable in PTime and Sigma_3^P, respectively. 

12:30  Lunch break  
14:00  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 CurryHoward correspondence, to study computation over inductive and coinductive data. The logic muMALL 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 muMALL 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 muMALL 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 muMALL). 

14:30  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 semiring, 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 semiring, 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 semiring 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 nonidempotents 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 nondeterminism; 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 OneDimensional Fragments with One Equivalence Relation
Show abstract The uniform onedimensional fragment U1 of firstorder logic was introduced recently as a natural generalization of the twovariable fragment FO2 to contexts with relation symbols of all arities. It was shown that U1 has the exponential model property and NEXPTIMEcomplete 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 onedimensional fragments. We introduce EhrenfeuchtFraisse 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 builtin equivalence relation E. We prove that while all the obtained systems retain the finite model property, their complexities differ. Namely, the satisfiability problem is NEXPTIMEcomplete for SU1(E) and 2NEXPTIMEcomplete for both RU1(E) and U1(E). Finally, we show undecidability of some natural extensions of SU1. 

16:30  Charles Paperman 
FiniteDegree Predicates and TwoVariable FirstOrder Logic
Show abstract We consider twovariable firstorder 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 finitedegree predicates are also definable with the order predicate only. From this result we derive the separation of the alternation hierarchy of twovariable logic on this signature. Replacing finitedegree 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 
Twovariable Logic with Counting and a Linear Order
Show abstract We study the finite satisfiability problem for the twovariable fragment of the firstorder 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 NEXPTIMEcomplete, 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:
