Cheap Ctl Compassion In Nusmv

We discuss expansions of CTL with connectives able to express Streett fairness objectives for single paths. We focus on (E)SFCTL: (Extended) Streett-Fair CTL inspired by a seminal paper of Emerson and Lei. Unlike several other fair extensions of CTL, our entire formalism (not just a subclass of formulas in some canonical form) allows a succinct embedding into the mu-calculus, while being able to express concisely all relevant types of path-based fairness objectives. We implement our syntax in the well-known symbolic model checker NuSMV, consequently also implementing CTL model checking with "compassion" objectives. Since the mu-calculus embedding requires only alternation depth two, the resulting specifications correspond to parity games with two priorities. This allows a comparison of the performance of our NuSMV(sf) with existing parity game solvers (both explicit and symbolic). The advantages of the symbolic approach seem to extend to fair model checking.