Programme for the week
Monday, 7 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  Martin Abadi 
The Prophecy of Timely Rollback
Show abstract Techniques for rollback recovery play a central role in ensuring faulttolerance in many distributed systems. This talk addresses the formal specification and analysis of those techniques. In particular, we will discuss the relevance of prophecy variables (auxiliary program variables whose values are defined in terms of current program state and future behavior) to reasoning about systems with undo operations. We will then focus on a model for dataparallel computation with a notion of virtual time. In this model, rollbacks allow the selective undo of work at particular virtual times. A refinement theorem ensures the consistency of rollbacks. This talk is largely based on joint work with Michael Isard. 

10:00  Damiano Mazza 
Simple Parsimonious Types and Logarithmic Space
Show abstract We present a functional characterization of deterministic logspacecomputable predicates based on a variant (although not a subsystem) of propositional linear logic, which we call parsimonious logic. The resulting calculus is simplytyped and contains no primitive besides those provided by the underlying logical system, which makes it one of the simplest higherorder languages capturing logspace currently known. Completeness of the calculus uses the descriptive complexity characterization of logspace (we encode firstorder logic with deterministic closure), whereas soundness is established by executing terms on a token machine (using the geometry of interaction). 

10:30  Coffee break (Room H 3005)  
11:00  Simone Bova, Barnaby Martin 
FirstOrder Queries on Finite Abelian Groups
Show abstract We study the computational problem of checking whether a logical sentence is true in a finite abelian group. We prove that model checking firstorder sentences on finite abelian groups is fixedparameter tractable, when parameterized by the size of the sentence. We also prove that model checking monadic secondorder sentences on finite abelian groups finitely presented by integer matrices is not fixedparameter tractable (under standard assumptions in parameterized complexity). 

11:30  Anuj Dawar, Pengming Wang 
A Definability Dichotomy for Finite Valued CSPs
Show abstract Finite valued constraint satisfaction problems are a formalism for describing many natural optimisation problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Živný have recently established a complexity dichotomy for valued constraint languages. They show that each such languages either gives rise to a polynomialtime solvable optimisation problem, or to an NPhard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimisation problems in the first class are definable in fixedpoint language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexitytheoretic assumption. 

12:00  Sjoerd Cranen, Bas Luttik, Tim Willemse 
Evidence for fixpoint logic
Show abstract For many modal logics, dedicated model checkers offer diagnostics (e.g., counterexamples) that help the user understand the result provided by the solver. Fixpoint logic offers a unifying framework in which such problems can be expressed and solved, but a drawback of this framework is that it lacks comprehensive diagnostics generation. We extend the framework with a notion of evidence, which can be specialized to obtain diagnostics for various model checking problems, behavioural equivalence and refinement checking problems. We demonstrate this by showing how our notion of evidence can be used to obtain diagnostics for the problem of deciding stuttering bisimilarity. Moreover, we show that our notion generalizes the existing notions of counterexample and witness for LTL and ACTL* model checking. 

12:30  Lunch break  
14:00  Matthias Baaz, Christian Fermüller 
Elementary Elimination of Prenex Cuts in Disjunctionfree Intuitionistic Logic
Show abstract The size of shortest cutfree proofs of firstorder formulas in intuitionistic sequent calculus is known to be nonelementary in the worst case in terms of the size of given sequent proofs with cuts of the same formulas. In contrast to that fact, we provide an elementary bound for the size of cutfree proofs for disjunctionfree intuitionistic logic for the case where the cutformulas of the original proof are prenex. Moreover, we establish nonelementary lower bounds for classical disjunctionfree proofs with prenex cutformulas and intuitionistic disjunctionfree proofs with nonprenex cutformulas. 

14:30  Stefan Hetzl, Sebastian Zivota 
Tree grammars for the elimination of nonprenex cuts
Show abstract Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs with prenex Pi_1cuts in classical firstorder logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. nonprenex) cuts without quantifier alternations. The key to treating nonprenex cuts lies in using a new class of tree grammars, constraint grammars, which describe the relationship of the applicability of its productions by a propositional formula. 

