-
20 février 2018 à 10h30, Salle 2
Sam van Gool,
Monadic second order logics as model companions of temporal logics, Part II
In this talk I will explain a model-theoretic approach to monadic second order (MSO) logic, which I am developing in ongoing joint work with Silvio Ghilardi. We exhibit, for various classes of semantic structures, a close connection between MSO logic and the first order theory of the algebras for well-known propositional temporal logics. This connection is given by the notion of model companions from model theory, which I will recall in the talk. Specifically, we have proved so far that MSO logic over infinite words gives the model companion of linear temporal logic [1], and that bisimulation invariant MSO logic over infinite trees gives the model companion of a new extension of computation tree logic with local fairness constraints [2].
Proving these results requires two main ingredients: (i) completeness for the axiomatization of the temporal logic with respect to the intended semantic structures, for which we use Stone duality and a tableau construction; (ii) a conversion from full MSO logic to the existential fragment of the first order theory of the algebras for the temporal logic, for which we use correspondences between MSO logic and automata.
References:
[1] S. Ghilardi and S. J. v. Gool, "A model-theoretic characterization of monadic second-order logic on infinite words", J. Symbolic Logic, vol. 82, no. 1, 62-76 (2017)
[2] S. Ghilardi and S. J. v. Gool, "Monadic second order logic as the model companion of temporal logic", LICS 2016, 417--426 (2016)
-
13 février 2018 à 10h30, Salle 2
Sam van Gool,
Monadic second order logics as model companions of temporal logics, Part I
In this talk I will explain a model-theoretic approach to monadic second order (MSO) logic, which I am developing in ongoing joint work with Silvio Ghilardi. We exhibit, for various classes of semantic structures, a close connection between MSO logic and the first order theory of the algebras for well-known propositional temporal logics. This connection is given by the notion of model companions from model theory, which I will recall in the talk. Specifically, we have proved so far that MSO logic over infinite words gives the model companion of linear temporal logic [1], and that bisimulation invariant MSO logic over infinite trees gives the model companion of a new extension of computation tree logic with local fairness constraints [2].
Proving these results requires two main ingredients: (i) completeness for the axiomatization of the temporal logic with respect to the intended semantic structures, for which we use Stone duality and a tableau construction; (ii) a conversion from full MSO logic to the existential fragment of the first order theory of the algebras for the temporal logic, for which we use correspondences between MSO logic and automata.
References:
[1] S. Ghilardi and S. J. v. Gool, "A model-theoretic characterization of monadic second-order logic on infinite words", J. Symbolic Logic, vol. 82, no. 1, 62-76 (2017)
[2] S. Ghilardi and S. J. v. Gool, "Monadic second order logic as the model companion of temporal logic", LICS 2016, 417--426 (2016)
-
6 février 2018 à 10h30, Salle 2
Clemens Berger,
Comprehensive factorisation for idempotent semigroups and
non-commutative Stone duality
-
30 janvier 2018 à 10h30, Salle 2
Clemens Berger,
Working session on monotone-light factorization, distributive lattices,
rings and Hochster's theorem
-
23 janvier 2018 à 10h30, Salle de Conférences
Matthias Baaz,
On the benefit of unsound rules
The study of proofs is motivated by our desire for deductive reasoning to be correct, i.e., we wish that it be such that the procedures involved derive only true conclusions. The traditional way of ensuring this involves restricting proofs to those satisfying specific properties. In this work we challenge this practice and give examples of correct logical calculi augmented with unsound rules. More precisely, we give examples of calculi that extend Gentzen’s sequent calculus LK by unsound quantifier inferences in such a way that (i) derivations lead only to true sequents, and (ii) proofs therein are non-elementarily shorter than LK-proofs. This is joint work with Juan P. Aguilera.
-
19 décembre 2017 à 10h30, Salle 1
Clemens Berger,
Factorisation systems and
universal coverings, Part II
There is a correspondence
between factorisation systems and
minor variant of what Lawvere calls
comprehension schemes. The latter are
often easier to define than the
corresponding factorisation systems.
This happens for instance for the
comprehension scheme which assigns to
a small category C the category
Funct(C,Sets) of set-valued diagrams
on C. The corresponding factorisation
of a functor is called its
comprehensive factorisation and has
been defined for the first time by
Street and Walters.
We shall
be interested in the comprehension
scheme which assigns to a well-behaved
topological space X the category of
locally constant set-valued sheaves on
X, or what amounts to the same (by the
espace étalé-construction) the
category of topological coverings of
X. The associated factorisation system
gives a formal construction of the
universal covering of X, and actually
permits a Galois-theoretical
interpretation of topological
coverings.
-
7 décembre 2017 à 15h00, Salle 1
Clemens Berger,
Factorisation systems and
universal coverings, Part I
There is a correspondence
between factorisation systems and
minor variant of what Lawvere calls
comprehension schemes. The latter are
often easier to define than the
corresponding factorisation systems.
This happens for instance for the
comprehension scheme which assigns to
a small category C the category
Funct(C,Sets) of set-valued diagrams
on C. The corresponding factorisation
of a functor is called its
comprehensive factorisation and has
been defined for the first time by
Street and Walters.
We shall
be interested in the comprehension
scheme which assigns to a well-behaved
topological space X the category of
locally constant set-valued sheaves on
X, or what amounts to the same (by the
espace étalé-construction) the
category of topological coverings of
X. The associated factorisation system
gives a formal construction of the
universal covering of X, and actually
permits a Galois-theoretical
interpretation of topological
coverings.
-
28 novembre 2017 à 10h30, Salle 1
Daniela Petrisan,
Automata Minimization: a Functorial Approach
In this talk I will present a categorical approach to automata minimization. We regard automata (or more generally language recognisers) as functors from a category that captures the structure of the input (words, monoids, trees) to another category that models the type of the automata (deterministic, non-deterministic, weighted, transducers etc). We show how to obtain a unifying framework for understanding various well-known phenomena in automata theory. Examples include the usual minimization of DFAs, of weighted automata over a field, of subsequential transducers, but also syntactic algebras for regular languages and the syntactic Boolean space with an internal monoid for a non-regular language. We have also obtained the existence of a minimimal automaton for a new model of automata that generalizes Schützenberger's weighted automata.
This talk is based on the papers:
[1] Thomas Colcombet, Daniela Petrişan. “Automata Minimization: a Functorial Approach”. In CALCO 2017
[2] Thomas Colcombet, Daniela Petrişan. “Automata in glued vector spaces”. In: MFCS 2017.
-
21 novembre 2017 à 10h30, Salle 1
Célia Borlido,
Semidirect products, monoids and categories
Motivated by the Prime Decomposition Theorem (also known by Krohn-Rhodes Theorem), the question of determining whether a given finite monoid belongs to a semidirect product of two pseudovarieties came into the picture in the mid sixties. Tilson, by defining the derived category of a relational morphism of monoids, made it clear that considering finite categories as generalized monoids was crucial to obtain satisfactory answers. We will explain some of the concepts involved, see examples and, if time allows, we will illustrate in a simple case how in some situations all those tools can be used to obtain an equational description of semidirect products.
-
14 novembre 2017 à 10h30, Salle 1
Carlos Simpson,
Counting categories, 2-metric spaces and approximate categorical structures
We start by discussing the problem of counting how many finite categories there are with a given matrix. A natural structure which shows up is close to the notion of 2-metric space. We’ll then recall this, and explain how it can be generalized to a definition of “approximate categorical structure”. Lawvere’s notion of bimodule leads to a Yoneda functor for certain ACS, which can be used to express these ACS as substructures of metrized categories.
-
24 octobre 2017 à 10h30, Salle 1
Mai Gehrke,
Discussion on formal languages and duality
-
17 octobre 2017 à 10h30, Salle 1
Luca Reggio,
Adding a layer of (simple) quantifiers via semidirect products and codensity monads, Part II
Obtaining equations for logic fragments is closely related to understanding the dual spaces of the the corresponding Boolean algebras of formal languages. Further, since logic fragments typically are built up from atomic formulas by alternating applications of quantifiers and Boolean (or lattice) closure, it is an important technical point to understand what construction on recognisers corresponds to the application of one layer of quantifiers. It is well-known from regular language theory that various forms of (two-sided) semidirect products of (finite and profinite) monoids are part of the answer.
In this talk we show, in the setting of arbitrary formal languages, that certain simple quantifiers, such as the classical existential quantifier and modular counting quantifiers, correspond dually to certain semidirect products for recognisers. Our main tools are codensity monads and duality theory. Our construction yields, in particular, a new characterisation of the profinite monad of the free S-semimodule monad for finite commutative semirings S. In the case of the classical existential quantifier, the semiring S is the two-element lattice, yielding the Vietoris monad on Boolean spaces as the codensity monad of the finite powerset functor.
While `soundness’ of our construction is very cleanly explained using category theoretic constructions, the `completeness’ part of our results require methods from Stone duality.
-
10 octobre 2017 à 16h00, Salle 1
Luca Reggio,
Adding a layer of (simple) quantifiers via semidirect products and codensity monads, Part I
Obtaining equations for logic fragments is closely related to understanding the dual spaces of the the corresponding Boolean algebras of formal languages. Further, since logic fragments typically are built up from atomic formulas by alternating applications of quantifiers and Boolean (or lattice) closure, it is an important technical point to understand what construction on recognisers corresponds to the application of one layer of quantifiers. It is well-known from regular language theory that various forms of (two-sided) semidirect products of (finite and profinite) monoids are part of the answer.
In this talk we show, in the setting of arbitrary formal languages, that certain simple quantifiers, such as the classical existential quantifier and modular counting quantifiers, correspond dually to certain semidirect products for recognisers. Our main tools are codensity monads and duality theory. Our construction yields, in particular, a new characterisation of the profinite monad of the free S-semimodule monad for finite commutative semirings S. In the case of the classical existential quantifier, the semiring S is the two-element lattice, yielding the Vietoris monad on Boolean spaces as the codensity monad of the finite powerset functor.
While `soundness’ of our construction is very cleanly explained using category theoretic constructions, the `completeness’ part of our results require methods from Stone duality.
-
3 octobre 2017 à 10h30, Salle 2
Mai Gehrke,
Recognition in automata theory, its connection to Stone duality for Boolean algebras, and to logic, Part II
In this talk we will introduce the basic notions of regular language theory such as automata and recognition by automata and by monoids and we will see how recognition is related to Stone duality. We also introduce Buchi’s logic on words, which identifies words (i.e. elements of free monoids) as relational structures for a formal logical language, and give examples of im- portant language classes which are precisely the model classes of sentences from various logic fragments.
-
26 septembre 2017 à 10h30, Salle 1
Mai Gehrke,
Recognition in automata theory, its connection to Stone duality for Boolean algebras, and to logic, Part I
In this talk we will introduce the basic notions of regular language theory such as automata and recognition by automata and by monoids and we will see how recognition is related to Stone duality. We also introduce Buchi’s logic on words, which identifies words (i.e. elements of free monoids) as relational structures for a formal logical language, and give examples of im- portant language classes which are precisely the model classes of sentences from various logic fragments.