How can I check if an LTL (Linear Temporal Logic) property is safety or liveness? Is it right to say that a property is safety OR liveness (or neither)? How can I evaluate this: ...
it is well known that the modal $\mu$-calculus is one of the most expressive temporal logics for expressing properties of trees/graphs, and that CTL* is strictly less expressive than the $\mu$-...
I would like to know if somebody has studied the following very simple fragment of the modal mu-calculus: $$F::= X \;| \; p \; | \; F \wedge G \; | \; [a]F \; | \; \nu X.F$$ where p ranges over ...
I saw in this question a reference to $\mu$-recursive functions or $\mu$-calculus as some computation model equivalent to Turing machines and $\lambda$-calculus. I know about these two but never heard ...
I need a book on Mu-Calculus with lots of examples that can be used for self-study and preparation for exams.