You are not logged in |
joint work with Szymon Toruńczyk) & Evaluation of normalized mu-calculus formulas is polynomial for fixed structure size
- Speaker(s)
- Szczepan Humel & Paweł Parys
- Affiliation
- Uniwersytet Warszawski
- Date
- Jan. 27, 2010, 1 p.m.
- Room
- room 5870
- Seminar
- Seminar Automata Theory
Szczepan 13.00
Bojańczyk and Colcombet have recently introduced new classes of omega languages, \omega B-, \omega S- and \omega BS-regular languages. All those classes can be characterized by counter automata with different acceptance conditions or by extensions of omega-regular expressions with two variants of Kleene star. As a consequence, they all extend the class of classical omega-regular languages. We prove that the Borel complexities of the classes are \Sigma_3, \Pi_3 and \Sigma_4, respectively. We give both, upper and lower, bounds for that. Since the result itself occurs to be short, I should have enough time to define some basic topological notions and recollect basic facts that bind topology and automata theory.
Bojańczyk and Colcombet have recently introduced new classes of omega languages, \omega B-, \omega S- and \omega BS-regular languages. All those classes can be characterized by counter automata with different acceptance conditions or by extensions of omega-regular expressions with two variants of Kleene star. As a consequence, they all extend the class of classical omega-regular languages. We prove that the Borel complexities of the classes are \Sigma_3, \Pi_3 and \Sigma_4, respectively. We give both, upper and lower, bounds for that. Since the result itself occurs to be short, I should have enough time to define some basic topological notions and recollect basic facts that bind topology and automata theory.
Paweł 14.30
We consider mu-calculus formulas in a normal form: after a prefix of fixed-point quantifiers follows a quantifier-free expression. We prove that the problem of evaluating (model checking) of such formula in a fixed powerset lattice (expression complexity) is polynomial. Assumptions about the quantifier-free part of the expression are weakest possible: it can be any monotone function given by a computational procedure.
