CINXE.COM

<!DOCTYPE html> <html xmlns="http://www.w3.org/1999/xhtml" lang="en" dir="ltr" class="no-js"> <head> <meta charset="UTF-8" /> <title>Logic, automata, algebra and games</title>  <script> var _paq = window._paq = window._paq || []; /* tracker methods like "setCustomDimension" should be called before "trackPageView" */ _paq.push(['trackPageView']); _paq.push(['enableLinkTracking']); (function() { var u="//apps.roulois.fr/matomo/"; _paq.push(['setTrackerUrl', u+'matomo.php']); _paq.push(['setSiteId', '1']); var d=document, g=d.createElement('script'), s=d.getElementsByTagName('script')[0]; g.async=true; g.src=u+'matomo.js'; s.parentNode.insertBefore(g,s); })(); </script>  <script>(function(H){H.className=H.className.replace(/\bno-js\b/,'js')})(document.documentElement)</script> <meta name="viewport" content="width=device-width,initial-scale=1" /> <link rel="shortcut icon" href="https://www.irif.fr/_media/favicon.ico" /> <link rel="apple-touch-icon" href="https://www.irif.fr/_media/apple-touch-icon.png" /> <meta name="generator" content="DokuWiki"/> <meta name="robots" content="index,follow"/> <meta name="keywords" content="en,seminaires,laag,index"/> <link rel="search" type="application/opensearchdescription+xml" href="https://www.irif.fr/lib/exe/opensearch.php" title=""/> <link rel="start" href="https://www.irif.fr/"/> <link rel="contents" href="https://www.irif.fr/en/seminaires/laag/index?do=index" title="Sitemap"/> <link rel="manifest" href="https://www.irif.fr/lib/exe/manifest.php"/> <link rel="alternate" type="text/html" title="Plain HTML" href="https://www.irif.fr/_export/xhtml/en/seminaires/laag/index"/> <link rel="alternate" type="text/plain" title="Wiki Markup" href="https://www.irif.fr/_export/raw/en/seminaires/laag/index"/> <link rel="canonical" href="https://www.irif.fr/en/seminaires/laag/index"/> <link rel="stylesheet" href="https://www.irif.fr/lib/exe/css.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/css/fixedHeader.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/css/fixedColumns.dataTables.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/css/dataTables.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/css/buttons.bootstrap.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/font-awesome/css/font-awesome.min.css"/> <link type="text/css" rel="stylesheet" href="https://www.irif.fr/lib/plugins/icons/assets/material-design-icons/css/materialdesignicons.min.css"/>  <script >/*<![CDATA[*/var NS='en:seminaires:laag';var JSINFO = {"plugin":{"datatables":{"config":{"dom":"lBfrtip","language":{"url":"https:\/\/www.irif.fr\/lib\/plugins\/datatables\/assets\/datatables.net-i18n\/en-GB.json"}},"enableForAllTables":1}},"move_renameokay":false,"move_allowrename":false,"bootstrap3":{"mode":"show","toc":[],"config":{"collapsibleSections":0,"fixedTopNavbar":1,"showSemanticPopup":0,"sidebarOnNavbar":1,"tagsOnTop":1,"tocAffix":1,"tocCollapseOnScroll":1,"tocCollapsed":0,"tocLayout":"default","useAnchorJS":1,"useAlternativeToolbarIcons":1}},"id":"en:seminaires:laag:index","namespace":"en:seminaires:laag","ACT":"show","useHeadingNavigation":1,"useHeadingContent":1}; /*!]]>*/</script> <script src="https://www.irif.fr/lib/exe/jquery.php?tseed=34a552433bc33cc9c3bc32527289a0b2" defer="defer"></script> <script src="https://www.irif.fr/lib/exe/js.php?t=bootstrap3&tseed=999b1f07158911a883ed4b945a522775&lang=en" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/jquery.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedheader-dt/js/fixedHeader.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-fixedcolumns-dt/js/fixedColumns.dataTables.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/dataTables.buttons.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.html5.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.print.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/jszip/jszip.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/pdfmake.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/pdfmake/vfs_fonts.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net/js/dataTables.bootstrap.min.js" defer="defer"></script> <script type="text/javascript" src="https://www.irif.fr/lib/plugins/datatables/assets/datatables.net-buttons/js/buttons.bootstrap.min.js" defer="defer"></script> <script type="text/x-mathjax-config">/*<![CDATA[*/MathJax.Hub.Config({ tex2jax: { inlineMath: [ ["$","$"], ["\$","\$"] ], displayMath: [ ["$$","$$"], ["\\[","\\]"] ], processEscapes: true } }); /*!]]>*/</script> <script type="text/javascript" charset="utf-8" src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.9/MathJax.js?config=TeX-AMS_CHTML.js"></script>  <style type="text/css">@media screen { body { margin-top: 60px; } #dw__toc.affix { top: 50px; position: fixed !important; } #dw__toc .nav .nav .nav { display: none; } }</style>  </head> <body class="simplex dokuwiki mode_show tpl_bootstrap3 dw-fluid-container" data-page-id="en:seminaires:laag:index"><div class="dokuwiki"> <header id="dokuwiki__header" class="dw-container dokuwiki container-fluid mx-5">  <nav id="dw__navbar" class="navbar navbar-fixed-top navbar-inverse" role="navigation"> <div class="dw-container container-fluid mx-5"> <div class="navbar-header"> <button class="navbar-toggle" type="button" data-toggle="collapse" data-target=".navbar-collapse"> <span class="icon-bar"></span> <span class="icon-bar"></span> <span class="icon-bar"></span> </button> <a class="navbar-brand d-flex align-items-center" href="https://www.irif.fr/index" accesskey="h" title=""><img id="dw__logo" class="pull-left h-100 mr-4" alt="" src="https://www.irif.fr/_media/logo.png" /><div class="pull-right"><div id="dw__title"></div></div></a> </div> <div class="collapse navbar-collapse"> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">INFORMATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/informations/presentation" class="wikilink1" title="en:informations:presentation" >Presentation</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/contacts" class="wikilink1" title="en:informations:contacts" >Contact and access</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/charte" class="wikilink1" title="en:informations:charte" >IRIF Members Charter</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/egalite-fh/index" class="wikilink1" title="en:egalite-fh:index" >Equality</a> </li> <li class="level2"> <a href="https://www.irif.fr/environnement/index" class="wikilink1" title="environnement:index" >Environment</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/annuaire" class="wikilink1" title="en:informations:annuaire" >Directory</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/informations/mentorat" class="wikilink1" title="en:informations:mentorat" >IRIF’s mentoring program</a> </li> <li class="level2"> <a href="https://www.irif.fr/informations/childcare" class="wikilink1" title="informations:childcare" >Childcare program</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">RESEARCH <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/asd/index" class="wikilink1" title="en:poles:asd:index" >Algorithms and discrete structures</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/algocomp/index" class="wikilink1" title="en:equipes:algocomp:index" >Algorithms and complexity</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/combi/index" class="wikilink1" title="en:equipes:combi:index" >Combinatorics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/distribue/index" class="wikilink1" title="en:equipes:distribue:index" >Distributed computing</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/graphes/index" class="wikilink1" title="en:equipes:graphes:index" >Theory and algorithmics of graphs</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/asv/index" class="wikilink1" title="en:poles:asv:index" >Automata, structures and verification</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/automates/index" class="wikilink1" title="en:equipes:automates:index" >Automata and applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/verif/index" class="wikilink1" title="en:equipes:verif:index" >Modeling and verification</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/poles/pps/index" class="wikilink1" title="en:poles:pps:index" >Proofs, programs and systems</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/algebre/index" class="wikilink1" title="en:equipes:algebre:index" >Algebra and computation</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/programmes/index" class="wikilink1" title="en:equipes:programmes:index" >Programs and Languages (PL)</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/preuves/index" class="wikilink1" title="en:equipes:preuves:index" >Proofs and programs</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/equipes/picube/index" class="wikilink1" title="en:equipes:picube:index" >Picube (Inria)</a><hr/> </li> <li class="level2"> <strong><a href="https://cnrs.hal.science/IRIF#" class="" title="https://cnrs.hal.science/IRIF#" rel="ugc nofollow">PUBLICATIONS (hal)</a></strong><br/> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node active dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">EVENTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/evenements" class="wikilink1" title="en:seminaires:evenements" >IRIF events</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/irif/index" class="wikilink1" title="en:seminaires:irif:index" >IRIF Distinguished Talks Series</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/rencontres/irif/index" class="wikilink1" title="en:rencontres:irif:index" >IRIF days</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/rencontres/poles/index" class="wikilink1" title="en:rencontres:poles:index" >Pole meetings</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/env/index" class="wikilink1" title="en:seminaires:env:index" >IRIF and environment group</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/seminaires" class="wikilink1" title="en:seminaires:seminaires" >Research seminars</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/algocomp/index" class="wikilink1" title="en:seminaires:algocomp:index" >Algorithms and complexity</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/asd/index" class="wikilink1" title="en:seminaires:asd:index" >Algorithms and discrete structures</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/automates/index" class="wikilink1" title="en:seminaires:automates:index" >Automata</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/combi/index" class="wikilink1" title="en:seminaires:combi:index" >Enumerative and analytic combinatorics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/adg/index" class="wikilink1" title="en:seminaires:adg:index" >Graphs and distributed computing</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/picube/index" class="wikilink1" title="en:seminaires:picube:index" >Formath</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/pps/index" class="wikilink1" title="en:seminaires:pps:index" >Proofs, programs and systems</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/verif/index" class="wikilink1" title="en:seminaires:verif:index" >Verification</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/doctorants/index" class="wikilink1" title="en:seminaires:doctorants:index" >Non-permanent members’ seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/onlineseminars" class="wikilink1" title="en:seminaires:onlineseminars" >Online seminars</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/greta/index" class="wikilink1" title="en:seminaires:greta:index" >Graph Transformation Theory and Applications</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/numeration/index" class="wikilink1" title="en:seminaires:numeration:index" >One world numeration seminar</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/gt" class="wikilink1" title="en:seminaires:gt" >Working groups</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/cat/index" class="wikilink1" title="en:seminaires:cat:index" >Higher categories, polygraphs and homotopy</a> </li> <li class="level2 active"> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-curid="true">Logic, automata, algebra and games</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/programmation/index" class="wikilink1" title="en:seminaires:programmation:index" >Programming</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/semantique/index" class="wikilink1" title="en:seminaires:semantique:index" >Semantics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/sms/index" class="wikilink1" title="en:seminaires:sms:index" >Syntax Meets Semantics</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/hott/index" class="wikilink1" title="en:seminaires:hott:index" >Type theory and homotopy theory</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/types/index" class="wikilink1" title="en:seminaires:types:index" >Type theory and realisability</a> </li> <li class="level2"> <strong><a href="https://www.irif.fr/en/seminaires/soutenances" class="wikilink1" title="en:seminaires:soutenances" >Defences</a></strong> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/these/index" class="wikilink1" title="en:seminaires:these:index" >PhD defences</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/seminaires/hdr/index" class="wikilink1" title="en:seminaires:hdr:index" >Habilitation defences</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">MEDIATION <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/mediation/fdls" class="wikilink1" title="en:mediation:fdls" >Fête de la Science</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/mediation/scolaire" class="wikilink1" title="en:mediation:scolaire" >Middle/High school internships</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/portraits/index" class="wikilink1" title="en:portraits:index" >Research profiles</a> </li> <li class="level2"> <a href="https://icalp2022.irif.fr/?page_id=1111" class="" title="https://icalp2022.irif.fr/?page_id=1111" rel="ugc nofollow">50 Years Exhibitation</a> </li> <li class="level2"> <a href="https://qubobs.irif.fr" class="" title="https://qubobs.irif.fr" rel="ugc nofollow">Projet QuBOBS (quantum computing explained)</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">HIGHLIGHTS <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/distinctions/index" class="wikilink1" title="en:distinctions:index" >Awards and Honors</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/logiciels/index" class="wikilink1" title="en:logiciels:index" >Software</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/contrats/index" class="wikilink1" title="en:contrats:index" >Grants</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/international/index" class="wikilink1" title="en:international:index" >International Collaborations</a> </li> <li class="level2"> <a href="https://epit.irif.fr" class="" title="https://epit.irif.fr" rel="ugc nofollow">The EPIT Research School</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/formation/index" class="wikilink1" title="en:formation:index" >Academics</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1 node dropdown"><a href="#" class="dropdown-toggle" data-target="#" data-toggle="dropdown" role="button" aria-haspopup="true" aria-expanded="false">JOIN US <span class="caret"></span></a> <ul class="dropdown-menu" role="menu"> <li class="level2"> <a href="https://www.irif.fr/en/informations/visit" class="wikilink1" title="en:informations:visit" >Visitor program</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/admin" class="wikilink1" title="en:postes:admin" >Research support position</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/universite" class="wikilink1" title="en:postes:universite" >Faculty members</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/chercheur" class="wikilink1" title="en:postes:chercheur" >Researchers</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/postdoc" class="wikilink1" title="en:postes:postdoc" >Postdocs</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/ater" class="wikilink1" title="en:postes:ater" >Teaching assistants</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/these" class="wikilink1" title="en:postes:these" >PhD Studies</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/stage" class="wikilink1" title="en:postes:stage" >Master Internships</a> </li> <li class="level2"> <a href="https://www.irif.fr/en/postes/stage-scolaire" class="wikilink1" title="en:postes:stage-scolaire" >Middle/High school internships</a> </li> </ul> </li> </ul> <ul class="nav navbar-nav"> <li class="level1"> <a href="https://www.irif.fr/en/intranet/index" class="wikilink1" title="en:intranet:index" >INTRANET</a> </li> </ul> <div class="navbar-right" id="dw__navbar_items">  <ul class="nav navbar-nav" id="dw__translation"> <li class="dropdown"> <a href="" class="dropdown-toggle" data-target="#" data-toggle="dropdown" title="Translations of this page" role="button" aria-haspopup="true" aria-expanded="false"> <span class="iconify" data-icon="mdi:flag"></span> <span class="hidden-lg hidden-md hidden-sm">Translations of this page</span><span class="caret"></span> </a> <ul class="dropdown-menu" role="menu"> <li class="dropdown-header hidden-xs hidden-sm"> <span class="iconify" data-icon="mdi:flag"></span> Translations of this page </li> <li><div class='li'><a href="https://www.irif.fr/seminaires/laag/index" class="wikilink1 flag" title="Français"><img src="https://www.irif.fr/lib/plugins/translation/flags/fr.gif" alt="fr" height="11" />Français</a></li><li><div class='li cur'><a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1 cur flag" title="English"><img src="https://www.irif.fr/lib/plugins/translation/flags/en.gif" alt="en" height="11" />English</a></li> </ul> </li> </ul>  <ul class="nav navbar-nav"> <li> <span class="dw__actions dw-action-icon"> <a href="https://www.irif.fr/en/seminaires/laag/index?do=login&sectok=" title="Log In" rel="nofollow" class="menuitem login btn btn-default navbar-btn"><svg xmlns="http://www.w3.org/2000/svg" width="24" height="24" viewBox="0 0 24 24"><path d="M10 17.25V14H3v-4h7V6.75L15.25 12 10 17.25M8 2h9a2 2 0 0 1 2 2v16a2 2 0 0 1-2 2H8a2 2 0 0 1-2-2v-4h2v4h9V4H8v4H6V4a2 2 0 0 1 2-2z"/></svg><span class=""> Log In</span></a> </span> </li> </ul> </div> </div> </div> </nav>  </header> <a name="dokuwiki__top" id="dokuwiki__top"></a> <main role="main" class="dw-container pb-5 dokuwiki container-fluid mx-5"> <div id="dokuwiki__pageheader"> <p class="text-right"> </p> <div id="dw__msgarea" class="small"> </div> </div> <div class="row"> <article id="dokuwiki__content" class="col-sm-12 col-md-12 " itemscope itemtype="http://schema.org/Article" itemref="dw__license">  <div class="no-panel" itemprop="articleBody"> <div class="page "> <div class="dw-content-page "><div class="dw-content"><div class="plugin_include_content plugin_include__en:seminaires:laag:indexheader" id="plugin_include__en__seminaires__laag__indexheader"> <div class="datatemplateentry"> <p> <br/> </p> <div class="wrap_right plugin_wrap"> <p> <div class="bs-wrap bs-wrap-well well"> <span class="bs-wrap bs-wrap-button" data-btn-type="primary" data-btn-size="sm" data-btn-disabled="1">Working group</span> </p> <div class=""> <p> <span class="bs-wrap bs-wrap-label label label-default">Pole</span> <a href="https://www.irif.fr/en/seminaires/laag/0_pageid" class="wikilink2" title="en:seminaires:laag:0_pageid" rel="nofollow" data-wiki-id="en:seminaires:laag:0_pageid"><a href="https://www.irif.fr/en/poles/asv/index" class="wikilink1" title="en:poles:asv:index" data-wiki-id="en:poles:asv:index">Automata, structures and verification</a></a><br/> </p> </div><div class=""> <p> <span class="bs-wrap bs-wrap-label label label-default">Thematic team</span> <a href="https://www.irif.fr/en/seminaires/laag/0_pageid" class="wikilink2" title="en:seminaires:laag:0_pageid" rel="nofollow" data-wiki-id="en:seminaires:laag:0_pageid"><a href="https://www.irif.fr/en/equipes/automates/index" class="wikilink1" title="en:equipes:automates:index" data-wiki-id="en:equipes:automates:index">Automata and applications</a></a><br/> </p> </div> <p> </div> </p> <div style='display:none'><div class="wrap_right plugin_wrap"> <p> <span class="bs-wrap bs-wrap-button" data-btn-type="default"><a href="https://www.irif.fr/admindb/seminaires/" class="urlextern" title="https://www.irif.fr/admindb/seminaires/" rel="ugc nofollow">Manage talks</a></span> </p> </div></div></div> <h2 id="logic_automata_algebra_and_games" class=" page-header pb-3 mb-4 mt-5">Logic, automata, algebra and games</h2> <div class="level2"> <p> <br/> </p> </div> <h4 id="day_hour_and_place">Day, hour and place</h4> <div class="level4"> <p> Wednesday at 2pm, room 4033 </p> <p> The <a href="http://www.irif.fr/_media/ical/laag.ics" class="urlextern" title="http://www.irif.fr/_media/ical/laag.ics" rel="ugc nofollow">calendar</a> of events (iCal format). <br/> In order to add the event calendar to your favorite agenda, subscribe to the calendar by using this link. </p> <p> <br/> </p> </div> <h4 id="contact_s">Contact(s)</h4> <div class="level4"> <div class=""> <p> <a href="https://www.irif.fr/~colcombe/" class="urlextern" title="https://www.irif.fr/~colcombe/" rel="ugc nofollow">Thomas Colcombet</a><br/> <a href="https://www.irif.fr/~schmitz/" class="urlextern" title="https://www.irif.fr/~schmitz/" rel="ugc nofollow">Sylvain Schmitz</a><br/> <a href="http://www.samvangool.net" class="urlextern" title="http://www.samvangool.net" rel="ugc nofollow">Sam van Gool</a><br/> </p> </div> </div> </div><div class="level0"> <p> The goal of this reading group is to present in two hours blackboard sessions for some classical or more recent results concerning logic, automata theory, algebraic methods and games. </p> </div> <h0 class="sectionedit3" id="organization">Organization</h0> <div class="level0"> <p> The reading group happens the Wednesday from 2pm to 4pm, room 4033, building Sophie Germain, every two weeks on average. </p> </div> </div> <p> <br/> </p> <h3 class="sectionedit4 page-header pb-3 mb-4 mt-5" id="previous_talks">Previous talks</h3> <div class="level3"> <p> <br/> </p> </div> <h4 id="year_2019">Year 2019</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2019" id="plugin_include__en__seminaires__laag__laag2019"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday May 22, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 7/7: Lower bounds for Random-Facet and Random-Edge</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3614"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3614"><div class="bs-wrap bs-wrap-well well well-sm"> In this lecture we present sub-exponential lower bounds for Random-Facet (the randomized algorithm considered in Lecture 3) and Random-Edge. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday May 15, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 6/7: Lower bounds for Policy Iteration</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3615"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3615"><div class="bs-wrap bs-wrap-well well well-sm"> Policy Iteration, introduced in the first lecture, is a very natural class of algorithms for solving TBSGs. Policy Iteration algorithms work very well in practice. However, we now know that their worst-case complexity is exponential. We will present such lower bounds. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday April 17, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 5/7: Parity Games</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3616"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3616"><div class="bs-wrap bs-wrap-well well well-sm"> In this lecture we consider Parity Games (PGs), a very special case of MPGs, with many relations to automata on infinite words and to automatic verification. In a recent breakthrough Calude et al. obtained a quasi-polynomial time algorithm for solving PGs. We will describe one of the existing variants of their algorithm. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday April 10, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 4/7: Acyclic Unique Sink Orientations (AUSOs)</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3617"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3617"><div class="bs-wrap bs-wrap-well well well-sm"> In this lecture we consider Acyclic Unique Sink Orientations (AUSOs) an abstraction related to linear programming that also captures the games we are interested in. We present algorithms for finding the sink of an AUSOs, which directly translate to algorithms for solving games. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday April 3, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 3/7: Randomized sub-exponential time algorithm</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3618"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3618"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk we present an elegant randomized algorithm that solves all the games we consider in <em>sub-exponential</em> time. This is currently the fastest known algorithm for TBSGs, and also for MPGs and EGs, when there is no restriction on the edge costs. The algorithm is an adaptation of a randomized algorithms of Kalai and Matousek, Sharir and Welzl for solving linear programs. We also mention relations to abstractions of Linear Programming abstractions. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday March 27, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 2/7: Mean Payoff games and Energy Games</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3619"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3619"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk we consider non-stochastic versions of the games introduced in the first lecture, namely Mean Payoff Games (MPGs) and Energy Games (EGs). We show reductions between these two games. We then describe a pseudo-polynomial time algorithm of Brim et al. for EGs, and hence also MPGs <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday March 20, 2019, 2:15PM, 3052<br/> <strong>Uri Zwick</strong> (Blavatnik School of Computer Science) <em>Games on Graphs and Linear Programming Abstractions, Part 1/7: Two-player Turn-based Stochastic Games</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3620"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3620"><div class="bs-wrap bs-wrap-well well well-sm"> In the first lecture we define the two-player Turn-Based Stochastic Games (TBSGs), the most general games considered in this lecture series. We define the objectives of the two players, the strategies that they can use, and define the values of the games. We then consider algorithms for finding the values and optimal strategies, first in one-player games and then in two-player games. While for one-player games polynomial time algorithms are known, for most two-player games no polynomial time algorithms are currently known. <p> <a href="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" class="urlextern" title="https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf" rel="ugc nofollow">https://www.irif.fr/_media/actualites/ressources/zwick_program.pdf</a> </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2018">Year 2018</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2018" id="plugin_include__en__seminaires__laag__laag2018"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday May 9, 2018, 2PM, 3014<br/> <strong>Thomas Colcombet</strong> (IRIF) <em>Superpolynomial lower bound for complementing unambiguous automata</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3621"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3621"><div class="bs-wrap bs-wrap-well well well-sm"> I will explain the proof of a result of Mikhail Raskin published this year (ICALP 2018) that solves a question open for more than a decade: what is the complexity of complementing an unambiguous automaton. The result is that complementing an unambiguous automaton may require a superpolynomial number of states, even if the output automaton is non-deterministic. The opposite fact was conjectured. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday March 14, 2018, 2PM, 4033<br/> <strong>Joanna Ochremiak</strong> (Université Denis Diderot - Paris 7) <em>Proof complexity, constraint satisfaction and graph isomorphism</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3622"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3622"><div class="bs-wrap bs-wrap-well well well-sm"> In this second part of my talk I will discuss the algebraic approach to the constraint satisfaction problem (CSP), a framework which was very recently used to confirm the famous Feder-Vardi CSP dichotomy conjecture. I will also indicate how this approach can be employed to analyse the power of various proof systems for CSPs. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday February 14, 2018, 2PM, 4033<br/> <strong>Joanna Ocremiak</strong> (Université Denis Diderot - Paris 7) <em>Proof complexity, constraint satisfaction and graph isomorphism</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3623"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3623"><div class="bs-wrap bs-wrap-well well well-sm"> The goal of my talk will be to present some results on the power of various proof systems for the graph isomorphism problem and the constraint satisfaction problem. In order to do so I will give a short introduction to proof complexity, discuss different relaxations of the graph isomorphism problem and the algebraic approach to the constraint satisfaction problem. No prior knowledge on any of those topics is required. </div> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2017">Year 2017</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2017" id="plugin_include__en__seminaires__laag__laag2017"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday November 23, 2017, 10AM, 4033<br/> <strong>Nathanaël Fijlakow</strong> (Turing Institute / CNRS) <em>Quasi-polynomial algorithms for parity games</em> <br/> </p> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2016">Year 2016</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2016" id="plugin_include__en__seminaires__laag__laag2016"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday June 16, 2016, 10:30AM, 4033<br/> <strong>Florent Capelli</strong> (Liafa) <em>Lyndon’s theorem</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3624"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3624"><div class="bs-wrap bs-wrap-well well well-sm"> A first-order formula is positive if it does not contain any negations. 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′ also satisfies the formula. Lyndon’s theorem states that all first-order formulae 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. <p> In 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). </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday February 4, 2016, 10:30AM, 4033<br/> <strong>Christoph Haase</strong> (LSV) <em>A Survey on Classical and Novel Results on Presburger Arithmetic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3625"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3625"><div class="bs-wrap bs-wrap-well well well-sm"> Presburger arithmetic is the first-order theory of the natural numbers with addition and order. This theory was shown decidable by M. Presburger in 1929. In the 1960s, Presburger arithmetic was studied in the context of formal language theory. Two of the main results from this period are that the sets of natural numbers definable in Presburger arithmetic are the so-called semi-linear sets, and that Parikh images of languages generated by context-free grammars are semi-linear and hence Presburger-definable. Subsequently, from the 1970s onwards the computational complexity of Presburger arithmetic received interest. The landmark results from this period are a doubly exponential lower bound shown by Fischer and Rabin in 1974 and a triply-exponential upper bound shown by Oppen in 1978. The 1980ies brought a more fine-grained complexity analysis of (fragments of) Presburger 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 used for showing new lower bounds for equivalence problems for commutative grammars. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday January 21, 2016, 10:30AM, 4033<br/> <strong>Christoph Haase</strong> (LSV) <em>A Survey on Classical and Novel Results on Presburger Arithmetic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3626"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3626"><div class="bs-wrap bs-wrap-well well well-sm"> First part </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday January 7, 2016, 10:30AM, 4033<br/> <strong>Sylvain Schmitz</strong> (LSV) <em>Ideals in VAS Reachability</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3627"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3627"><div class="bs-wrap bs-wrap-well well well-sm"> The decidability of the reachability problem for vector addition systems is a notoriously difficult result. First shown by Mayr in 1981 after a decade of unsuccessful attempts and partial results, its proof has been simplified and refined several times, by Kosaraju, Reutenauer, and Lambert, and re-proven by very different techniques by Leroux in 2012. The principles behind the original proof remained however obscure. <p> In this seminar, I will present the ideas behind the algorithms of Mayr, Kosaraju, and Lambert (the KLM algorithm) in the light of ideals of well-quasi-orders. The interest here is that ideals provide a semantics to the structures manipulated in the KLM algorithm, bringing some new understanding to its proof of correctness. </p> <p> Joint work with Jérôme Leroux (LaBRI) presented at LICS’15; see <a href="http://arxiv.org/abs/1503.00745" class="urlextern" title="http://arxiv.org/abs/1503.00745" rel="ugc nofollow">http://arxiv.org/abs/1503.00745</a> </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2015">Year 2015</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2015" id="plugin_include__en__seminaires__laag__laag2015"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday December 17, 2015, 10:30AM, 4033<br/> <strong>Ranko Lazic</strong> (Warwick university) <em>Rackoff’s Coverability Technique</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3628"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3628"><div class="bs-wrap bs-wrap-well well well-sm"> Rackoff’s small witness property for the coverability problem is the standard means to prove tight upper bounds in vector addition systems (VAS) and many extensions. We show how to derive the same bounds directly 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 structural invariant in the VAS case. The same reasoning readily generalises to several VAS extensions. <p> Joint work with Sylvain Schmitz presented at RP ’15; see <a href="https://hal.inria.fr/hal-01176755/" class="urlextern" title="https://hal.inria.fr/hal-01176755/" rel="ugc nofollow">https://hal.inria.fr/hal-01176755/</a>. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday December 3, 2015, 10:30AM, 2015<br/> <strong>Sylvain Schmitz</strong> (LSV) <em>Ideals of Well-Quasi-Orders</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3629"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3629"><div class="bs-wrap bs-wrap-well well well-sm"> The purpose of this seminar is to introduce the notion of ideals of well-quasi-orders. These irreducible downwards-closed sets of elements 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 of downwards-closed sets, in the same way as bases of minimal elements provide representations of upwards-closed sets. <p> After defining ideals and establishing some of their properties, I will illustrate their use in a concrete setting. I will present some recent results by Czerwiński, Martens, 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. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday November 12, 2015, 10:30AM, 2015<br/> <strong>Luc Segoufin</strong> (LSV) <em>Abiteboul-Vianu theorem</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3630"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3630"><div class="bs-wrap bs-wrap-well well well-sm"> Descriptive complexity measure a problem in terms of the difficulty to express it. At first look this seems to have nothing to do with computational measures such as time and space. However it does have intimate links with classical computational complexity. <p> The most celebrated one is Fagin’s theorem linking the complexity class NP with the expressive power of existential second-order logic. </p> <p> In this lecture we will study the Abiteboul-Vianu theorem saying that the separation of PTime and PSpace can be rephrased in terms of expressive powers of partial fixpoints versus least fixpoints. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday November 5, 2015, 10:30AM, 2015<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>“À la Bojańcyk” proof of limitedness</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3631"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3631"><div class="bs-wrap bs-wrap-well well well-sm"> The limitedness is a question of boundedness: given a function from words to integers described by some suitable model of finite state machines (distance automata, B-automata, …), determine whether the function it computes is bounded. It happens that for distance automata [Hashiguchi81, 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 describe L by means of a regular expression with nesting of Kleene stars bounded by k). <p> In 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 duration, 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. </p> <p> The decidability of limitedness was already presented in the LAAG seminar (using the algebraic approach of stabilization monoids), but the proof here is entirely different. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday July 1, 2015, 10AM, 4068<br/> <strong>Stefan Göller</strong> (LSV) <em>Decidability of DPDA equivalence, part IV</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3632"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3632"><div class="bs-wrap bs-wrap-well well well-sm"> These two talks will continue the study of the equivalence problem of deterministic pushdown automata (DPDA). <p> The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive. </p> <p> More precisely, we will present a recent paper by Jancar that shows 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 height. </p> <p> As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars. </p> <p> This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well. </p> <p> These talks will be completely self-contained and require no background knowledge. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday June 17, 2015, 10:30AM, 4068<br/> <strong>Stefan Göller</strong> (LSV) <em>Decidability of DPDA equivalence, part III</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3633"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3633"><div class="bs-wrap bs-wrap-well well well-sm"> These two talks will continue the study of the equivalence problem of deterministic pushdown automata (DPDA). <p> The main focus of these talks will be on the computational complexity of this problem. We will give a proof of Stirling’s result that DPDA equivalence is primitive recursive. </p> <p> More precisely, we will present a recent paper by Jancar that shows 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 height. </p> <p> As in Arnaud’s talk we will view DPDA equivalence in terms of trace equivalence of deterministic first-order grammars. </p> <p> This talk aims at going hand-in-hand with Arnaud’s talk but is intended to be self-contained as well. </p> <p> These talks will be completely self-contained and require no background knowledge. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday June 3, 2015, 10:30AM, 4068a<br/> <strong>Arnaud Carayol</strong> (LIGM) <em>Decidability of DPDA equivalence, part II</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3634"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3634"><div class="bs-wrap bs-wrap-well well well-sm"> In this series of talks, we will present a proof of the decidability of the equivalence problem for deterministic pushdown automata. Namely given two deterministic pushdown automata, it is decidable if they accept the same language. This result was first proved by Géraud Sénizergues in 1997. His proof consists in two semi-decision procedures and hence while establishing decidability does not give an upper-bound on the complexity of the problem. In 2002, Colin Stirling gave a primitive recursive algorithm to decide the problem. <p> The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present 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 procedures. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday May 27, 2015, 10:30AM, 4068a<br/> <strong>Arnaud Carayol</strong> (LIGM) <em>Decidability of DPDA equivalence, part I</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3635"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3635"><div class="bs-wrap bs-wrap-well well well-sm"> In this series of talks, we will present a proof of the decidability of the equivalence problem for deterministic pushdown automata. Namely given two deterministic pushdown automata, it is decidable if they accept the same language. This result was first proved by Géraud Sénizergues in 1997. His proof consists in two semi-decision procedures and hence while establishing decidability does not give an upper-bound on the complexity of the problem. In 2002, Colin Stirling gave a primitive recursive algorithm to decide the problem. <p> The aim of the talk is to present what seems to be the simplest self-contained proof of this result. We will present 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 procedures. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday April 15, 2015, 10:30AM, 4067<br/> <strong>Nathanaël Fijalkow</strong> (LIAFA) <em>Algorithmics Properties of Probabilistic Automata, part II</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3636"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3636"><div class="bs-wrap bs-wrap-well well well-sm"> This talk is a continuation of the talk from two weeks ago, but it will be independent, so please consider coming even if you didn’t attend the first part. <p> The plan for this second session is: </p> <ol class=" fix-media-list-overlap"> <li class="level1"><div class="li"> explain how to obtain a universally non-regular automaton (by adding one state to last time’s example),</div> </li> <li class="level1"><div class="li"> explain how to encode Minsky machines using bounded-error probabilistic automata, with two-way and one-way variants,</div> </li> <li class="level1"><div class="li"> explain how to encode probabilistic automata using only one random probabilistic transition,</div> </li> </ol> <p> show the decidability of two problems: the equivalence and the finiteness problem. Both proofs rely on one observation: the reals with the addition and the multiplication form a field, and some linear algebra. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday April 1, 2015, 10:30AM, 4068<br/> <strong>Nathanaël Fijalkow</strong> (LIAFA) <em>The Naughty Side of Probabilistic Automata.</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3637"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3637"><div class="bs-wrap bs-wrap-well well well-sm"> This talk is about probabilistic automata over finite words: such machines, when reading a letter, flip a coin to determine which transition to follow. Although quite simple, this computational model is quite powerful, and many natural problems are undecidable. <p> In this talk, I will review some of the most important undecidability results, with new simplified constructions. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday March 11, 2015, 10:30AM, 4068<br/> <strong>Michał Skrzypczak</strong> (LIAFA) <em>On topology in automata theory, Part II</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3638"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3638"><div class="bs-wrap bs-wrap-well well well-sm"> This talk will be a continuation of my talk from 11th February. I will not assume knowledge of any material presented then except for basic notions of topology. During this talk I will move to the case of regular languages of infinite trees. Since there are known examples of such languages 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 between topological complexity and automata-theoretic complexity measured by the Rabin-Mostowski index. My aim will be to prove certain results of strict containment using purely topological methods. At the end I hope to present some recent results about extensions of MSO. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday February 11, 2015, 10:30AM, 4068<br/> <strong>Michał Skrzypczak</strong> (LIAFA) <em>On topology in automata theory, Part I</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3639"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3639"><div class="bs-wrap bs-wrap-well well well-sm"> The interplay between topology and automata theory has a form of synergy: descriptive set theory motivates new problems and methods in automata theory but on the other hand, automata theory introduces natural examples for classical topological concepts. <p> During this talk I will introduce basic notions of topology and descriptive set theory focusing on the 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 theory. 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. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday January 28, 2015, 10:30AM, 4068<br/> <strong>Gabriele Puppis</strong> (LABRI) <em>Non-determinism vs two-way.</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3640"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3640"><div class="bs-wrap bs-wrap-well well well-sm"> Non-determinism and walking mechanisms were considered already at the very beginning of automata theory. I will survey a few results connecting models of automata and transducers enhanced with non-determinism and two-wayness. <p> A classical result by Rabin and Scott shows that deterministic finite state automata are as expressive as their non-deterministic and two-way counterparts. The translation from two-way automata to one-way automata is easily seen to imply an exponential blowup in the worst case, even when one maps deterministic two-way models to non-deterministic one-way models. The converse translation, which is based on the subset construction 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 possibly introducing two-wayness. In particular, the question of whether the exponential blowup is unavoidable in transforming non-determinism to two-wayness is open. </p> <p> When one turns to models of transducers, some translations 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 natural problem thus arises that amounts at characterizing the two-way transductions that can be implemented by one-way functional transducers. The latter problem was solved in recent paper by Filiot, Gauwin, Reynier, and Servais – however, some questions related to complexity remains open. Another interesting, but older, result by Hopcroft shows that functional non-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 two-way transducers are closed under functional composition. </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2014">Year 2014</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2014" id="plugin_include__en__seminaires__laag__laag2014"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday December 17, 2014, 10:30AM, 4068<br/> <strong>Stefan Göller</strong> (LSV) <em>Equivalence checking of infinite state systems: A couple of lower bounds</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3641"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3641"><div class="bs-wrap bs-wrap-well well well-sm"> We will recall a generic technique for proving lower bounds for bisimulation equivalence checking (for which there was not enough time in my last LAAG talk) . First, we will introduce bisimulation equivalence and recall Jancar’s and Srba’s Defender’s Forcing lower bound technique. Then, we will apply this technique to different classes of infinite state systems for showing the following hardness results : (1) undecidability for prefix-recognizable graphs, (2) undecidability for vector addition systems, (3) nonelementary hardness for pushdown graphs, and (4) Ackermann hardness for equational graphs of finite out-degree. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday December 3, 2014, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>Stabilization monoids and cost functions</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3642"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3642"><div class="bs-wrap bs-wrap-well well well-sm"> In this third part, we will introduce stabilization monoids and cost functions, and show ho this constitutes a good framework in which the results of the previous talks can be unified. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday November 19, 2014, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>Decidability of Boundedness and Limitedness</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3643"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3643"><div class="bs-wrap bs-wrap-well well well-sm"> This talk constitutes the continuation of the previous one, in which the star-height problem was reduced to a boundedness question. <p> In this second part, we will establish the decidability of this second problem, following the ideas of Leung, Simon, and Kirsten. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday November 5, 2014, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>The star-height problem and its link to boundedness and limitedness</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3644"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3644"><div class="bs-wrap bs-wrap-well well well-sm"> This talk is the first in a series of lecture intended to describe the main ideas and the use of automata limitedness and related questions. <p> The goal of the first session is to present the famous (restricted) star-height problem, and show the first steps toward its resolution. The 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 expression of star-height (i.e., nesting of Kleene stars) at most k. This problem has been open for 25 years unit Hashiguchi provided a proof in a series 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). </p> <p> The idea behind both these proofs is to reduce the original problem to a question of existence of bounds 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. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday April 10, 2014, 10:30AM, 2014<br/> <strong>David Xiao</strong> (LIAFA) <em>Une introduction aux graphes expandeurs</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3645"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3645"><div class="bs-wrap bs-wrap-well well well-sm"> Les graphes expandeurs sont des graphes creux mais fortement connexes. Ils peuvent se substituer aux graphes denses ou même aux graphes complets dans beaucoup d’applications, et ainsi permettre une réduction de complexité de calcul ou d’aléa. Ils jouent un rôle clé dans plusieurs domaines de l’informatique fondamentale, notamment dans la dérandomisation et le pseudo-aléa. <p> Dans cet exposé nous présenterons les graphes expandeurs, leur(s) définition(s), quelques lemmes structurels fondamentaux, et quelques exemples de leur utilisation dans la dérandomisation. Nous esquisserons également la construction basée sur le produit zigzag. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday March 27, 2014, 10:30AM, 2014<br/> <strong>Michael Vanden Boom</strong> (Oxford university) <em>Automata characterizations of WMSO</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3646"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3646"><div class="bs-wrap bs-wrap-well well well-sm"> Weak monadic second-order logic (WMSO) over the infinite binary tree has the same syntax as MSO, but second-order quantification is interpreted only over finite sets. It captures a strict subclass of the regular languages of infinite trees, but is expressive enough to subsume temporal logics like CTL. <p> In this talk, I will sketch the proofs showing the equivalence of WMSO and a form of automata called weak alternating automata. I will also prove Rabin’s characterization of WMSO: a language is weakly definable iff the language and its complement are recognizable by nondeterministic Büchi automata. </p> <p> I will conclude by describing connections with recent work (joint with Thomas Colcombet, Denis Kuperberg, and Christof Löding) showing that given a Büchi automaton as input, it is decidable whether the language is definable in WMSO. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday March 13, 2014, 10:30AM, 2014<br/> <strong>Olivier Serre</strong> (LIAFA) <em>Rabin theorem</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3647"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3647"><div class="bs-wrap bs-wrap-well well well-sm"> In 1969, Michael O. Rabin established that the class of regular tree languages (i.e. languages of infinite node-labelled complete binary trees accepted by non-deterministic tree automata) form a Boolean algebra. The goal of this talk is to present the underlying objects of this statement as well as a complete proof of it. <p> Hence, the structure of the talk will be as follows: </p> <ol class=" fix-media-list-overlap"> <li class="level1"><div class="li"> Main definitions and examples : infinite trees, parity tree automata and regular tree languages</div> </li> <li class="level1"><div class="li"> Basic recalls on positional determinacy of two-player parity games on graphs (see previous LAAG seminar by Nathanaël Fijalkow)</div> </li> <li class="level1"><div class="li"> Acceptance game and emptiness game/test for parity tree automata</div> </li> <li class="level1"><div class="li"> Complementation of parity tree automata relying on positional determinacy and determinisation of automata on infinite words (see previous LAAG seminar).</div> </li> </ol> <p> I will assume no specific knowledge on automata nor games for that talk. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Saturday March 1, 2014, 10:30AM, 2014<br/> <strong>Nathanaël Fijalkow</strong> (LIAFA) <em>Positional determinacy part II</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3648"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3648"><div class="bs-wrap bs-wrap-well well well-sm"> Last week, Thomas Colcombet presented a proof of Positional Determinacy for Parity Games, following a forward approach. In this second part, I will present a completely different proof of the same result based on ideas by Muller and Schupp, following a backward approach. <p> I will highlight the differences between the two approaches, and the applications of both techniques. In particular, I will explain why backward approaches naturally induce determinization procedures for automata over infinite words. </p> <p> The talk will be self-contained, and in particular I will quickly recall all required definitions at the beginning. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday February 6, 2014, 10:30AM, 2014<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>Positional determinacy part I</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3649"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3649"><div class="bs-wrap bs-wrap-well well well-sm"> In this sequence of two seminars, we will recall the basic definitions of games and parity games. We will give several proofs and applications of the most famous result in this context: the memoryless determinacy theorem. We will also see how some of these techniques naturally provide determinization procedures over infinite words. <p> This is in preparation to the seminars after the holidays, that will aim at presenting the results on the monadic theory of the infinite binary tree. </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2013">Year 2013</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2013" id="plugin_include__en__seminaires__laag__laag2013"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday December 19, 2013, 10:30AM, 4068<br/> <strong>Sylvain Schmitz</strong> (LSV) <em>Complexity classes beyond elementary</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3650"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3650"><div class="bs-wrap bs-wrap-well well well-sm"> I will present a hierarchy of fast-growing complexity classes and show its suitability for completeness statements of many non elementary problems, which occur naturally in logic, combinatorics, formal language, verification, etc., with complexities ranging from simple towers of exponentials to Ackermannian and beyond. <p> I plan to skim over the following topics: </p> <ol class=" fix-media-list-overlap"> <li class="level1"><div class="li"> subrecursive hierarchies: these are functions and classes that allow to define rapidly-growing functions by recursion over ordinal indices,¡/li¿</div> </li> <li class="level1"><div class="li"> 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¿</div> </li> <li class="level1"><div class="li"> the definition of fast-growing complexity classes and some easy properties.</div> </li> </ol> <p> The recent results will be taken from work together with S. Abriola, D. Figueira, S. Figueira, C. Haase, S. Haddad, and Ph. Schnoebelen. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday November 28, 2013, 10:30AM, 4068<br/> <strong>Joël Ouaknine</strong> (Oxford university) <em>Decision Problems for Linear Recurrence Sequences</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3651"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3651"><div class="bs-wrap bs-wrap-well well well-sm"> Linear recurrence sequences (such as the Fibonacci numbers) permeate a vast number of areas of mathematics and computer science (in particular: program termination and probabilistic verification), and also have many applications in other fields such as economics, theoretical biology, and statistical physics. In this talk, I will focus on three fundamental 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 (are all but finitely many terms of the sequence positive?). <p> This is joint work with James Worrell. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday November 7, 2013, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>Green’s relations and automata theory</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3652"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3652"><div class="bs-wrap bs-wrap-well well well-sm"> Green’s relations form a fundamental tool in the analysis of the structure of semigroups and monoids, in particular for the finite ones. Understanding Green’s relations can give remarkable intuitions concerning 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 decomposition into strongly connected components that is used in many proofs. <p> During this talk, I will present some of the key results concerning Green’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-trivial 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 time do to all these). </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday October 17, 2013, 10:30AM, 4068<br/> <strong>Arnaud Durand</strong> (Université Denis Diderot - Paris 7) <em>How to count in weak formalisms?</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3653"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3653"><div class="bs-wrap bs-wrap-well well well-sm"> 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 their expressive power, and also resorts to complexity theoretic motivations : the more we can count the closer we get to real computing power. The question was investigated in several papers in complexity theory and in weak arithmetic a long time ago. In each case, the considered formalism (constant-depth circuits, MSO with addition or first-order bounded arithmetic) was shown to be able to count up to a polylogarithmic number. An essential 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 expressibility of this mapping depends on some strong and non-constructive argument (group theoretic device or prime number theorem). <p> In this talk we will evocate these different methods and present a completely elementary (and constructive) approach to reprove uniformly all these results (based on an old paper with M. More and C. Lautemann). We will also review why some of these results cannot be extended. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday June 13, 2013, 10:30AM, 4068<br/> <strong>Łukasz Kaiser</strong> (LIAFA) <em>Machine Learning Viewed by a Logician</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3654"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3654"><div class="bs-wrap bs-wrap-well well well-sm"> Machine learning guys do things like linear regression, neural networks and support vector machines. Logic guys do relational structures, 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 sometimes 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 this 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 relationship can be beneficial for both fields - providing theorems and deeper understanding to machine learning and practically relevant questions and experimental results to logic. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday May 30, 2013, 10:30AM, 4068<br/> <strong>Gabriele Puppis</strong> (LABRI) <em>The Cost of Repairing Regular Specifications</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3655"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3655"><div class="bs-wrap bs-wrap-well well well-sm"> 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 database community for relational integrity constraints, and in the AI community for propositional logics. Different modification operators have been considered on the basis of the application scenarios. For instance, a repair of an XML document usually consists of applying to the underlying tree structure a certain number of editing operations such as relabelings, deletions, and insertions of nodes. In this talk I will survey some results related to the worst-case cost of repairing documents between regular specifications. 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 specification (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 word/tree in T using a finite, uniformly bounded number of editing operations. I will give effective characterizations of these pairs when S and T are given by finite state automata (word case) or stepwise tree automata (tree case), and derive some complexity bounds for the corresponding problems. Time permitting, I will also talk about the normalized repair cost; more specifically, about the problem of computing the worst-case repair cost between two languages S and T normalized by the length of the input word. <p> The presentation is based on joint works with Michael Benedikt, Cristian Riveros, Sławek Staworko, and Pierre Bourhis. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday May 16, 2013, 10:30AM, 4068<br/> <strong>Howard Straubing</strong> (Boston college) <em>A New Proof of Simon’s Theorem, and Separation by Piecewise Testable Languages</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3656"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3656"><div class="bs-wrap bs-wrap-well well well-sm"> 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 testability of regular languages and J-triviality of the syntactic monoid. Mikolaj 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 size 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 will explain this more general result. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday April 18, 2013, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>Tree walking automata</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3657"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3657"><div class="bs-wrap bs-wrap-well well well-sm"> Tree walking automata were introduced during the 70s as a model for describing regular languages of trees [AU77]. The run of such an automaton, instead of being a tree as for standard tree automata, form a path in the input tree. At each step of the run, the (unique) head of the automato is located in some node, and based on the current configuration of the tree and the current state of the automaton goes to one of the children of the current node, or go to the parent of the current node, and changes of states. Iterating this process, the automaton walks a path in the tree, possibly ending accepting the input tree. Tree walking automata are easy to show to define regular languages of finite trees. <p> In this talk, we will cover several subjects related to tree walking automata, including, the separation properties (deterministic tree walking automata are strictly weaker than non-deterministic ones [BC06], which in turn are strictly weaker than regular languages [BC08]) and closure properties (under complementation in particular [MSS06]). We will also present the models of pebble automata and relate it to first-order logic with transitive closure [EH99]. We will conclude with the separation of this logic from monadic logic over finite trees [BSSS06,BS10]. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday April 4, 2013, 10:30AM, 4068<br/> <strong>Achim Blumensath</strong> (RWTH Aachen) <em>The Transduction Hierarchy and Definable Orderings</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3658"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3658"><div class="bs-wrap bs-wrap-well well well-sm"> I will give a survey on my recent work with Bruno Courcelle concerning the expressive power of monadic second-order logic on certain graph classes. In particular, I will present our work on the transduction hierarchy, a classification of graph classes according to their encoding power with respect to transductions. I will also give an overview on more recent work on the definability of linear orderings on certain classes of graphs. Here we aim at simple combinatorial characterisations of whether such an ordering is definable or not. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Wednesday March 20, 2013, 10:30AM, 4068<br/> <strong>Christof Löding</strong> (RWTH Aachen) <em>Definability of uniformisation and choice in monadic second order logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3659"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3659"><div class="bs-wrap bs-wrap-well well well-sm"> 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 binary tree. Such a choice function would be given by a formula that has one free set variable and one free element variable, and for each non-empty set 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. <p> A consequence of this result is that MSO-definable relations of infinite trees cannot be uniformized in MSO (where a uniformization of a binary relation is a function that is a subset of the relation and has the same domain as the relation). One can also use the result to show that there are nondeterministic automata on infinite trees that are not equivalent to an unambiguous automaton, i.e., an automaton that has at most one accepting run for each input. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday February 21, 2013, 10:30AM, 4068<br/> <strong>Christian Choffrut</strong> (LIAFA) <em>Uniformization</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3660"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3660"><div class="bs-wrap bs-wrap-well well well-sm"> To uniformize a binary relation means to find a partial function whose graph lies in the relation and whose domain coincides with that of the relation. Said differently it consists of selecting a unique image for 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 class. <p> I 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. </div> </p> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday February 7, 2013, 10:30AM, 4068<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>The construction of Safra</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3661"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3661"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we will present the classical construction of Safra, which transforms non-deterministic Büchi automata to deterministic Rabin automata. We will adopt the point of view of modern presentations of this result (in particular of Schewe), and cover the lower bound results. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday January 17, 2013, 10:30AM, -<br/> <strong>Stefan Göller</strong> (LSV) <em>Two lower bound techniques in formal verification</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3662"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3662"><div class="bs-wrap bs-wrap-well well well-sm"> First, I will talk about Defender’s Forcing, a technique introduced by Jancar and Srba that is used for proving lower bounds in bisimilarity 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-recognisable graphs, Petri Nets or PA processes. <p> Second, I will recall two classical results from complexity theory (i) PSPACE is serializable meaning roughly that for determining whether a word lies in a fixed PSPACE language one only needs to check if the yield (the leaf string) of the computation tree of an NP machine lies in a fixed regular language (ii) Converting 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 reachability problems and model checking problems for one-counter automata and timed automata, respectively. </div> </p> </div> </div> </div> <div class="level4"> <p> <br/> </p> </div> <h4 id="year_2012">Year 2012</h4> <div class="level4"> </div> <div class="plugin_include_content plugin_include__en:seminaires:laag:laag2012" id="plugin_include__en__seminaires__laag__laag2012"> <div class="level4"> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday December 20, 2012, 10:30AM, -<br/> <strong>Sam Van Gool</strong> (LIAFA) <em>A topological proof of Gödel’s completeness theorem for first-order logic</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3663"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3663"><div class="bs-wrap bs-wrap-well well well-sm"> In the fifties of the previous century, Rasiowa and Sikorski gave a topological proof of Gödel’s completeness theorem for first-order logic. Their proof ultimately relies on the Baire category theorem, which is mainly known for its powerful applications in real and functional analysis. Therefore, the application of Baire’s theorem to prove this fundamental result in logic is a surprising and interesting one. The main goal of this talk will be to give an exposition of this elegant topological proof by Rasiowa and Sikorski. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday December 13, 2012, 10:30AM, -<br/> <strong>Colin Riba</strong> (ENS Lyon) <em>A Model Theoretic Proof of Completeness of an Axiomatization of Monadic Second-Order Logic on Infinite Words</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3664"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3664"><div class="bs-wrap bs-wrap-well well well-sm"> We discuss the completeness of an axiomatization of Monadic Second-Order Logic (MSO) on infinite words (or streams). By using model-theoretic tools, we give an alternative proof of D. Siefkes’ result that a fragment with full comprehension and induction of second-order Peano’s arithmetic is complete w.r.t. the validity of MSO-formulas on streams. We rely on Feferman-Vaught Theorems and the Ehrenfeucht-Fraissé method for Henkin models of second-order arithmetic. Our main technical contribution is an infinitary Feferman-Vaught Fusion of such models. We show it using Ramseyan 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-definable colorings implies Ramsey’s theorem for all MSO-definable colorings. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday June 14, 2012, 10:30AM, -<br/> <strong>Frédéric Magniez</strong> (LIAFA) <em>An Introduction to Communication Complexity</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3665"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3665"><div class="bs-wrap bs-wrap-well well well-sm"> We will give a self-content course on the basics of Communication Complexity together with simple and elegant applications for proving lower bounds in different computational models. For instance, we will give a space time tradeoff for recognizing a palindrome on a Turing machine. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday May 31, 2012, 10:30AM, -<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>The collapse of monadic second order logic over countable linear orderings</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3666"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3666"><div class="bs-wrap bs-wrap-well well well-sm"> This talk corresponds to a joint work with Olivier Carton and Gabriele Puppis and provides a prolongation of the previous seminar. The subject wil be the algebraic approach to monadic second order logic over infinite words. We will in particular show how this notion of recognition is equivalent to the logic. This techniques provide at the same time a collapse of the logic to the one with only one alternation of monadic quantifiers. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday May 10, 2012, 10:30AM, -<br/> <strong>Thomas Colcombet</strong> (LIAFA) <em>The monadic theory of orderings</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3667"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3667"><div class="bs-wrap bs-wrap-well well well-sm"> In this talk, we present the aproaches of Rabin (69) and Shelah (75) for deciding the monadic theory of the rationals with order. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday May 3, 2012, 10:30AM, -<br/> <strong>Michel De Rougemont</strong> (LIAFA) <em>Games for Monadic Σ11 (EMSO) and probabilistic methods</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3668"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3668"><div class="bs-wrap bs-wrap-well well well-sm"> I’ll survey the classical Ehrenfeucht-Fraisse and Ajtai-Fagin games for this Logic. I’ll explain the role of the probabilistic method to prove that s,t-connexity is not Σ11 (EMSO) on graphs, using the Ajtai-Fagin games. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Thursday April 12, 2012, 10:30AM, -<br/> <strong>Olivier Carton</strong> (LIAFA) <em>Kamp's theorem</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3669"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3669"><div class="bs-wrap bs-wrap-well well well-sm"> Kamp’s theorem states the equivalence between temporal logics and temporal logics with past operators over complete linear orderings. </div> </div> <p> <a href="https://www.irif.fr/en/seminaires/laag/index" class="wikilink1" title="en:seminaires:laag:index" data-wiki-id="en:seminaires:laag:index">Logic, automata, algebra and games</a><br/> Monday March 26, 2012, 10:30AM, submarine<br/> <strong>Achim Blumensath</strong> (LIAFA) <em>Stability theory</em> <span class="bs-wrap bs-wrap-button" data-btn-type="link" data-btn-size="xs" data-btn-collapse="b23-3670"><i class="dw-icons fa-lg fa fa-info-circle" style="color:#777" title=""></i></span><br/> </p> <div class="bs-wrap bs-wrap-collapse collapse" id="b23-3670"><div class="bs-wrap bs-wrap-well well well-sm"> - </div> </div> </div> </div> <div class="level4"> </div> </div></div><p> <style> .page a.urlextern, .page a.interwiki, .page a.windows, .page a.mail, .page a.media { padding-left: 0 !important; background: none !important; } .page { text-align: justify; } body {font-size: 15px; font-weight: 300; color: #333333; } b,strong {font-weight: 600; color: #333333; } p {margin-bottom:1.3em} h1 {font-size: 2.8em; margin-bottom:1.5em; font-weight: 400; } h2 {font-size: 2.2em; margin-bottom:1.2em; font-weight: 400; } h3 {font-size: 1.9em; margin-bottom:0.9em; font-weight: 400; } h4 {font-size: 1.7em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.5em; margin-bottom:0.8em; font-weight: 300; } h5 {font-size: 1.4em; margin-bottom:0.8em; font-weight: 300; } </style> </p> </div> </div> <div class="small text-right"> </div> </article> </div> </main> <footer id="dw__footer" class="dw-container py-5 dokuwiki container-fluid">  <div class="dw-container small container-fluid mx-5"> <div class="footer-dw-title"> <div class="media"> <div class="media-left">  <img src="https://www.irif.fr/_media/logo_footer.png" alt="" class="media-object" style="height:10px" /> </div> <div class="media-body"> <div class="row"> <div class="col-sm-2"> <h4 class="media-heading"></h4> <p> </p> </div> <div class="col-sm-10"> </div> </div> </div> </div> </div> <a style="font-size:12px" href="https://www.irif.fr/informations/mentions-legales">Mentions légales</a> <div class="footer-license row"> <hr/> <div id="dw__license" class="col-sm-6"> </div> <div class="col-sm-6"> </div> </div> </div>  </footer> <a href="#dokuwiki__top" class="back-to-top hidden-print btn btn-default" title="skip to content" accesskey="t"> <span class="iconify" data-icon="mdi:chevron-up"></span> </a> <div id="screen__mode"> <span class="visible-xs-block"></span> <span class="visible-sm-block"></span> <span class="visible-md-block"></span> <span class="visible-lg-block"></span> </div> <img src="https://www.irif.fr/lib/exe/taskrunner.php?id=en%3Aseminaires%3Alaag%3Aindex&1732758314" width="2" height="1" alt="" /> </div> </body> </html>