Scalar and Vectorial mu-calculus with Atoms

03/18/2018
by   Bartek Klin, et al.
0

We study an extension of modal mu-calculus to sets with atoms and we study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show expressive limitations of atom-enriched mu-calculi, and explain how their expressive power depends on the structure of atoms used, and on the choice between basic or vectorial syntax.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset