---
OA_place: publisher
OA_type: hybrid
_id: '22719'
abstract:
- lang: eng
text: 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.
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.'
alternative_title:
- LNCS
article_processing_charge: Yes (in subscription journal)
arxiv: 1
author:
- first_name: Guy
full_name: Avni, Guy
id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
last_name: Avni
orcid: 0000-0001-5588-8287
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Kaushik
full_name: Mallik, Kaushik
id: 0834ff3c-6d72-11ec-94e0-b5b0a4fb8598
last_name: Mallik
orcid: 0000-0001-9864-7475
- first_name: Suman
full_name: Sadhukhan, Suman
last_name: Sadhukhan
- first_name: K. S.
full_name: Thejaswini, K. S.
last_name: Thejaswini
citation:
ama: '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'
apa: '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'
chicago: 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.
ieee: 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.
ista: '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.'
mla: 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.
short: G. Avni, T.A. Henzinger, K. Mallik, S. Sadhukhan, K.S. Thejaswini, in:, 38th
International Conference on Computer Aided Verification, Springer Nature, 2026,
pp. 237–257.
conference:
end_date: 2026-07-29
location: Lisbon, Portugal
name: 'CAV: Computer Aided Verification'
start_date: 2026-07-26
das_tickbox: '0'
date_created: 2026-08-16T22:01:44Z
date_published: 2026-07-24T00:00:00Z
date_updated: 2026-08-18T08:41:44Z
day: '24'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-032-32519-8_13
ec_funded: 1
external_id:
arxiv:
- '2605.13185'
file:
- access_level: open_access
checksum: f17ba3f82854fdb4eb69fd922965661a
content_type: application/pdf
creator: dernst
date_created: 2026-08-18T08:40:07Z
date_updated: 2026-08-18T08:40:07Z
file_id: '22730'
file_name: 2026_LNCS_Avni.pdf
file_size: 531980
relation: main_file
success: 1
file_date_updated: 2026-08-18T08:40:07Z
has_accepted_license: '1'
intvolume: ' 16682'
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 237-257
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
call_identifier: H2020
grant_number: '101020093'
name: Vigilant Algorithmic Monitoring of Software
publication: 38th International Conference on Computer Aided Verification
publication_identifier:
eissn:
- 1611-3349
isbn:
- '9783032325181'
issn:
- 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
researchdata_availability: no
scopus_import: '1'
status: public
supplementarymaterial: no
title: Decoupled planning for multiple omega-regular objectives
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 16682
year: '2026'
...