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.
Use and reproduction:No Creative Commons license - The provisions of the German Copyright Act (UrhG) apply.Please note that individual components of the publication may be subject to other licensing or copyright conditions.