15:00  Aleksy Schubert, Wil Dekkers, Henk Barendregt 
Automata Theoretic Account of Proof Search
Show abstract Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automatatheoretic model for inhabitant search, which can be viewed as proof search by the CurryHoward isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata. 

15:30  Coffee break (Room H 3005)  
16:00  Filip Mazowiecki, Cristian Riveros 
Maximal partition logic: towards a logical characterization of copyless cost register automata
Show abstract It is highly desirable for a computational model to have a logic characterization like in the seminal work from Buchi that connects MSO with finite automata. For example, weighted automata are the quantitative extension of finite automata for computing functions over words and they can be naturally characterized by a subframent of weighted logic introduced by Droste and Gastin. Recently, cost register automata (CRA) were introduced by Alur et all as an alternative model for weighted automata. In hope of finding decidable subclasses of weighted automata, they proposed to restrict their model with the socalled copyless restriction. Unfortunately, copyless CRA do not enjoy good closure properties and, therefore, a logical characterization of this class seems to be unlikely. In this paper, we introduce a new logic called maximal partition logic (MPL) for studying the expressiveness of copyless CRA. In contrast from the previous approaches (i.e. weighted logics), MPL is based on a new set of "regular" quantifiers that partition a word into maximal subwords, compute the output of a subformula over each subword separately, and then aggregate these outputs with a semiring operation. We study the expressiveness of MPL and compare it with weighted logics. Furthermore, we show that MPL is equally expressive to a natural subclass of copyless CRA. This shows the first logical characterization of copyless CRA and it gives a better understanding of the copyless restriction in weighted automata. 

16:30  Olivier Carton, Luc Dartois 
Aperiodic twoway transducers and FOtransductions
Show abstract Deterministic twoway transducers on finite words have been shown by Engelfriet and Hoogeboom to have the same expressive power as MSOtransductions. We introduce a notion of aperiodicity for these transducers and we show that aperiodic transducers correspond exactly to FOtransductions. This lifts to transducers the classical equivalence for languages between FOdefinability, recognition by aperiodic monoids and acceptance by counterfree automata. 

17:00  Orna Kupferman, Gal Vardi 
On Relative and Probabilistic Finite Counterability
Show abstract A counterexample to the satisfaction of a linear property $\psi$ in a system $\S$ is an infinite computation of $\S$ that violates $\psi$. Counterexamples are of great help in detecting design errors and in modeling methodologies such as CEGAR. When $\psi$ is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a badprefix for $\psi$: a finite word all whose extensions violate $\psi$. The existence of finite counterexamples is very helpful in practice. Liveness properties do not have badprefixes and thus do not have finite counterexamples. We extend the notion of finite counterexamples to nonsafety properties. We study counterable languages  ones that have at least one badprefix. Thus, a language is counterable iff it is not liveness. Three natural problems arise: (1) Given a language, decide whether it is counterable, (2) study the length of minimal badprefixes for counterable languages, and (3) develop algorithms for detecting badprefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACEcompleteness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a longstanding open problem. We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of badprefixes. The first adds a probabilistic component to the definition. There, a prefix is bad if almost all its extensions violate the property. The second makes it relative to the system. There, a prefix is bad if all its extensions in the system violate the property. We also study the combination of the probabilistic and relative variants. Our framework suggests new variants also of safety and liveness languages. We solve the above three problems for the different variants. Interestingly, the probabilistic variant not only increases the chances to return finite counterexamples, but also makes the solution of the three problems exponentially easier. 

17:30  Alberto Molinari, Angelo Montanari, Adriano Peron 
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Show abstract Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, pointbased temporal logics, it is still largely unexplored in the interval logic setting. Recently, a nonelementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACEhardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones. 

