Nie jesteś zalogowany |
MSO+∇ is undecidable
- Prelegent(ci)
- Edon Kelmendi
- Afiliacja
- Uniwersytet Warszawski
- Termin
- 3 października 2018 14:15
- Pokój
- p. 5050
- Seminarium
- Seminarium „Teoria automatów”
We consider an extension of monadic second order logic on the infinite binary tree with a probabilistic path quantifier called ∇.
Intuitively this quantifier means "the set of branches that satisfy a formula has probability 1".
The probability measure that we use is the coin-tossing measure,
i.e. we generate a random branch by starting at the root, tossing a coin and proceeding to the left or right child according to the result of the coin toss, and so on.
By adding this quantifier we get a logic that properly extends MSO.
There is a weak variant that is decidable but the full logic is not.
In this talk we will sketch the undecidability proof.
There is a weak variant that is decidable but the full logic is not.
In this talk we will sketch the undecidability proof.
This is joint work with Mikołaj Bojańczyk and Michał Skrzypczak.
