conference paper published yes Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Nicolas Adrien Mazzocchi author b26baa86-3308-11ec-87b0-8990f34baa85 Naci E Sarac author 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425 ToHe department GradSch department CONCUR: Conference on Concurrency Theory Vigilant Algorithmic Monitoring of Software project We study the following refinement relation between nondeterministic state-transition models: model ℬ strategically dominates model 𝒜 iff every deterministic refinement of 𝒜 is language contained in some deterministic refinement of ℬ. 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 𝒜 and ℬ: every strategy that resolves the nondeterminism of 𝒜 is dominated by a strategy that resolves the nondeterminism of ℬ. 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 automata, and checking the inclusion between hyperproperties that are specified by nondeterministic boolean and quantitative automata. https://research-explorer.ista.ac.at/download/18068/18081/2024_LIPICS_Henzinger.pdf application/pdfno https://creativecommons.org/licenses/by/4.0/ Schloss Dagstuhl - Leibniz-Zentrum für Informatik2024Calgary, Canada eng 1868-8969 9783959773393 2407.10473 00155684740002910.4230/LIPIcs.CONCUR.2024.29 311 T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 35th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). Strategic dominance: A new preorder for nondeterministic processes. In <i>35th International Conference on Concurrency Theory</i> (Vol. 311). Calgary, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.29">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a> Henzinger TA, Mazzocchi NA, Sarac NE. Strategic dominance: A new preorder for nondeterministic processes. In: <i>35th International Conference on Concurrency Theory</i>. Vol 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2024. doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.29">10.4230/LIPIcs.CONCUR.2024.29</a> Henzinger, Thomas A., et al. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” <i>35th International Conference on Concurrency Theory</i>, vol. 311, 29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024, doi:<a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.29">10.4230/LIPIcs.CONCUR.2024.29</a>. Henzinger TA, Mazzocchi NA, Sarac NE. 2024. Strategic dominance: A new preorder for nondeterministic processes. 35th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 311, 29. Henzinger, Thomas A, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Strategic Dominance: A New Preorder for Nondeterministic Processes.” In <i>35th International Conference on Concurrency Theory</i>, Vol. 311. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. <a href="https://doi.org/10.4230/LIPIcs.CONCUR.2024.29">https://doi.org/10.4230/LIPIcs.CONCUR.2024.29</a>. T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Strategic dominance: A new preorder for nondeterministic processes,” in <i>35th International Conference on Concurrency Theory</i>, Calgary, Canada, 2024, vol. 311. 180682024-09-15T22:01:40Z2025-12-02T13:45:38Z