Scaling GR(1) synthesis via a compositional framework for LTL discrete event control
Author(s)
Gagliardi, Hernan
Braberman, Victor
Uchitel, Sebastian
Type
Conference Paper
Abstract
We present a compositional approach to controller synthesis of discrete event system controllers with linear temporal logic (LTL) goals. We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems (LTS), to mitigate state explosion that monolithic approaches to synthesis are prone to. Maximally permissive safe controllers are iteratively built for subsets of the plant LTSs by solving weaker control problems. Observational synthesis equivalence is used to reduce the size of the controlled subset of the plant by abstracting away local events. The result of synthesis is also compositional, a set of controllers that when run in parallel ensure the LTL goal. We implement synthesis in the MTSA tool for an expressive subset of LTL, GR(1), and show it computes solutions to that can be up to 1000 times larger than those that the monolithic approach can solve.
Date Issued
2025-07-23
Date Acceptance
2025-05-23
Citation
Lecture Notes in Computer Science, 2025, 15934, pp.201-223
ISBN
978-3-031-98684-0
ISSN
0302-9743
Publisher
Springer
Start Page
201
End Page
223
Journal / Book Title
Lecture Notes in Computer Science
Volume
15934
Copyright Statement
© 2025 The Author(s). Published by Springer Nature. This is the author’s accepted manuscript made available under a CC-BY licence in accordance with Imperial’s Research Publications Open Access policy (www.imperial.ac.uk/oa-policy)
License URL
Source
Computer Aided Verification (CAV 2025)
Publication Status
Published
Start Date
2025-07-23
Finish Date
2025-07-25
Coverage Spatial
Zagreb, Croatia
Date Publish Online
2025-07-23