{"id":7,"date":"2023-12-08T17:42:20","date_gmt":"2023-12-08T17:42:20","guid":{"rendered":"https:\/\/dlt2019.mimuw.edu.pl\/?page_id=7"},"modified":"2023-12-10T21:44:41","modified_gmt":"2023-12-10T21:44:41","slug":"invited-speakers","status":"publish","type":"page","link":"https:\/\/dlt2019.mimuw.edu.pl\/invited-speakers\/","title":{"rendered":"Invited speakers"},"content":{"rendered":"\n<ul uk-accordion=\"\">\n \t<li class=\"uk-card uk-card-default uk-card-small\">\n<div class=\"uk-card-header\">\n<div class=\"uk-grid-small uk-flex-middle\" uk-grid=\"\">\n<div class=\"uk-width-auto\">\n                <img loading=\"lazy\" decoding=\"async\" class=\"uk-border-circle\" src=\"\/wp-content\/uploads\/2019\/05\/uboker-small.png\" style=\"object-fit: cover; width:60px; height:60px;\" width=\"60\" height=\"60\" alt=\"Udi Boker\"><\/div>\n<div class=\"uk-width-expand\">\n<h3 class=\"uk-card-title uk-margin-remove-bottom\">Udi Boker<\/h3>\n<p class=\"uk-text-bold\" style=\"margin-top:0\">Inherent Size Blow-up in Omega-Automata<\/p>\n\n<\/div>\n<\/div>\n<\/div>\n<div class=\"uk-card-body uk-accordion-content\" style=\"margin-top:0\">\n\n        We clarify the succinctness of the different omega-automata types and the size blowup involved in boolean operations on them. We argue that there are good reasons for the classic acceptance conditions, while there is also place for additional acceptance conditions, especially in the deterministic setting; Boolean operations on deterministic automata with the classic acceptance conditions involve an exponential size blowup, which can be avoided by using stronger acceptance conditions. In particular, we analyze the combination of hyper-Rabin and hyper-Streett automata, which we call hyper-dual, and show that in the deterministic setting it allows for exponential succinctness compared to the classic types, boolean operations on it only involve a quadratic size blowup, and its nonemptiness, universality, and containment checks are in PTIME.\n\n<\/div>\n<div class=\"uk-card-footer uk-accordion-title\">\n        \t<a href=\"#\" class=\"uk-button uk-button-text\">Show abstract<\/a><\/div><\/li>\n \t<li class=\"uk-card uk-card-default uk-card-small\">\n<div class=\"uk-card-header\">\n<div class=\"uk-grid-small uk-flex-middle\" uk-grid=\"\">\n<div class=\"uk-width-auto\">\n                <img loading=\"lazy\" decoding=\"async\" class=\"uk-border-circle\" src=\"\/wp-content\/uploads\/2019\/05\/adoumane-small.jpg\" style=\"object-fit: cover; width:60px; height:60px;\" width=\"60\" height=\"60\" alt=\"Amina Doumane\"><\/div>\n<div class=\"uk-width-expand\">\n<h3 class=\"uk-card-title uk-margin-remove-bottom\">Amina Doumane<\/h3>\n<p class=\"uk-text-bold\" style=\"margin-top:0\">Completeness for Identity-free Kleene Lattices<\/p>\n\n<\/div>\n<\/div>\n<\/div>\n<div class=\"uk-card-body uk-accordion-content\" style=\"margin-top:0\">\n\n         We provide a finite set of axioms for identity-free Kleene\nlattices, which we prove sound and complete for the equational theory of\ntheir relational models.\n\nOur proof builds on the completeteness theorem for Kleene algebra, and\non a novel automata construction that makes it possible to extract\naxiomatic proofs using a Kleene-like algorithm.\n\n<\/div>\n<div class=\"uk-card-footer uk-accordion-title\">\n        \t<a href=\"#\" class=\"uk-button uk-button-text\">Show abstract<\/a><\/div><\/li>\n \t<li class=\"uk-card uk-card-default uk-card-small\">\n<div class=\"uk-card-header\">\n<div class=\"uk-grid-small uk-flex-middle\" uk-grid=\"\">\n<div class=\"uk-width-auto\">\n                <img loading=\"lazy\" decoding=\"async\" class=\"uk-border-circle\" src=\"\/wp-content\/uploads\/2019\/05\/ajez-small.jpg\" style=\"object-fit: cover; width:60px; height:60px;\" width=\"60\" height=\"60\" alt=\"Artur Je\u017c\"><\/div>\n<div class=\"uk-width-expand\">\n<h3 class=\"uk-card-title uk-margin-remove-bottom\">Artur Je\u017c<\/h3>\n<p class=\"uk-text-bold\" style=\"margin-top:0\">Deciding Context Unification (with regular constraints)<\/p>\n\n<\/div>\n<\/div>\n<\/div>\n<div class=\"uk-card-body uk-accordion-content\" style=\"margin-top:0\">\n\nGiven a ranked signature, context are terms with a single occurrence of\na special symbol \u2022\n(outside of the signature), which represents a missing subterm.\nOne can naturally build equations over contexts: the context variables\nare treated as symbols of arity one and a subtitution $S$ assigns to\neach such a variable\na context $S(X)$. A substitution $S$ is extended to terms with context\nvariables in a natural way:\n$S(X(t))$ is a context $S(X)$ in which the unique occurrence of \u2022 is\nreplaced with $S(t)$.\nFor historical reasons, the satisfiability of context equations is\nusually referred to as context unification.\n\nContext unification generalizes word equations and first-order term\nunification (which are decidable)\nand is subsumed by second order unification (which is undecidable)\nand its decidability status remained open for almost two decades.\nIn this talk I will show a PSPACE algorithm for this problem.\nThe idea is to apply simple compression rules\n(replacing pairs of neighbouring function symbols)\nto the solution of the context equation;\nto this end we appropriately modify the equation\n(without the knowledge of the actual solution)\nso that compressing the solution can be simulated by compressing parts\nof the equation.\nWhen the compression operations are appropriately chosen,\nthen the size of the instance is polynomial during the whole algorithm,\nthus giving a PSPACE-upper bound.\nThe best known lower bounds are as for word equations, i.e. NP.\nThe method can be extended to the scenario in which tree-regular\nconstraints for the variables are present,\nin which case the problem is EXPTIME-complete.\n\n<\/div>\n<div class=\"uk-card-footer uk-accordion-title\">\n        \t<a href=\"#\" class=\"uk-button uk-button-text\">Show abstract<\/a><\/div><\/li>\n \t<li class=\"uk-card uk-card-default uk-card-small\">\n<div class=\"uk-card-header\">\n<div class=\"uk-grid-small uk-flex-middle\" uk-grid=\"\">\n<div class=\"uk-width-auto\">\n                <img loading=\"lazy\" decoding=\"async\" class=\"uk-border-circle\" src=\"\/wp-content\/uploads\/2019\/05\/sseki-small.png\" style=\"object-fit: cover; width:60px; height:60px;\" width=\"60\" height=\"60\" alt=\"Shinnosuke Seki\"><\/div>\n<div class=\"uk-width-expand\">\n<h3 class=\"uk-card-title uk-margin-remove-bottom\">Shinnosuke Seki<\/h3>\n<p class=\"uk-text-bold\" style=\"margin-top:0\">Single-stranded architectures for computing<\/p>\n\n<\/div>\n<\/div>\n<\/div>\n<div class=\"uk-card-body uk-accordion-content\" style=\"margin-top:0\">\n\nRNA is a chain of ribonucleotides of four kinds (denoted respectively by the letters A, C, G, U).While being synthesized sequentially from its template DNA (transcription), it folds upon itself into intricate higher-dimensional structures in such a way that the free energy is minimized, that is, the more hydrogen bonds between ribonucletoides or larger entropy a structure has, the more likely it is chosen, and furthermore the minimization is done locally. This phenomenon is called cotranscriptional folding (CF). It has turned out to play significant roles in in-vivo computation throughout experiments and recently proven even programmable artificially so as to self-assemble a specific RNA rectangular tile structure in vitro. The next step is to program a computation onto DNA in such a way that the computation can be &#8220;called&#8221; by cotranscriptional folding. In this novel paradigm of computation, what programmers could do is only twofold: designing a template DNA and setting environmental parameters. Oritatami is an introductory &#8220;toy&#8221; model to this paradigm of computation. In this model, programmers are also allowed to employ an arbitrarily large finite alphabet as well as an arbitrarily complex rule set for binding. We shall present known architectures of computing in the oritatami model from a simple half-adder to Turing machine along with several programming techniques of use, with hope that they will inspire in-vivo architectures of CF-driven self-assemblable computers, which could be even heritable.\n\n<\/div>\n<div class=\"uk-card-footer uk-accordion-title\">\n        \t<a href=\"#\" class=\"uk-button uk-button-text\">Show abstract<\/a><\/div><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"Udi Boker Inherent Size Blow-up in Omega-Automata We clarify the succinctness of the different omega-automata types and the size blowup involved in boolean operations on them. We argue that there are good reasons for the classic acceptance conditions, while there is also place for additional acceptance conditions, especially in the deterministic setting; Boolean operations on [&hellip;]","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"_links":{"self":[{"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/pages\/7"}],"collection":[{"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/comments?post=7"}],"version-history":[{"count":1,"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/pages\/7\/revisions"}],"predecessor-version":[{"id":8,"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/pages\/7\/revisions\/8"}],"wp:attachment":[{"href":"https:\/\/dlt2019.mimuw.edu.pl\/wp-json\/wp\/v2\/media?parent=7"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}