Complete abstraction through extensions of disjunctive modal transition systems
Modal transition systems and their many variants are established models for abstraction and specification as they explicitly specify necessary and possible state or behavior. Disjunctive modal transition systems can be more precise abstractions as they allow a disjunctive split on necessary transitions. We show that these abstractions are compact, sound, and complete for - and as expressive as - the modal mu-calculus if models are enriched with fairness constraints and conjunctive splitting abilities for possible transitions. We point out the potential benefits of our approach over other complete abstraction frameworks.