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.

Logo BII

BII

Rechte

Nutzung und Vervielfältigung:

Keine Lizenz. Es gelten die Bestimmungen des deutschen Urheberrechts (UrhG).

Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.