BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Logique\, automates\, algèbre et jeux seminar of IRIF
NAME:Logique\, automates\, algèbre et jeux
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Logique\, automates\, algèbre et jeux seminar of IRIF
X-WR-CALNAME:Logique\, automates\, algèbre et jeux
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Lyndon’s theorem - Florent Capelli\, Liafa
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160616T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160616T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:447
DESCRIPTION:A first-order formula is positive if it does not contain any n
egations. It is not so difficult to prove that such formulas are preserved
under surjective homomorphism\, meaning that if some model M satisfies it
\, and there is a surjective homomorphism from M onto M′\, then M′ als
o satisfies the formula. Lyndon’s theorem states that all first-order fo
rmulae preserved in this way are equivalent to a positive formula. Hence\,
Lyndon’s theorem characterizes syntactically this preservation property
. Statement of similar forms are usually called ‘preservation theorems
’. This theorem\, as it is often the case for preservation theorems for
first-order is not true in the finite: this signifies that there are first
-order formulae which are preserved under surjective homomorphism between
finite models\, but are not equivalent to any positive formula.\n\nIn this
presentation\, we will give a panorama of various classical preservation
theorems for first-order logic. We will then present a proof of Lyndon’s
theorem\, and a proof that it does not hold in the finite case (this last
construction is a joint work with Arnaud Durant\, Amélie Gheerbrant and
Cristina Sirangelo).
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Proof complexity\, constraint satisfaction and graph isomorphism -
Joanna Ochremiak\, Université Denis Diderot - Paris 7
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180314T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180314T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:453
DESCRIPTION:In this second part of my talk I will discuss the algebraic ap
proach to the constraint satisfaction problem (CSP)\, a framework which wa
s very recently used to confirm the famous Feder-Vardi CSP dichotomy conje
cture. I will also indicate how this approach can be employed to analyse t
he power of various proof systems for CSPs.
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Survey on Classical and Novel Results on Presburger Arithmetic -
Christoph Haase\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160204T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160204T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:454
DESCRIPTION:Presburger arithmetic is the first-order theory of the natural
numbers with addition and order. This theory was shown decidable by M. Pr
esburger in 1929. In the 1960s\, Presburger arithmetic was studied in the
context of formal language theory. Two of the main results from this perio
d are that the sets of natural numbers definable in Presburger arithmetic
are the so-called semi-linear sets\, and that Parikh images of languages g
enerated by context-free grammars are semi-linear and hence Presburger-def
inable. Subsequently\, from the 1970s onwards the computational complexity
of Presburger arithmetic received interest. The landmark results from thi
s period are a doubly exponential lower bound shown by Fischer and Rabin i
n 1974 and a triply-exponential upper bound shown by Oppen in 1978. The 19
80ies brought a more fine-grained complexity analysis of (fragments of) Pr
esburger arithmetic by Fürer\, Grädel and Scarpellini. In this talk\, I
will survey those classical results and show the relevant proofs or proof
ideas for most of them. I will in depth discuss a recent result that shows
that Presburger arithmetic with a fixed number of quantifier alternations
is complete for every level of the weak EXP hierarchy. If time permits\,
I will discuss some recent work in which Presburger arithmetic has been us
ed for showing new lower bounds for equivalence problems for commutative g
rammars.
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Survey on Classical and Novel Results on Presburger Arithmetic -
Christoph Haase\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160121T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160121T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:455
DESCRIPTION:First part
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ideals in VAS Reachability - Sylvain Schmitz\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160107T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160107T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:456
DESCRIPTION:The decidability of the reachability problem for vector additi
on systems is a notoriously difficult result. First shown by Mayr in 1981
after a decade of unsuccessful attempts and partial results\, its proof ha
s been simplified and refined several times\, by Kosaraju\, Reutenauer\, a
nd Lambert\, and re-proven by very different techniques by Leroux in 2012.
The principles behind the original proof remained however obscure.\n\nIn
this seminar\, I will present the ideas behind the algorithms of Mayr\, Ko
saraju\, and Lambert (the KLM algorithm) in the light of ideals of well-qu
asi-orders. The interest here is that ideals provide a semantics to the st
ructures manipulated in the KLM algorithm\, bringing some new understandin
g to its proof of correctness.\n\nJoint work with Jérôme Leroux (LaBRI)
presented at LICS’15\; see http://arxiv.org/abs/1503.00745
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rackoff’s Coverability Technique - Ranko Lazic\, Warwick univers
ity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20151217T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20151217T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:457
DESCRIPTION:Rackoff’s small witness property for the coverability proble
m is the standard means to prove tight upper bounds in vector addition sys
tems (VAS) and many extensions. We show how to derive the same bounds dire
ctly on the computations of the VAS instantiation of the generic backward
coverability algorithm. This relies on a dual view of the algorithm using
ideal decompositions of downwards-closed sets\, which exhibits a key struc
tural invariant in the VAS case. The same reasoning readily generalises to
several VAS extensions.\n\nJoint work with Sylvain Schmitz presented at R
P ’15\; see https://hal.inria.fr/hal-01176755/.
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Quasi-polynomial algorithms for parity games - Nathanaël Fijlakow
\, Turing Institute / CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171123T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171123T110000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:458
DESCRIPTION:
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ideals of Well-Quasi-Orders - Sylvain Schmitz\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20151203T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20151203T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:461
DESCRIPTION:The purpose of this seminar is to introduce the notion of idea
ls of well-quasi-orders. These irreducible downwards-closed sets of elemen
ts were first invented in the 1970’s but rediscovered in recent years in
the theory of well-structured transition systems\, notably by Finkel and
Goubault-Larrecq. Ideals provide indeed finite effective representations o
f downwards-closed sets\, in the same way as bases of minimal elements pro
vide representations of upwards-closed sets.\n\nAfter defining ideals and
establishing some of their properties\, I will illustrate their use in a c
oncrete setting. I will present some recent results by Czerwiński\, Marte
ns\, van Rooijen\, and Zeitoun (FCT’15) on the decidability of piecewise
-testable separability in the light of ideals. This seminar is also a warm
-up for the next seminar on reachability in vector addition systems.
LOCATION:2015
END:VEVENT
BEGIN:VEVENT
SUMMARY:Abiteboul-Vianu theorem - Luc Segoufin\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20151112T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20151112T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:462
DESCRIPTION:Descriptive complexity measure a problem in terms of the diffi
culty to express it. At first look this seems to have nothing to do with c
omputational measures such as time and space. However it does have intimat
e links with classical computational complexity.\n\nThe most celebrated on
e is Fagin’s theorem linking the complexity class NP with the expressive
power of existential second-order logic.\n\nIn this lecture we will study
the Abiteboul-Vianu theorem saying that the separation of PTime and PSpac
e can be rephrased in terms of expressive powers of partial fixpoints vers
us least fixpoints.
LOCATION:2015
END:VEVENT
BEGIN:VEVENT
SUMMARY:“À la Bojańcyk” proof of limitedness - Thomas Colcombet\, LI
AFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20151105T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20151105T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:463
DESCRIPTION:The limitedness is a question of boundedness: given a function
from words to integers described by some suitable model of finite state m
achines (distance automata\, B-automata\, ...)\, determine whether the fun
ction it computes is bounded. It happens that for distance automata [Hashi
guchi81\, Leung82\, Simon84] and B-automata [Kirsten05\, Bojańczyk&C.06\,
C.09]\, this problem turns out to be decidable. This deep result is used
in many situations\, and in particular for solving the famous star-height
problem [Hashiguchi88\, Kirsten05]. (This problems asks\, given a regular
language L and a non-negative integer k\, whether it is possible to descri
be L by means of a regular expression with nesting of Kleene stars bounded
by k).\n\nIn his recent LICS15 paper\, Bojańczyk gave a much shorter and
self-contained proof of the decidability of limitedness (and in fact also
star-height). It relies on a reduction to finite games of infinite durati
on\, and involves arguments of positionality of stragegies in quantitative
games [C.&Löding08]. The topic of this talk is the presentation of this
elegant proof.\n\nThe decidability of limitedness was already presented in
the LAAG seminar (using the algebraic approach of stabilization monoids)\
, but the proof here is entirely different.
LOCATION:2015
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decidability of DPDA equivalence\, part IV - Stefan Göller\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150701T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150701T110000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:464
DESCRIPTION:These two talks will continue the study of the equivalence pro
blem of deterministic pushdown automata (DPDA).\n\nThe main focus of these
talks will be on the computational complexity of this problem. We will gi
ve a proof of Stirling’s result that DPDA equivalence is primitive recur
sive.\n\nMore precisely\, we will present a recent paper by Jancar that sh
ows that in case two DPDAs are inequivalent they can be distinguished by a
word whose length is bounded by a tower of exponentials of elementary hei
ght.\n\nAs in Arnaud’s talk we will view DPDA equivalence in terms of tr
ace equivalence of deterministic first-order grammars.\n\nThis talk aims a
t going hand-in-hand with Arnaud’s talk but is intended to be self-conta
ined as well.\n\nThese talks will be completely self-contained and require
no background knowledge.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decidability of DPDA equivalence\, part III - Stefan Göller\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150617T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150617T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:465
DESCRIPTION:These two talks will continue the study of the equivalence pro
blem of deterministic pushdown automata (DPDA).\n\nThe main focus of these
talks will be on the computational complexity of this problem. We will gi
ve a proof of Stirling’s result that DPDA equivalence is primitive recur
sive.\n\nMore precisely\, we will present a recent paper by Jancar that sh
ows that in case two DPDAs are inequivalent they can be distinguished by a
word whose length is bounded by a tower of exponentials of elementary hei
ght.\n\nAs in Arnaud’s talk we will view DPDA equivalence in terms of tr
ace equivalence of deterministic first-order grammars.\n\nThis talk aims a
t going hand-in-hand with Arnaud’s talk but is intended to be self-conta
ined as well.\n\nThese talks will be completely self-contained and require
no background knowledge.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decidability of DPDA equivalence\, part II - Arnaud Carayol\, LIGM
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150603T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150603T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:466
DESCRIPTION:In this series of talks\, we will present a proof of the decid
ability of the equivalence problem for deterministic pushdown automata. Na
mely given two deterministic pushdown automata\, it is decidable if they a
ccept the same language. This result was first proved by Géraud Sénizerg
ues in 1997. His proof consists in two semi-decision procedures and hence
while establishing decidability does not give an upper-bound on the comple
xity of the problem. In 2002\, Colin Stirling gave a primitive recursive a
lgorithm to decide the problem.\n\nThe aim of the talk is to present what
seems to be the simplest self-contained proof of this result. We will pres
ent a proof based on the recent work of Petr Jancar which uses first-order
grammars instead of deterministic pushdown automata. To keep the proof as
simple as possible\, we will present the proof giving two semi-decision p
rocedures.
LOCATION:4068a
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decidability of DPDA equivalence\, part I - Arnaud Carayol\, LIGM
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150527T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150527T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:467
DESCRIPTION:In this series of talks\, we will present a proof of the decid
ability of the equivalence problem for deterministic pushdown automata. Na
mely given two deterministic pushdown automata\, it is decidable if they a
ccept the same language. This result was first proved by Géraud Sénizerg
ues in 1997. His proof consists in two semi-decision procedures and hence
while establishing decidability does not give an upper-bound on the comple
xity of the problem. In 2002\, Colin Stirling gave a primitive recursive a
lgorithm to decide the problem.\n\nThe aim of the talk is to present what
seems to be the simplest self-contained proof of this result. We will pres
ent a proof based on the recent work of Petr Jancar which uses first-order
grammars instead of deterministic pushdown automata. To keep the proof as
simple as possible\, we will present the proof giving two semi-decision p
rocedures.
LOCATION:4068a
END:VEVENT
BEGIN:VEVENT
SUMMARY:Algorithmics Properties of Probabilistic Automata\, part II - Nath
anaël Fijalkow\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150415T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150415T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:468
DESCRIPTION:This talk is a continuation of the talk from two weeks ago\, b
ut it will be independent\, so please consider coming even if you didn’t
attend the first part.\n\nThe plan for this second session is:\n\n - exp
lain how to obtain a universally non-regular automaton (by adding one stat
e to last time’s example)\,\n - explain how to encode Minsky machines u
sing bounded-error probabilistic automata\, with two-way and one-way varia
nts\,\n - explain how to encode probabilistic automata using only one ran
dom probabilistic transition\,\n show the decidability of two problems:
the equivalence and the finiteness problem. Both proofs rely on one obser
vation: the reals with the addition and the multiplication form a field\,
and some linear algebra.
LOCATION:4067
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Naughty Side of Probabilistic Automata. - Nathanaël Fijalkow\
, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150401T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150401T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:469
DESCRIPTION:This talk is about probabilistic automata over finite words: s
uch machines\, when reading a letter\, flip a coin to determine which tran
sition to follow. Although quite simple\, this computational model is quit
e powerful\, and many natural problems are undecidable.\n\nIn this talk\,
I will review some of the most important undecidability results\, with new
simplified constructions.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:On topology in automata theory\, Part II - Michał Skrzypczak\, LI
AFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150311T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150311T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:470
DESCRIPTION:This talk will be a continuation of my talk from 11th February
. I will not assume knowledge of any material presented then except for ba
sic notions of topology. During this talk I will move to the case of regul
ar languages of infinite trees. Since there are known examples of such lan
guages that are not Borel I will introduce the projective hierarchy. This
hierarchy allows to study complexity of sets defined using big quantifiers
(i.e. ranging over sets of naturals). I will focus on correspondence betw
een topological complexity and automata-theoretic complexity measured by t
he Rabin-Mostowski index. My aim will be to prove certain results of stric
t containment using purely topological methods. At the end I hope to prese
nt some recent results about extensions of MSO.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Non-determinism vs two-way. - Gabriele Puppis\, LABRI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150128T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150128T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:471
DESCRIPTION:Non-determinism and walking mechanisms were considered already
at the very beginning of automata theory. I will survey a few results con
necting models of automata and transducers enhanced with non-determinism a
nd two-wayness.\n\nA classical result by Rabin and Scott shows that determ
inistic finite state automata are as expressive as their non-deterministic
and two-way counterparts. The translation from two-way automata to one-wa
y automata is easily seen to imply an exponential blowup in the worst case
\, even when one maps deterministic two-way models to non-deterministic on
e-way models. The converse translation\, which is based on the subset cons
truction and maps non-deterministic one-way automata to deterministic ones
\, also implies an exponential blowup. This latter translation\, however\,
is not known to be optimal when one aims at removing non-determinism by p
ossibly introducing two-wayness. In particular\, the question of whether t
he exponential blowup is unavoidable in transforming non-determinism to tw
o-wayness is open.\n\nWhen one turns to models of transducers\, some trans
lations are not anymore possible. For example\, one-way transducers (even
those that exploit functional non-determinism) are easily seen to be less
powerful than two-way transducers (even input-deterministic ones). A natur
al problem thus arises that amounts at characterizing the two-way transduc
tions that can be implemented by one-way functional transducers. The latte
r problem was solved in recent paper by Filiot\, Gauwin\, Reynier\, and Se
rvais – however\, some questions related to complexity remains open. Ano
ther interesting\, but older\, result by Hopcroft shows that functional no
n-determinism can be removed from two-way transducers\, at the cost of an
exponential blow-up. A similar transformation can be used to prove that tw
o-way transducers are closed under functional composition.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:On topology in automata theory\, Part I - Michał Skrzypczak\, LIA
FA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20150211T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20150211T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:472
DESCRIPTION:The interplay between topology and automata theory has a form
of synergy: descriptive set theory motivates new problems and methods in a
utomata theory but on the other hand\, automata theory introduces natural
examples for classical topological concepts.\n\nDuring this talk I will in
troduce basic notions of topology and descriptive set theory focusing on t
he case of infinite words. I’ll say what is the Borel hierarchy and the
Wadge order. Then I’ll show how these tools are related to automata theo
ry. I’ll try to argue that even from purely automata theoretic point of
view\, it is possible to obtain new results and new proofs by referring to
topological concepts.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Equivalence checking of infinite state systems: A couple of lower
bounds - Stefan Göller\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20141217T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20141217T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:473
DESCRIPTION:We will recall a generic technique for proving lower bounds fo
r bisimulation equivalence checking (for which there was not enough time i
n my last LAAG talk) . First\, we will introduce bisimulation equivalence
and recall Jancar’s and Srba’s Defender’s Forcing lower bound techni
que. Then\, we will apply this technique to different classes of infinite
state systems for showing the following hardness results : (1) undecidabil
ity for prefix-recognizable graphs\, (2) undecidability for vector additio
n systems\, (3) nonelementary hardness for pushdown graphs\, and (4) Acker
mann hardness for equational graphs of finite out-degree.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Stabilization monoids and cost functions - Thomas Colcombet\, LIAF
A
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20141203T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20141203T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:474
DESCRIPTION:In this third part\, we will introduce stabilization monoids a
nd cost functions\, and show ho this constitutes a good framework in which
the results of the previous talks can be unified.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decidability of Boundedness and Limitedness - Thomas Colcombet\, L
IAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20141119T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20141119T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:475
DESCRIPTION:This talk constitutes the continuation of the previous one\, i
n which the star-height problem was reduced to a boundedness question.\n\n
In this second part\, we will establish the decidability of this second pr
oblem\, following the ideas of Leung\, Simon\, and Kirsten.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:The star-height problem and its link to boundedness and limitednes
s - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20141105T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20141105T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:476
DESCRIPTION:This talk is the first in a series of lecture intended to desc
ribe the main ideas and the use of automata limitedness and related questi
ons.\n\nThe goal of the first session is to present the famous (restricted
) star-height problem\, and show the first steps toward its resolution. Th
e question is the following: given a regular language L and a non-negative
integer k\, can we decide whether L can bee represented as a regular expr
ession of star-height (i.e.\, nesting of Kleene stars) at most k. This pro
blem has been open for 25 years unit Hashiguchi provided a proof in a seri
es of four paper\, between 81 and 88. This proof is notoriously difficult\
, and the presentation here will be based on the ideas in the more modern\
, and much simpler\, proof of Kirsten (2005).\n\nThe idea behind both thes
e proofs is to reduce the original problem to a question of existence of b
ounds for a function computed by some specific forms of automata (distance
automata\, nested-distance desert automata\, B-automata\, …). This idea
goes much beyond the scope of the star-height problem\, and I will try to
convey this idea through several examples.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Une introduction aux graphes expandeurs - David Xiao\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20140410T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20140410T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:477
DESCRIPTION:Les graphes expandeurs sont des graphes creux mais fortement c
onnexes. Ils peuvent se substituer aux graphes denses ou même aux graphes
complets dans beaucoup d’applications\, et ainsi permettre une réducti
on de complexité de calcul ou d’aléa. Ils jouent un rôle clé dans pl
usieurs domaines de l’informatique fondamentale\, notamment dans la dér
andomisation et le pseudo-aléa.\n\nDans cet exposé nous présenterons le
s graphes expandeurs\, leur(s) définition(s)\, quelques lemmes structurel
s fondamentaux\, et quelques exemples de leur utilisation dans la dérando
misation. Nous esquisserons également la construction basée sur le produ
it zigzag.
LOCATION:2014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Automata characterizations of WMSO - Michael Vanden Boom\, Oxford
university
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20140327T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20140327T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:478
DESCRIPTION:Weak monadic second-order logic (WMSO) over the infinite binar
y tree has the same syntax as MSO\, but second-order quantification is int
erpreted only over finite sets. It captures a strict subclass of the regul
ar languages of infinite trees\, but is expressive enough to subsume tempo
ral logics like CTL.\n\nIn this talk\, I will sketch the proofs showing th
e equivalence of WMSO and a form of automata called weak alternating autom
ata. I will also prove Rabin’s characterization of WMSO: a language is w
eakly definable iff the language and its complement are recognizable by no
ndeterministic Büchi automata.\n\nI will conclude by describing connectio
ns with recent work (joint with Thomas Colcombet\, Denis Kuperberg\, and C
hristof Löding) showing that given a Büchi automaton as input\, it is de
cidable whether the language is definable in WMSO.
LOCATION:2014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Rabin theorem - Olivier Serre\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20140313T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20140313T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:479
DESCRIPTION:In 1969\, Michael O. Rabin established that the class of regul
ar tree languages (i.e. languages of infinite node-labelled complete binar
y trees accepted by non-deterministic tree automata) form a Boolean algebr
a. The goal of this talk is to present the underlying objects of this stat
ement as well as a complete proof of it.\n\nHence\, the structure of the t
alk will be as follows:\n\n - Main definitions and examples : infinite t
rees\, parity tree automata and regular tree languages\n - Basic recalls
on positional determinacy of two-player parity games on graphs (see previ
ous LAAG seminar by Nathanaël Fijalkow)\n - Acceptance game and emptine
ss game/test for parity tree automata\n - Complementation of parity tree
automata relying on positional determinacy and determinisation of automat
a on infinite words (see previous LAAG seminar).\n\nI will assume no speci
fic knowledge on automata nor games for that talk.
LOCATION:2014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Positional determinacy part II - Nathanaël Fijalkow\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20140301T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20140301T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:480
DESCRIPTION:Last week\, Thomas Colcombet presented a proof of Positional D
eterminacy for Parity Games\, following a forward approach. In this second
part\, I will present a completely different proof of the same result bas
ed on ideas by Muller and Schupp\, following a backward approach.\n\nI wil
l highlight the differences between the two approaches\, and the applicati
ons of both techniques. In particular\, I will explain why backward approa
ches naturally induce determinization procedures for automata over infinit
e words.\n\nThe talk will be self-contained\, and in particular I will qui
ckly recall all required definitions at the beginning.
LOCATION:2014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Positional determinacy part I - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20140206T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20140206T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:481
DESCRIPTION:In this sequence of two seminars\, we will recall the basic de
finitions of games and parity games. We will give several proofs and appli
cations of the most famous result in this context: the memoryless determin
acy theorem. We will also see how some of these techniques naturally provi
de determinization procedures over infinite words.\n\nThis is in preparati
on to the seminars after the holidays\, that will aim at presenting the re
sults on the monadic theory of the infinite binary tree.
LOCATION:2014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Complexity classes beyond elementary - Sylvain Schmitz\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20131219T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20131219T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:482
DESCRIPTION:I will present a hierarchy of fast-growing complexity classes
and show its suitability for completeness statements of many non elementar
y problems\, which occur naturally in logic\, combinatorics\, formal langu
age\, verification\, etc.\, with complexities ranging from simple towers o
f exponentials to Ackermannian and beyond.\n\nI plan to skim over the foll
owing topics:\n\n - subrecursive hierarchies: these are functions and cl
asses that allow to define rapidly-growing functions by recursion over ord
inal indices\,¡/li¿\n - length function theorems for well-quasi-orders
\, which are the key combinatorial statements for the upper bounds of most
of the non-elementary problems I will mention\,¡/li¿\n - the definiti
on of fast-growing complexity classes and some easy properties.\n\nThe rec
ent results will be taken from work together with S. Abriola\, D. Figueira
\, S. Figueira\, C. Haase\, S. Haddad\, and Ph. Schnoebelen.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Decision Problems for Linear Recurrence Sequences - Joël Ouaknine
\, Oxford university
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20131128T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20131128T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:483
DESCRIPTION:Linear recurrence sequences (such as the Fibonacci numbers) pe
rmeate a vast number of areas of mathematics and computer science (in part
icular: program termination and probabilistic verification)\, and also hav
e many applications in other fields such as economics\, theoretical biolog
y\, and statistical physics. In this talk\, I will focus on three fundamen
tal decision problems for linear recurrence sequences\, namely the Skolem
Problem (does the sequence have a zero?)\, the Positivity Problem (are all
terms of the sequence positive?)\, and the Ultimate Positivity Problem (a
re all but finitely many terms of the sequence positive?).\n\nThis is join
t work with James Worrell.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Green’s relations and automata theory - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20131107T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20131107T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:484
DESCRIPTION:Green’s relations form a fundamental tool in the analysis of
the structure of semigroups and monoids\, in particular for the finite on
es. Understanding Green’s relations can give remarkable intuitions conce
rning these objects\, and as a consequence for understanding the structure
of regular languages of words (finite or infinite). In particular\, this
description generalizes the understanding of automata through their decomp
osition into strongly connected components that is used in many proofs.\n\
nDuring this talk\, I will present some of the key results concerning Gree
n’s relations\, emphasizing on how one can think about regular languages
using them. I will also show how these can be used for deriving non-trivi
al automata related results (such as McNaughton’s determinization result
\, Schützenberger’s characterization of star-free languages\, Simon’s
factorization forest theorem\, ... though unfortunately I will not have t
ime do to all these).
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:How to count in weak formalisms? - Arnaud Durand\, Université Den
is Diderot - Paris 7
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20131017T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20131017T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:485
DESCRIPTION:The counting ability of weak formalisms (e.g. determining the
number of 1’s in a string of length N) is of interest as a measure of th
eir expressive power\, and also resorts to complexity theoretic motivation
s : the more we can count the closer we get to real computing power. The q
uestion was investigated in several papers in complexity theory and in wea
k arithmetic a long time ago. In each case\, the considered formalism (con
stant-depth circuits\, MSO with addition or first-order bounded arithmetic
) was shown to be able to count up to a polylogarithmic number. An essenti
al part of the proofs is the construction of a 1–1 mapping from a small
subset of {0\,...\,N - 1} into a small initial segment. In each case the e
xpressibility of this mapping depends on some strong and non-constructive
argument (group theoretic device or prime number theorem).\n\nIn this talk
we will evocate these different methods and present a completely elementa
ry (and constructive) approach to reprove uniformly all these results (bas
ed on an old paper with M. More and C. Lautemann). We will also review why
some of these results cannot be extended.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Machine Learning Viewed by a Logician - Łukasz Kaiser\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130613T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130613T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:486
DESCRIPTION:Machine learning guys do things like linear regression\, neura
l networks and support vector machines. Logic guys do relational structure
s\, formulas\, automata and such stuff. These two type of guys hardly ever
meet to work together. So few logic guys know that neural networks are so
metimes considered with only binary weights and signals\, which makes them
exactly circuits. And few machine learning guys know quantitative logics
good enough to recognize thier standard neural network in a formula. In th
is talk\, I will define very basic concepts used in machine learning in a
way that exposes their logic counterparts. I will then argue that such rel
ationship can be beneficial for both fields - providing theorems and deepe
r understanding to machine learning and practically relevant questions and
experimental results to logic.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Cost of Repairing Regular Specifications - Gabriele Puppis\, L
ABRI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130530T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130530T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:487
DESCRIPTION:What do you do if a computational object (e.g.\, a document\,
a program trace) fails a specification? An obvious approach is to perform
a repair: modify the object minimally to get something that satisfies the
constraints. This approach has been extensively investigated in the databa
se community for relational integrity constraints\, and in the AI communit
y for propositional logics. Different modification operators have been con
sidered on the basis of the application scenarios. For instance\, a repair
of an XML document usually consists of applying to the underlying tree st
ructure a certain number of editing operations such as relabelings\, delet
ions\, and insertions of nodes. In this talk I will survey some results re
lated to the worst-case cost of repairing documents between regular specif
ications. Precisely\, I will focus on the number of edits that are needed
to get from a document (i.e.\, a word or a tree) that satisfies a source s
pecification (i.e.\, a regular language S) to some document that satisfies
a target specification (i.e.\, a regular language T). As this number may
well be unbounded\, I will consider the problem of determining those pairs
of languages (S\,T) such that one can get from any word/tree in S to a wo
rd/tree in T using a finite\, uniformly bounded number of editing operatio
ns. I will give effective characterizations of these pairs when S and T ar
e given by finite state automata (word case) or stepwise tree automata (tr
ee case)\, and derive some complexity bounds for the corresponding problem
s. Time permitting\, I will also talk about the normalized repair cost\; m
ore specifically\, about the problem of computing the worst-case repair co
st between two languages S and T normalized by the length of the input wor
d.\n\nThe presentation is based on joint works with Michael Benedikt\, Cri
stian Riveros\, Sławek Staworko\, and Pierre Bourhis.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:A New Proof of Simon’s Theorem\, and Separation by Piecewise Tes
table Languages - Howard Straubing\, Boston college
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130516T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130516T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:488
DESCRIPTION:I am going to present a brand-new (about a week old) proof of
the classic theorem of I. Simon showing the equivalence of piecewise testa
bility of regular languages and J-triviality of the syntactic monoid. Miko
laj Bojanczyk and I found this proof while contemplating recent results\,
discovered independently by Czerwinski-Martens-Masopust and by van Rooijen
-Zeitoun\, which show that one can determine in polynomial time in the siz
e of NFAs recognizing L and M\, whether or not L and M can be separated by
a piecewise testable language. (In particular\, if M is the complement of
L\, this gives an efficient algorithm for determining if a given language
is piecewise testable.) After giving the proof of Simon’s Theorem\, I w
ill explain this more general result.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tree walking automata - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130418T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130418T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:489
DESCRIPTION:Tree walking automata were introduced during the 70s as a mode
l for describing regular languages of trees [AU77]. The run of such an aut
omaton\, instead of being a tree as for standard tree automata\, form a pa
th in the input tree. At each step of the run\, the (unique) head of the a
utomato is located in some node\, and based on the current configuration o
f the tree and the current state of the automaton goes to one of the child
ren of the current node\, or go to the parent of the current node\, and ch
anges of states. Iterating this process\, the automaton walks a path in th
e tree\, possibly ending accepting the input tree. Tree walking automata a
re easy to show to define regular languages of finite trees.\n\nIn this ta
lk\, we will cover several subjects related to tree walking automata\, inc
luding\, the separation properties (deterministic tree walking automata ar
e strictly weaker than non-deterministic ones [BC06]\, which in turn are s
trictly weaker than regular languages [BC08]) and closure properties (unde
r complementation in particular [MSS06]). We will also present the models
of pebble automata and relate it to first-order logic with transitive clos
ure [EH99]. We will conclude with the separation of this logic from monadi
c logic over finite trees [BSSS06\,BS10].
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Transduction Hierarchy and Definable Orderings - Achim Blumens
ath\, RWTH Aachen
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130404T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130404T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:490
DESCRIPTION:I will give a survey on my recent work with Bruno Courcelle co
ncerning the expressive power of monadic second-order logic on certain gra
ph classes. In particular\, I will present our work on the transduction hi
erarchy\, a classification of graph classes according to their encoding po
wer with respect to transductions. I will also give an overview on more re
cent work on the definability of linear orderings on certain classes of gr
aphs. Here we aim at simple combinatorial characterisations of whether suc
h an ordering is definable or not.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Definability of uniformisation and choice in monadic second order
logic - Christof Löding\, RWTH Aachen
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130320T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130320T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:491
DESCRIPTION:In this talk I will prove that it is not possible to define a
choice function in monadic second-order logic (MSO) over the infinite bina
ry tree. Such a choice function would be given by a formula that has one f
ree set variable and one free element variable\, and for each non-empty se
t of nodes the formula becomes true for exactly one element from this set.
This result has first been obtained by Gurevich and Shelah in 1983 using
set theoretic methods. The proof presented in this talk is (in my opinion)
much simpler\, and is completely based on automata theoretic arguments.\n
\nA consequence of this result is that MSO-definable relations of infinite
trees cannot be uniformized in MSO (where a uniformization of a binary re
lation is a function that is a subset of the relation and has the same dom
ain as the relation). One can also use the result to show that there are n
ondeterministic automata on infinite trees that are not equivalent to an u
nambiguous automaton\, i.e.\, an automaton that has at most one accepting
run for each input.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Uniformization - Christian Choffrut\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130221T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130221T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:492
DESCRIPTION:To uniformize a binary relation means to find a partial functi
on whose graph lies in the relation and whose domain coincides with that o
f the relation. Said differently it consists of selecting a unique image f
or each element of the domain. Depending on the class of relations\, it is
possible or not to uniformize the relations by functions in the same clas
s.\n\nI will not give a survey\, rather talk of what I know of the topic\,
which is mainly binary rational relations over finite and infinite words
and some connected problems.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:The construction of Safra - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130207T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130207T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:493
DESCRIPTION:In this talk\, we will present the classical construction of S
afra\, which transforms non-deterministic Büchi automata to deterministic
Rabin automata. We will adopt the point of view of modern presentations o
f this result (in particular of Schewe)\, and cover the lower bound result
s.
LOCATION:4068
END:VEVENT
BEGIN:VEVENT
SUMMARY:Two lower bound techniques in formal verification - Stefan Göller
\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20130117T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20130117T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:494
DESCRIPTION:First\, I will talk about Defender’s Forcing\, a technique i
ntroduced by Jancar and Srba that is used for proving lower bounds in bisi
milarity checking of infinite state systems\, i.e. the problem\, given two
infinite state systems\, to decide whether they are bisimilar. I plan to
apply this simple but powerful technique to some classes of infinite state
systems for which simple representations exist\, such as for prefix-recog
nisable graphs\, Petri Nets or PA processes.\n\nSecond\, I will recall two
classical results from complexity theory (i) PSPACE is serializable meani
ng roughly that for determining whether a word lies in a fixed PSPACE lang
uage one only needs to check if the yield (the leaf string) of the computa
tion tree of an NP machine lies in a fixed regular language (ii) Convertin
g a natural number in binary to its Chinese remainder representation is in
NCˆ1. I plan to use these results for proving lower bounds for reachabil
ity problems and model checking problems for one-counter automata and time
d automata\, respectively.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:A topological proof of Gödel’s completeness theorem for first-o
rder logic - Sam Van Gool\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20121220T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20121220T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:495
DESCRIPTION:In the fifties of the previous century\, Rasiowa and Sikorski
gave a topological proof of Gödel’s completeness theorem for first-orde
r logic. Their proof ultimately relies on the Baire category theorem\, whi
ch is mainly known for its powerful applications in real and functional an
alysis. Therefore\, the application of Baire’s theorem to prove this fun
damental result in logic is a surprising and interesting one. The main goa
l of this talk will be to give an exposition of this elegant topological p
roof by Rasiowa and Sikorski.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Model Theoretic Proof of Completeness of an Axiomatization of Mo
nadic Second-Order Logic on Infinite Words - Colin Riba\, ENS Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20121213T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20121213T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:496
DESCRIPTION:We discuss the completeness of an axiomatization of Monadic Se
cond-Order Logic (MSO) on infinite words (or streams). By using model-theo
retic tools\, we give an alternative proof of D. Siefkes’ result that a
fragment with full comprehension and induction of second-order Peano’s a
rithmetic is complete w.r.t. the validity of MSO-formulas on streams. We r
ely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraissé method for He
nkin models of second-order arithmetic. Our main technical contribution is
an infinitary Feferman-Vaught Fusion of such models. We show it using Ram
seyan factorizations similar to those for standard infinite words. We also
discuss a Ramsey’s theorem for MSO-definable colorings\, and show that
in linearly ordered Henkin models\, Ramsey’s theorem for additive MSO-de
finable colorings implies Ramsey’s theorem for all MSO-definable colorin
gs.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Introduction to Communication Complexity - Frédéric Magniez\,
LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120614T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120614T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:497
DESCRIPTION:We will give a self-content course on the basics of Communicat
ion Complexity together with simple and elegant applications for proving l
ower bounds in different computational models. For instance\, we will give
a space time tradeoff for recognizing a palindrome on a Turing machine.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:The collapse of monadic second order logic over countable linear o
rderings - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120531T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120531T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:498
DESCRIPTION:This talk corresponds to a joint work with Olivier Carton and
Gabriele Puppis and provides a prolongation of the previous seminar. The s
ubject wil be the algebraic approach to monadic second order logic over in
finite words. We will in particular show how this notion of recognition is
equivalent to the logic. This techniques provide at the same time a colla
pse of the logic to the one with only one alternation of monadic quantifie
rs.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:The monadic theory of orderings - Thomas Colcombet\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120510T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120510T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:499
DESCRIPTION:In this talk\, we present the aproaches of Rabin (69) and Shel
ah (75) for deciding the monadic theory of the rationals with order.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games for Monadic Σ11 (EMSO) and probabilistic methods - Michel D
e Rougemont\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120503T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120503T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:500
DESCRIPTION:I’ll survey the classical Ehrenfeucht-Fraisse and Ajtai-Fagi
n games for this Logic. I’ll explain the role of the probabilistic metho
d to prove that s\,t-connexity is not Σ11 (EMSO) on graphs\, using the Aj
tai-Fagin games.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kamp's theorem - Olivier Carton\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120412T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120412T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:501
DESCRIPTION:Kamp’s theorem states the equivalence between temporal logic
s and temporal logics with past operators over complete linear orderings.
LOCATION:-
END:VEVENT
BEGIN:VEVENT
SUMMARY:Stability theory - Achim Blumensath\, LIAFA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20120326T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20120326T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:502
DESCRIPTION:-
LOCATION:submarine
END:VEVENT
BEGIN:VEVENT
SUMMARY:Proof complexity\, constraint satisfaction and graph isomorphism -
Joanna Ocremiak\, Université Denis Diderot - Paris 7
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180214T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180214T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:561
DESCRIPTION:The goal of my talk will be to present some results on the pow
er of various proof systems for the graph isomorphism problem and the cons
traint satisfaction problem. In order to do so I will give a short introdu
ction to proof complexity\, discuss different relaxations of the graph iso
morphism problem and the algebraic approach to the constraint satisfaction
problem. No prior knowledge on any of those topics is required.
LOCATION:4033
END:VEVENT
BEGIN:VEVENT
SUMMARY:Superpolynomial lower bound for complementing unambiguous automata
- Thomas Colcombet\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180509T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180509T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:591
DESCRIPTION:I will explain the proof of a result of Mikhail Raskin publish
ed this year (ICALP 2018) that solves a question open for more than a deca
de: what is the complexity of complementing an unambiguous automaton. \nTh
e result is that complementing an unambiguous automaton may require a supe
rpolynomial number of states\, even if the output automaton is non-determi
nistic. The opposite fact was conjectured.
LOCATION:3014
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 1/7: Tw
o-player Turn-based Stochastic Games - Uri Zwick\, Blavatnik School of Com
puter Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190320T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190320T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:832
DESCRIPTION:In the first lecture we define the two-player Turn-Based Stoch
astic \nGames (TBSGs)\, the most general games considered in this lecture
series. \nWe define the objectives of the two players\, the strategies tha
t they \ncan use\, and define the values of the games. We then consider al
gorithms \nfor finding the values and optimal strategies\, first in one-pl
ayer games \nand then in two-player games. While for one-player games poly
nomial time \nalgorithms are known\, for most two-player games no polynomi
al time \nalgorithms are currently known.\n\n\n[[https://www.irif.fr/_medi
a/actualites/ressources/zwick_program.pdf]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 2/7: M
ean Payoff games and Energy Games - Uri Zwick\, Blavatnik School of Comput
er Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190327T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190327T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:833
DESCRIPTION:In this talk we consider non-stochastic versions of the games
introduced \nin the first lecture\, namely Mean Payoff Games (MPGs) and En
ergy Games \n(EGs). We show reductions between these two games. We then de
scribe a \npseudo-polynomial time algorithm of Brim et al. for EGs\, and h
ence also \nMPGs\n\n[[https://www.irif.fr/_media/actualites/ressources/zwi
ck_program.pdf]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 3/7: Ra
ndomized sub-exponential time algorithm - Uri Zwick\, Blavatnik School of
Computer Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190403T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190403T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:834
DESCRIPTION:In this talk we present an elegant randomized algorithm that s
olves all \nthe games we consider in //sub-exponential// time. This is cur
rently \nthe fastest known algorithm for TBSGs\, and also for MPGs and EGs
\, when \nthere is no restriction on the edge costs. The algorithm is an \
nadaptation of a randomized algorithms of Kalai and Matousek\, Sharir and
\nWelzl for solving linear programs.\nWe also mention relations to abstrac
tions of Linear Programming \nabstractions.\n\n[[https://www.irif.fr/_medi
a/actualites/ressources/zwick_program.pdf]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 4/7: Ac
yclic Unique Sink Orientations (AUSOs) - Uri Zwick\, Blavatnik School of C
omputer Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190410T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190410T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:835
DESCRIPTION:In this lecture we consider Acyclic Unique Sink Orientations (
AUSOs) an \nabstraction related to linear programming that also captures t
he games \nwe are interested in. We present algorithms for finding the sin
k of an \nAUSOs\, which directly translate to algorithms for solving games
.\n\n\n[[https://www.irif.fr/_media/actualites/ressources/zwick_program.pd
f]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 5/7: Pa
rity Games - Uri Zwick\, Blavatnik School of Computer Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190417T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190417T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:836
DESCRIPTION:In this lecture we consider Parity Games (PGs)\, a very specia
l case of \nMPGs\, with many relations to automata on infinite words and t
o automatic \nverification. In a recent breakthrough Calude et al. obtaine
d a \nquasi-polynomial time algorithm for solving PGs. We will describe on
e of \nthe existing variants of their algorithm.\n\n\n[[https://www.irif.f
r/_media/actualites/ressources/zwick_program.pdf]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 6/7: Lo
wer bounds for Policy Iteration - Uri Zwick\, Blavatnik School of Computer
Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190515T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190515T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:837
DESCRIPTION:Policy Iteration\, introduced in the first lecture\, is a very
natural \nclass of algorithms for solving TBSGs. Policy Iteration algorit
hms work \nvery well in practice. However\, we now know that their worst-c
ase \ncomplexity is exponential.\nWe will present such lower bounds.\n\n\n
[[https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf]]
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games on Graphs and Linear Programming Abstractions\, Part 7/7: Lo
wer bounds for Random-Facet and Random-Edge - Uri Zwick\, Blavatnik School
of Computer Science
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190522T141500
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190522T151500
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:838
DESCRIPTION:In this lecture we present sub-exponential lower bounds for Ra
ndom-Facet \n(the randomized algorithm considered in Lecture 3) and Random
-Edge.\n\n\n[[https://www.irif.fr/_media/actualites/ressources/zwick_progr
am.pdf]]
LOCATION:3052
END:VEVENT
END:VCALENDAR