 Nie jesteś zalogowany | zaloguj się |
| Nie jesteś zalogowany | zaloguj się |
Cotygodniowe seminarium badawcze
2021-12-01, godz. 14:15, online
Ismaël Jecker (MIM UW)
A finite automaton A is called composite if there exist automata A1, A2, . . . , Ak smaller than A such that the language of A is equal to the intersection of the languages of the Ai. Otherwise, A is prime. This notion of primality was introduced by Orna Kupferman and Jonathan Mosheiff in 2015, but...
2021-11-24, godz. 14:15, online
Krzysztof Ziemiański (MIM UW)
Higher dimensional automata (HDA) are a formalism for modeling concurrent systems introduced by Pratt and van Glabbeek. I will present several ways to define languages of HDA, which are collections of interval pomsets closed under subsumption. Then I will define regular interval pomset languages and...
2021-11-17, godz. 14:15, 5050
Jędrzej Kołodziejski (MIM UW)
Taming (un)boundedness - logic, automata and games with countdown
I will present extensions of: the modal fixpoint calculus, parity games, and parity automata - designed to capture (un)boundedness-related phenomena. The extensions lift the classical logic~games~automata correspondence beyond regular properties - in particular the logic and automata define the same...
2021-11-10, godz. 14:15, 5050
Szymon Toruńczyk (MIM UW)
Some results and directions in finite model theory
I will discuss the FO-transduction order on classes of graphs (or other structures), defined by the relation: a class C can be obtained by an FO-transduction from a class D. I will focus on the interplay of this order with notions such as treewidth, clique-width, twin-width, bounded expansion, ...
2021-11-03, godz. 14:15, 5050
Piotr Hofman (MIM UW)
Language inclusion for unambiguous VASSes
During the talk, I will present our unpublished results with Wojciech Czerwiński. I will show the decidability of language inclusion for unambiguous VASSes. The main tool is, up to our knowledge, a new concept of future-determinization. ...
2021-10-27, godz. 14:15, 5050
Paweł Parys (MIM UW)
Higher-Order Model Checking Step by Step
I will show a new simple algorithm that solves the model-checking problem for recursion schemes: check whether the tree generated by a given higher-order recursion scheme is accepted by a given alternating parity automaton. Recursion scheme is a formalism to represent/generate an infinite tree, e...
2021-10-20, godz. 14:15, 5050
Jakub Gajarsky (MIM UW)
Differential games, locality, and model checking for FO logic of graphs
We introduce differential games for FO logic of graphs, a variant of Ehrenfeucht-Fraisse games in which the game is played on one graph only and the moves of both players are restricted. We prove that these games are strong enough to capture essential information about graphs from graph classes whic...
2021-10-13, godz. 14:15, 5050
Michał Skrzypczak (MIM UW)
Guidable automata and their index problem
Rabin's theorem relies on the equivalence between Monadic Second-Order logic and non-deterministic automata over infinite trees. The non-determinism of the involved model is known to be "inherent", both in terms of descriptive complexity and from the standpoint of uniformisability / unambiguity. As ...
2021-10-06, godz. 14:15, 5050
Szymon Toruńczyk (MIM UW)
Model checking separator logic on graphs that exclude a fixed topological minor.
We consider separator logic on graphs introduced recently by Bojańczyk, and independently by Siebertz, Shrader, and Vigny. This logic extends first-order logic by atomic predicates of arity k+2, for each k, expressing that every path from a vertex s to a vertex t must pass through one of the ver...
2021-06-30, godz. 14:15, online
Albert Gutowski (MIM UW)
Finite entailment of non-local queries in description logics
We study the problem of finite entailment of ontology-mediated queries. In particular, we are interested in non-local queries. Recent studies show that a vast majority of user-issued CRPQs only use Kleene star over unions of roles. We show how to answer such simple CRPQs, mediated by ontologies exp...