19:00  Welcome Reception (Room H 3005, same as the coffee breaks) 
Tuesday, 8 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  Elham Kashefi  Verification of Quantum Computing  
10:00  Samson Abramsky, Rui Soares Barbosa, Kohei Kishida, Raymond Lal, Shane Mansfield 
Contextuality, Cohomology and Paradox
Show abstract Contextuality is a key feature of quantum mechanics that provides an important nonclassical resource for quantum information and computation. Abramsky and Brandenburger used sheaf theory to give a general treatment of contextuality in quantum theory [New Journal of Physics 13 (2011) 113036]. However, contextual phenomena are found in other fields as well, for example database theory. In this paper, we shall develop this unified view of contextuality. We provide two main contributions: firstly, we expose a remarkable connection between contexuality and logical paradoxes; secondly, we show that an important class of contextuality arguments has a topological origin. More specifically, we show that "AllvsNothing" proofs of contextuality are witnessed by cohomological obstructions. 

10:30  Coffee break (Room H 3005)  
11:00  Sylvain Salvati, Igor Walukiewicz 
A model for behavioural properties of higherorder programs
Show abstract We consider simply typed lambdacalculus with fixpoints as a noninterpreted functional programming language: the result of the execution of a program is its normal form that can be seen as a potentially infinite tree of calls to builtin operations. Properties of such trees are properties of executions of programs and monadic secondorder logic (MSOL) is well suited to express them. For a given MSOL property we show how to construct a finitary model recognizing it. In other words, the value of a lambdaterm in the model determines if the tree that is the result of the execution of the term satisfies the property. The finiteness of the construction has as consequences many known results about the verification of higherorder programs in this framework. 

11:30  Lorenzo Clemente, Sławomir Lasota 
Reachability analysis of firstorder definable pushdown systems
Show abstract We study pushdown systems where control states, stack alphabet, and transition relation, instead of being finite, are firstorder definable in a fixed countablyinfinite structure. We show that the reachability analysis can be addressed with the wellknown saturation technique for the wide class of oligomorphic structures. Moreover, for the more restrictive homogeneous structures, we are able to give concrete complexity upper bounds. We show ample applicability of our technique by presenting several concrete examples of homogeneous structures, subsuming, with optimal complexity, known results from the literature. We show that infinitely many such examples of homogeneous structures can be obtained with the classical wreath product construction. 

12:00  Charles Grellois, PaulAndré Melliès 
Relational Semantics of Linear Logic and Higherorder Model Checking
Show abstract In this article, we develop a new and somewhat unexpected connection between higherorder modelchecking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higherorder recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion scheme. We show how to extend this result to alternating parity automata (APT) by introducing a parametric version of the exponential modality of linear logic, capturing the formal properties of colors (or priorities) in higherorder modelchecking. We show in particular how to reunderstand in this way the typetheoretic approach to higherorder modelchecking developed by Kobayashi and Ong. We briefly explain in the end of the paper how this analysis driven by linear logic results in a new and purely semantic proof of decidability of the formulas of the monadic secondorder logic for higherorder recursion schemes. 

12:30  Lunch break  
14:00  Juha Kontinen, JulianSteffen Müller, Henning Schnoor, Heribert Vollmer 
A Van Benthem Theorem for Modal Team Semantics
Show abstract The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of firstorder logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic (MDL) and team semantics. We show that Modal Team Logic (MTL) extending MDL by classical negation captures exactly the FOdefinable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area. 

14:30  Katsuhiko Sano, Jonni Virtema 
Axiomatizing Propositional Dependence Logics
Show abstract We give sound and complete Hilbertstyle axiomatizations for propositional dependence logic (PD), modal dependence logic (MDL), and extended modal dependence logic (EMDL) by extending existing axiomatizations for propositional logic and modal logic. In addition, we give novel labeled tableau calculi for PD, MDL, and EMDL. We prove soundness, completeness and termination for each of the labeled calculi. 

