Rank logic is dead, long live rank logic!
Erich Grädel and Wied Pakusa.
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.
Constructive decidability of the first levels of the modal mu alternation hierarchy
Karoliina Lehtinen and Sandra Quickert.
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.
Reachability analysis of firstorder definable pushdown systems
Lorenzo Clemente and Sławomir Lasota.
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.
FiniteDegree Predicates and TwoVariable FirstOrder Logic
Charles Paperman.
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.
A Coalgebraic Decision Procedure for WS1S
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.
Binding Forms in FirstOrder Logic
Fabio Mogavero and Giuseppe Perelli.
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.
Elementary Elimination of Prenex Cuts in Disjunctionfree Intuitionistic Logic
Matthias Baaz and Christian Fermüller.
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.
Aperiodic twoway transducers and FOtransductions
Olivier Carton and Luc Dartois.
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.
Automata Theoretic Account of Proof Search
Aleksy Schubert, Wil Dekkers and Henk Barendregt.
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.
Tree grammars for the elimination of nonprenex cuts
Stefan Hetzl and Sebastian Zivota.
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.
Axiomatizing Propositional Dependence Logics
Katsuhiko Sano and Jonni Virtema.
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.
Evidence for fixpoint logic
Sjoerd Cranen, Bas Luttik and Tim Willemse.
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.
Classical and Intuitionistic WellFoundness are Equivalent
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.
What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead
Felix Klein and Martin Zimmermann.
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.
A Van Benthem Theorem for Modal Team Semantics
Juha Kontinen, JulianSteffen Müller, Henning Schnoor and Heribert Vollmer.
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.
Infinite and Biinfinite Words with Decidable Monadic Theories
Dietrich Kuske, Jiamou Liu and Anastasia Moskvina.
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:
(a) The set of recursive $\omega$words with decidable monadic second order theories is $\Sigma_3$complete.
(b) We characterise those sets $P\subseteq\Z$ that yield biinfinite words $(\Z,\le,P)$ with decidable monadic second order theories.
(c) We show that such "tame" predicates $P$ exist in every Turing degree.
(d) We determine, for $P\subseteq\Z$, the number of predicates $Q\subseteq\Z$ such that $(\Z,\le,P)$ and $(\Z,\le,Q)$ are indistinguishable.
Through these results we demonstrate similarities and differences between logical properties of infinite and biinfinite words.
A unified approach to boundedness properties in MSO
Lukasz Kaiser, Martin Lang, Simon Leßenich and Christof Löding.
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.
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives
Alberto Molinari, Angelo Montanari and Adriano Peron.
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.
A Definability Dichotomy for Finite Valued CSPs
Anuj Dawar and Pengming Wang.
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.
Functions out of Higher Truncations
Paolo Capriotti, Nicolai Kraus and Andrea Vezzosi.
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.
Static Analysis for LogicBased Dynamic Programs
Thomas Schwentick, Nils Vortmeier and Thomas Zeume.
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.
Confluence of layered rewrite systems
Jiaxiang Liu, JeanPierre Jouannaud and Mizuhito Ogawa.
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.
Leaving the Nest: Nominal techniques for variables with interleaving scopes
Murdoch Gabbay, Dan Ghica and Daniela Petrisan.
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.
On Classical PCF, Linear Logic and the MIX rule
Thomas Ehrhard and Shahin Amini.
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).
On Relative and Probabilistic Finite Counterability
Orna Kupferman and Gal Vardi.
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.
Uniform OneDimensional Fragments with One Equivalence Relation
Emanuel Kieronski and Antti Kuusisto.
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.
Weak Subgame Perfect Equilibria and their Application to Quantitative Reachability
Thomas Brihaye, Véronique Bruyère, Noémie Meunier and JeanFrancois Raskin.
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.
Simple Parsimonious Types and Logarithmic Space
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).
Contextuality, Cohomology and Paradox
Samson Abramsky, Rui Soares Barbosa, Kohei Kishida, Ray Lal and Shane Mansfield.
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.
FirstOrder Queries on Finite Abelian Groups
Simone Bova and Barnaby Martin.
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).
SubClassical Boolean Bunched Logics and the Meaning of Par
James Brotherston and Jules Villard.
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.
Least and Greatest Fixed Points in Ludics
David Baelde, Amina Doumane and Alexis Saurin.
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).
Twovariable Logic with Counting and a Linear Order
Witold Charatonik and Piotr Witkowski.
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.
Maximal partition logic: towards a logical characterization of copyless cost register automata
Filip Mazowiecki and Cristian Riveros.
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.
A model for behavioural properties of higherorder programs
Sylvain Salvati and Igor Walukiewicz.
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.
On Unambiguous Regular Tree Languages of Index $(0,2)$
Jacques Duparc, Kevin Fournier and Szczepan Hummel.
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:

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

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}$.
Modelling Coeffects in the Relational Semantics of Linear Logic
Michele Pagani and Flavien Breuvart.
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.
Tensorial logic with colours and higherorder model checking
Charles Grellois and PaulAndré Melliès.
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.
TwoRestricted One Context Unification is in Polynomial Time
Adria Gascon, Manfred SchmidtSchauss and Ashish Tiwari.
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.