Decoupled planning for multiple omega-regular objectives

Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. 2026. Decoupled planning for multiple omega-regular objectives. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16682, 237–257.

Download
OA 2026_LNCS_Avni.pdf 531.98 KB [Published Version]

Conference Paper | Published | English

Scopus indexed
Author
Avni, GuyISTA ; Henzinger, Thomas AISTA ; Mallik, KaushikISTA ; Sadhukhan, Suman; Thejaswini, K. S.
Series Title
LNCS
Abstract
We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled.
Publishing Year
Date Published
2026-07-24
Proceedings Title
38th International Conference on Computer Aided Verification
Publisher
Springer Nature
Acknowledgement
This work is funded by the following grants: European Research Council under Grant No.: ERC-2020-AdG 101020093, ISF grant no. 1679/21, grant RYC2024-049116, MICIU/AEI/10.13039/501100011033, the ESF+, and Volkswagen Foundation within its Momentum framework under project no. 9C283.
Volume
16682
Page
237-257
Conference
CAV: Computer Aided Verification
Conference Location
Lisbon, Portugal
Conference Date
2026-07-26 – 2026-07-29
ISSN
eISSN
IST-REx-ID

Cite this

Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. Decoupled planning for multiple omega-regular objectives. In: 38th International Conference on Computer Aided Verification. Vol 16682. Springer Nature; 2026:237-257. doi:10.1007/978-3-032-32519-8_13
Avni, G., Henzinger, T. A., Mallik, K., Sadhukhan, S., & Thejaswini, K. S. (2026). Decoupled planning for multiple omega-regular objectives. In 38th International Conference on Computer Aided Verification (Vol. 16682, pp. 237–257). Lisbon, Portugal: Springer Nature. https://doi.org/10.1007/978-3-032-32519-8_13
Avni, Guy, Thomas A Henzinger, Kaushik Mallik, Suman Sadhukhan, and K. S. Thejaswini. “Decoupled Planning for Multiple Omega-Regular Objectives.” In 38th International Conference on Computer Aided Verification, 16682:237–57. Springer Nature, 2026. https://doi.org/10.1007/978-3-032-32519-8_13.
G. Avni, T. A. Henzinger, K. Mallik, S. Sadhukhan, and K. S. Thejaswini, “Decoupled planning for multiple omega-regular objectives,” in 38th International Conference on Computer Aided Verification, Lisbon, Portugal, 2026, vol. 16682, pp. 237–257.
Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. 2026. Decoupled planning for multiple omega-regular objectives. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16682, 237–257.
Avni, Guy, et al. “Decoupled Planning for Multiple Omega-Regular Objectives.” 38th International Conference on Computer Aided Verification, vol. 16682, Springer Nature, 2026, pp. 237–57, doi:10.1007/978-3-032-32519-8_13.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2026-08-18
MD5 Checksum
f17ba3f82854fdb4eb69fd922965661a


Export

Marked Publications

Metadata Export

Sources

arXiv 2605.13185

Search this title in

Google Scholar
ISBN Search