15:00  Thomas Schwentick, Nils Vortmeier, Thomas Zeume 
Static Analysis for LogicBased Dynamic Programs
Show abstract The goal of dynamic programs as introduced by Patnaik and Immerman (1994) is to maintain the result of a fixed query for an input database which is subject to tuple insertions and deletions. To this end such programs store an auxiliary database whose relations are updated via firstorder formulas upon modifications of the input database. One of those auxiliary relations is supposed to store the answer to the query. Several static analysis problems can be associated to such dynamic programs. Is the answer relation of a given dynamic program always empty? Does a program actually maintain a query? That is, is the answer given of the program the same when an input database was reached by two different modification sequences? Even more, is the content of auxiliary relations independent of the modification sequence that lead to an input database? We study the algorithmic properties of those and similar static analysis problems. Since all these problems can easily be seen to be undecidable for full firstorder programs, we examine the exact borderline for decidability for restricted programs. Our focus is on restricting the arity of the input databases as well as the auxiliary databases, and to restrict the use of quantifiers. 

15:30  Coffee break (Room H 3005)  
16:00  James Brotherston, Jules Villard 
SubClassical Boolean Bunched Logics and the Meaning of Par
Show abstract We investigate intermediate logics between the bunched logics Boolean BI and Classical BI, obtained by combining classical propositional logic with various flavours of Hyland and De Paiva's full intuitionistic linear logic. Thus, in addition to the usual multiplicative conjunction (with its adjoint implication and unit), our logics also feature a multiplicative disjunction (with its adjoint coimplication and unit). The multiplicatives behave "subclassically", in that disjunction and conjunction are related by a weak distribution principle, rather than by De Morgan equivalence. We formulate a Kripke semantics, covering all our subclassical bunched logics, in which the multiplicatives are naturally read in terms of resource operations. Our main theoretical result is that validity according to this semantics coincides with provability in a corresponding Hilbertstyle proof system. Our logical investigation sheds considerable new light on how one can understand the multiplicative disjunction, better known as linear logic's "par", in terms of resource operations. In particular, and in contrast to the earlier Classical BI, the models of our logics include the heaplike memory models of separation logic, in which disjunction can be interpreted as a property of intersection operations over heaps. 

16:30  Stefano Berardi 
Classical and Intuitionistic WellFoundness are Equivalent
Show abstract Assume that we may prove in Classical Functional Analysis that a primitive recursive relation $R$ is wellfounded, using the inductive definition of wellfounded. In this paper we prove that such a proof of wellfoundation may be made intuitionistic. We conclude that if we are able to formulate any mathematical problem as the inductive wellfoundation of some primitive recursive relation, then intuitionistic and classical provability coincide, and for such a statement of wellfoundation we may always find an intuitionistic proof if we may find a proof at all. The core of intuitionism are the methods for computing out data with given properties from input data with given properties: these are the results we are looking for when we do constructive mathematics. Proving that a primitive recursive relation R is inductively wellfounded is a more abstract kind of result, but it is crucial as well, because once we proved that R is inductively wellfounded, then we may write programs by induction over R. This is the way inductive relation are currently used in intuitionism and in proof assistants based on intuitionism, like Coq. In the paper we introduce the comprehension axiom for Functional Analysis in the form of introduction and elimination rules for predicates of types Prop, Nat>Prop, ..., in order to use Girard's method of candidates for impredicative arithmetic. 

17:00  Paolo Capriotti, Nicolai Kraus, Andrea Vezzosi 
Functions out of Higher Truncations
Show abstract In homotopy type theory, the truncation operator n (for a number n greater or equal to 1) is often useful if one does not care about the higher structure of a type and wants to avoid coherence problems. However, its elimination principle only allows to eliminate into ntypes, which makes it hard to construct functions An > B if B is not an ntype. This makes it desirable to derive more powerful elimination theorems. We show a first general result: If B is an (n+1)type, then functions An > B correspond exactly to functions A > B that are constant on all (n+1)st loop spaces. We give one "elementary" proof and one proof that uses a higher inductive type, both of which require some effort. As a sample application of our result, we show that we can construct "setbased" representations of 1types, as long as they have "braided" loop spaces. The main result with one of its proofs and the application have been formalised in Agda. 

