Strategic Dominance: A New Preorder for Nondeterministic Processes
Thomas A. Henzinger, Nicolas Mazzocchi, N. Ege Sara\c{c}

TL;DR
This paper introduces a new preorder called strategic dominance for nondeterministic models, which lies between trace inclusion and simulation, and provides a logical framework for its decidability and applications.
Contribution
It defines strategic dominance as a novel refinement relation for nondeterministic processes and characterizes it via resolver logic, enabling new verification applications.
Findings
Strategic dominance is strictly between trace inclusion and simulation.
Resolver logic can decide strategic dominance in 2-ExpTime.
Applications include checking automata properties and hyperproperty inclusion.
Abstract
We study the following refinement relation between nondeterministic state-transition models: model B strategically dominates model A iff every deterministic refinement of A is language contained in some deterministic refinement of B. While language containment is trace inclusion, and the (fair) simulation preorder coincides with tree inclusion, strategic dominance falls strictly between the two and can be characterized as "strategy inclusion" between A and B: every strategy that resolves the nondeterminism of A is dominated by a strategy that resolves the nondeterminism of B. Strategic dominance can be checked in 2-ExpTime by a decidable first-order Presburger logic with quantification over words and strategies, called resolver logic. We give several other applications of resolver logic, including checking the co-safety, co-liveness, and history-determinism of boolean and quantitative…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBusiness Strategy and Innovation
