Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control

TL;DR

This paper introduces a modular compositional framework for synthesizing controllers for discrete event systems with LTL goals, significantly reducing computational complexity compared to monolithic methods.

Contribution

It proposes a novel compositional synthesis approach leveraging system modularity and observational equivalence, enabling scalable controller synthesis for larger systems.

Findings

Achieves up to 1000x larger solutions than monolithic methods.

Uses a set of controllers to ensure LTL goals in parallel.

Implemented in the MTSA tool for GR(1) synthesis.

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.