17:30  Murdoch Gabbay, Dan Ghica, Daniela Petrisan 
Leaving the Nest: Nominal techniques for variables with interleaving scopes
Show abstract We examine the key syntactic and semantic aspects of a nominal framework allowing scopes of name bindings to be arbitrarily interleaved. Name binding (e.g. λx.M) is handled by explicit namecreation and namedestruction brackets (e.g. ⟨x M x⟩) which admit interleaving. We define an appropriate notion of alphaequivalence for such a language and study the syntactic structure required for alphaequivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics. 

20:00  Annual Meeting of the EACSL 
Wednesday, 9 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  Ryan Williams 
Thinking Algorithmically About Impossibility
Show abstract Complexity lower bounds like P != NP assert impossibility results for all possible programs of some restricted form. As there are presently enormous gaps in our lower bound knowledge, a central question on the minds of today's complexity theorists is how will we find better ways to reason about all efficient programs? I argue that some progress can be made by (very deliberately) thinking algorithmically about lower bounds. Slightly more precisely, to prove a lower bound against some class C of programs, we can start by treating C as a set of inputs to another (larger) process, which is intended to perform some basic analysis of programs in C. By carefully studying the algorithmic "metaanalysis" of programs in C, we can learn more about the limitations of the programs being analyzed. This essay is mostly selfcontained; scant knowledge is assumed of the reader. 

10:00  Erich Grädel, Wied Pakusa 
Rank logic is dead, long live rank logic!
Show abstract Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixedpoint logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power. In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR. One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers. 

10:30  Coffee break (Room H 3005)  
11:00  Adria Gascon, Manfred SchmidtSchauss, Ashish Tiwari 
TwoRestricted One Context Unification is in Polynomial Time
Show abstract One Context Unification (1CU) extends firstorder unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several moregeneral classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of firstorder unification and can be used to solve related problems in polynomial time, such as firstorder unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs. 

11:30  Jiaxiang Liu, JeanPierre Jouannaud, Mizuhito Ogawa 
Confluence of layered rewrite systems
Show abstract We investigate a new, Turingcomplete class of layered systems, whose linearized lefthand sides of rules can only be overlapped at the root position. Layered systems define a natural notion of rank for terms: the maximal number of redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be nonterminating, nonleftlinear, or nonright linear. Using a novel unification technique, cyclic unification, we show that rank nonincreasing layered systems are confluent provided their cyclic critical pairs have cyclicjoinable decreasing diagrams. 

12:00  Ackermann Award Ceremony  
13:00  Lunch break  
14:00  Lukasz Kaiser, Martin Lang, Simon Leßenich, Christof Löding 
A unified approach to boundedness properties in MSO
Show abstract In the past years, extensions of monadic secondorder logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resourceautomatic structures. 

14:30  Karoliina Lehtinen, Sandra Quickert 
Constructive decidability of the first levels of the modal mu alternation hierarchy
Show abstract We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blowup incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed subexponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula. 

15:00  Dietrich Kuske, Jiamou Liu, Anastasia Moskvina 
Infinite and Biinfinite Words with Decidable Monadic Theories
Show abstract We study word structures of the form $(D,<,P)$ where $D$ is either $\N$ or $\Z$, $<$ is a linear ordering on $D$ and $P\subseteq D$ is a predicate on $D$. In particular we show:
Through these results we demonstrate similarities and differences between logical properties of infinite and biinfinite words. 

15:30  The busses for the excursion leave in front of the main building  
16:00  Excursion to Potsdam  
19:30  Conference Dinner 
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:
