ABSTRACT. Abstract—Regular cost functions offer a toolbox for automatically solving problems of existence of bounds, in a way similar to the theory of regular languages. More precisely, it allows to test the existence of bounds for quantities that can be defined in cost monadic second-order logic (a quantitative variant of monadic second-order logic) with inputs that range over finite words, infinite words, finite trees, and (sometimes) infinite trees.

Though the initial results date from the works of Hashiguchi in the early eighties, it is during the last decade that the theory took its current shape and that many new results and applications have been established.

In this tutorial, two connections linking logic with the theory of regular cost functions will be described. The first connection is a proof of a result of Blumensath, Otto and Weyer stating that it is decidable whether the fixpoint of a monadic second-order formula is reached within a bounded number of iterations over the class of infinite trees. The second connection is how non-standard models (and more precisely non-standard analysis) give rise to a unification of the theory of regular cost functions with the one of regular languages.

ABSTRACT. Decidability of the determinization problem for weighted automata over the semiring (Z ∪ {−∞}, max, +), WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N and for all words α in the language of N, the accepting run of D on α is always at most k-away from a maximal accepting run of N on α. That is, along all prefixes of the same length, the absolute difference between the running sums of weights of the two runs is at most k. A WA N is r-regret determinizable if for all words α in its language, its non-determinism can be resolved on the fly to construct a run of N such that the absolute difference between its value and the value assigned to α by N is at most r.

We show that a WA is determinizable if and only if it is k-delay determinizable for some k. Hence deciding the existence of some k is as difficult as the general determinization problem. When k and r are given as input, the k-delay and r-regret determinization problems are shown to be EXPTIME-complete. We also show that determining whether a WA is r-regret determinizable for some r is in EXPTIME.

ABSTRACT. We study 2-player turn-based perfect-information stochastic games with countably infinite state space. The players aim at maximizing/minimizing the probability of a given event (i.e., measurable set of infinite plays), such as reachability, Buchi, ω-regular or more general objectives.

These games are known to be weakly determined, i.e., they have value. However, strong determinacy of quantitative objectives (given by an event E and a threshold c in [0,1]) was open in many cases: is it always the case that the maximizer or the minimizer has a winning strategy, i.e., one that enforces, against all strategies of the other player, that E is satisfied with probability >=c (resp.

We show that almost-sure objectives (where c=1) are strongly determined. This vastly generalizes a previous result on finite games with almost-sure tail objectives. On the other hand we show that >= 1/2 (co-)Buchi objectives are not strongly determined, not even if the game is finitely branching.

Moreover, for almost-sure reachability and almost-sure Buchi objectives in finitely branching games, we strengthen strong determinacy by showing that one of the players must have a memoryless deterministic (MD) winning strategy.

ABSTRACT. We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi-dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary.

ABSTRACT. This paper deals with the construction of shift-invariant maximal filters on $\mathbb{Z}$ and their relation to hormonal cellular automata, a generalization of the cellular automata computation model with some information about the global state shared among all the cells.

We first design shift-invariant maximal filters in order to define this new model of computation. Starting from different assumptions, we show how to construct such filters, and analyze the computation power of the induced cellular automata computation model.

ABSTRACT. We consider a declarative framework for machine learning where concepts and hypotheses are defined by formulas of a logic over some background structure. We show that within this framework, concepts defined by first-order formulas over a background structure of at most polylogarithmic degree can be learned in polylogarithmic time in the "probably approximately correct" learning sense.

ABSTRACT. The evaluation of conjunctive regular path queries -- which form the navigational core of the query languages for graph databases -- raises challenges in the context of the homomorphism problem that are not fully addressed by existing techniques. We start a systematic investigation of such challenges using a notion of homomorphism for regular graph patterns (RGPs). We observe that the RGP homomorphism problem cannot be reduced to known instances of the homomorphism problem, and new techniques need to be developed for its study.

We first show that the non-uniform version of the problem is computationally harder than for the usual homomorphism problem. By establishing a connection between both problems, in turn, we postulate a dichotomy conjecture, analogous to the algebraic dichotomy conjecture held in CSP. We also look at which structural restrictions on left-hand side instances of the RGP homomorphism problem ensure efficiency. We study restrictions based on the notion of bounded treewidth modulo equivalence, which characterizes tractability for the usual homomorphism notion. We propose two such notions, based on different interpretations of RGP equivalence, and show that they both ensure the efficiency of the RGP homomorphism problem.

ABSTRACT. We introduce the logic FOCN(P) which extends first-order logic by counting and by numerical predicates from a set P, and which can be viewed as a natural generalisation of various counting logics that have been studied in the literature.

We obtain a locality result showing that every FOCN(P)-formula can be transformed into a formula in Hanf normal form that is equivalent on all finite structures of degree at most d. A formula is in Hanf normal form if it is a Boolean combination of formulas describing the neighbourhood around its tuple of free variables and arithmetic sentences with predicates from P over atomic statements describing the number of realisations of a type with a single center. The transformation into Hanf normal form can be achieved in time elementary in d and the size of the input formula.

From this locality result, we infer the following applications: (1) The Hanf-locality rank of first-order formulas of bounded quantifier alternation depth only grows polynomially with the formula size. (2) The model checking problem for the fragment FOC(P) of FOCN(P) on structures of bounded degree is fixed parameter tractable (with elementary parameter dependence). (3) The query evaluation problem for fixed FOC(P)-queries over fully dynamic databases of degree at most d can be solved efficiently: there is a dynamic algorithm that can enumerate the tuples in the query result with constant delay, and that allows to compute the size of the query result and to test if a given tuple belongs to the query result within constant time after every database update.

ABSTRACT. Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential k-pebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: - Isomorphism in the coKleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. - The key notion of core is axiomatized, and a k-pebble version is formulated. - The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. - CoKleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Furer-Immerman construction.

These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation.

ABSTRACT. We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in the linear theory of the reals. We give a new and simpler proof of this result and at the same time stengthen its formulation, showing that the reachability relation can be expressed by a Boolean combination of difference constraints. We show that the resulting formula has size singly exponential in the size of the timed automaton. As a corollary we derive NEXPTIME-completeness of the model checking problem for the fragment of parametric TCTL generated by the EF modality.

ABSTRACT. We prove that emptiness of timed register pushdown automata is decidable in doubly exponential time. This is a very expressive class of automata, whose transitions may involve state and top-of-stack clocks with unbounded differences. It strictly subsumes pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed register pushdown automata of Clemente and Lasota. Along the way, we prove two further decidability results of independent interest: for emptiness of least solutions to systems of equations over sets of integers with addition, union and intersections with N and -N, and for reachability in one-dimensional branching vector addition systems with states and subtraction, both in exponential time.

ABSTRACT. We introduce geometric consideration into the theory of formal languages. We aim to shed light on our understanding of global patterns that occur on infinite strings. We utilize methods of geometric group theory. Our emphasis is on large scale geometries. Two infinite strings have the same large scale geometry if there are color preserving bi-Lipschitz maps with distortions between the strings. Call these maps quasi-isometries. Introduction of large scale geometriesposes several questions. The first question asks to study the partial order induced by quasi-isometries. This partial order compares large scale geometries; as such it presentsan algebraic tool for classification of global patterns. We prove there is a greatest large scale geometry and infinitely many minimal large scale geometries. The second question is related to understanding the quasi-isometric maps on various classes of strings. The third question investigates the sets of large scale geometries of strings accepted by computational models, e.g. Buchi automata. We provide an algorithm that describes large scale geometries of strings accepted by Buchi automata. This links large scale geometries with automata theory. The fourth question studies the complexity of the quasi-isometry problem. We show the problem is Sigma-03-complete thus providing a bridge with computability theory. Finally, the fifth question asks to build algebraic structures that are invariants of large scale geometries. We invoke asymptotic cones, a key concept in geometric group theory, dedined via model-theoretic notion of ultra-product. Partly, we study asymptotic cones of algorithmically random strings thus connecting the topic with algorithmic randomness and model theory.

ABSTRACT. We introduce an extension of Strategy Logic for the imperfect-information setting, called SLi, and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, the problem turns out to be undecidable. We introduce a syntactical class of “hierarchical instances” for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model. We prove that model-checking SLi restricted to hierarchical instances is decidable. This result, because it allows for complex patterns of existential and universal quantification on strategies, greatly generalises previous ones, such as decidability of multiplayer games with imperfect information and hierarchical observations, and decidability of distributed synthesis for hierarchical systems.

To establish the decidability result, we introduce and study QCTLi, an extension of QCTL (itself an extension of CTL with second-order quantification over atomic propositions) by parameterising its quantifiers with observations. The simple syntax of QCTLi allows us to provide a conceptually neat reduction of SLi to QCTLi that separates concerns, allowing one to forget about strategies and agents and focus solely on second-order quantification. While the model-checking problem of QCTLi is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable. The decidability result for SLi follows since the reduction maps hierarchical instances of SLi to hierarchical formulas of QCTLi.

ABSTRACT. In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called *projective*. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity.

ABSTRACT. A structure enjoys the Herbrand property if, whenever it satisfies an equality between terms, all these terms are unifiable. The expressive power of equalities is, thus, trivialized, as their satisfiability is reduced to a purely-syntactic check.

In this paper, we introduce the concept of Herbrand property and study its consequences on both a finite-model theoretic and a structural-complexity theoretic level.

We first show that the Herbrand property can be implemented in the finite, by what we call quasi-Herbrand models. In particular, this result holds in presence of functions in the vocabulary, in stark contrast to the naive implementation of the property via Herbrand models, showing that the intrinsic infinity of Herbrand universes is somehow inessential. Finite quasi-Herbrand models allow to prove the finite-model property and a decidable finite-satisfiability problem for previously unsettled fragments of first-order logic, where known techniques fail, was it only for the presence of functions in the vocabulary.

We then use the Herbrand property to establish computational-complexity results. We obtain, indeed, tight bounds for satisfiability and entailment problems for several fragments of first-order logic. Most prominently, we show that the entailment problem for quantified conjunctive positive relational logic, also known as the quantified conjunctive query containment problem, is in \NPTime. This amounts to a remarkable result both from a logical perspective, boiling down to a generalization of the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (due to Chandra and Merlin, STOC'77), and from a complexity, even algorithmic, perspective, tightening to \NPTime the known 3\ExpTime upper bound (due to Chen, Madelaine, and Martin, LICS'08).

ABSTRACT. The algebra of binary relations provides union and composition as basic operators, with the empty set as neutral element for union and the identity relation as neutral element for composition. The basic algebra can be enriched with additional features. We consider the diversity relation, the full relation, intersection, set difference, projection, coprojection, and transitive closure. It is customary to express boolean queries on binary relational structures as finite sets of quasi-equations (finite conjunctions of containments). We investigate which features are primitive in this setting, in the sense that omitting the feature would allow strictly less boolean queries to be expressible. Our main result is that, modulo a finite list of elementary interdependencies among the features, every feature is indeed primitive.

ABSTRACT. First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB_0, and the *finite-degree* predicates: FO[Arb] = FO[<, MSB_0, Fin].

The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[Arb] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[<, Fin] and FO[<, MSB_0]. Thus FO[<, Fin] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[Arb]. Some applications to counting are presented.

ABSTRACT. We present new data structures for quasistrict higher categories, in which associativity and unit laws hold strictly. Our approach has low axiomatic complexity compared to traditional algebraic definitions of higher categories, and we use it to give a practical definition of quasistrict 4-category. This definition is amenable to computer implementation, and we use it to give a new machine-verified algebraic proof that every adjunction of 1-cells in a quasistrict 4-category can be promoted to a coherent adjunction satisfying the butterfly equations.

ABSTRACT. Nonuniform (or "nested" or "heterogeneous") datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)recursion and (co)induction principles based on a weak variant of parametricity.

ABSTRACT. We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations.

ABSTRACT. We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $\lambda$-calculi with algebraic effects. We first of all introduce a computational lambda-calculus, and endow it with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which the obtained notion of applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract.

ABSTRACT. We present fully abstract encodings of the call-by-name lambda-calculus into HOcore, a minimal higher-order process calculus with no name restriction. We consider several equivalences on the lambda-calculus side---normal-form bisimilarity, applicative bisimilarity, and contextual equivalence---that we internalize into abstract machines in order to prove full abstraction.

ABSTRACT. We present two finitary cut-free sequent calculi for the modal mu-calculus. One is a variant of Kozen’s axiomatisation in which cut is replaced by a strengthening of the induction rule for greatest fixed point. The second system derives annotated sequents in the style of Stirling’s ‘tableau proof system with names’ (2014) and features a generalisation of the nu-regeneration rule that allows discharging open assumptions. Soundness and completeness for the two calculi is proved by establishing a sequence of embeddings between proof systems, starting at Stirling’s tableau-proofs and ending at the original axiomatisation of the mu-calculus due to Kozen. As a corollary we obtain a new, constructive, proof of completeness for Kozen’s axiomatisation which avoids the usual detour through automata and games.

ABSTRACT. We investigate multi-agent epistemic modal logic with common knowledge modalities for groups of agents and obtain van Benthem style model-theoretic characterisation, in terms of bisimulation invariance of classical first-order logic over the non-elementary classes of (finite or arbitrary) common knowledge Kripke frames. The fixpoint character of common knowledge modalities and the rôle that reachability and transitive closures play for the derived accessibility relations take our analysis beyond classical model-theoretic terrain and technically pose a novel challenge to the analysis of model-theoretic games. Over and above the more familiar locality-based techniques for relational structures we exploit a specific structure theory for specially adapted Cayley groups. We show that suitable finite Cayley groups can (a) be viewed as typical epistemic frames through the association of agents with the generators, and (b) support a locality analysis at different levels of granularity as induced by distance measures w.r.t. various coalitions of agents.

ABSTRACT. A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKID-omega includes the provability of the classical system of Martin-Lof's inductive definitions, called LKID, and conjectured the equivalence. By this year the equivalence has been left an open question. In general, the conjecture was proved to be false in FoSSaCS 2017 paper by Berardi and Tatsuta. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the conjecture is proved to be true in FoSSaCS 2017 paper by Simpson. This paper shows that if we add arithmetic to both systems, they become equivalent, namely, the conjecture holds. The result of this paper includes that of the paper by Simpson as a special case. In order to construct a proof of LKID for a given cyclic proof, this paper shows every bud in the cyclic proof is provable in LKID, by cutting the cyclic proof into subproofs such that in each subproof the conclusion is a companion and the assumptions are buds. The global trace condition gives some induction principle, by using an extension of Podelski-Rybalchenko termination theorem from well-foundedness to induction schema. In order to show this extension, this paper also shows that infinite Ramsey theorem is formalizable in Peano arithmetic.