Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Hernan Gagliardi, Victor Braberman, Sebastian Uchitel

TL;DR

The paper tackles the scalability problem in synthesizing discrete-event controllers with LTL goals for modular DES by introducing a compositional framework that builds safe subcontrollers for subplants and minimizes controlled subplants via observational equivalence. It formalizes a synthesis tuple and two preservation transformations (Composition and Partial Synthesis) to iteratively reduce the plant size while preserving the solution set, culminating in a live controller for the remaining subproblem. Implemented in MTSA and evaluated on GR(1) DES benchmarks, the approach achieves substantial scalability gains, solving problems up to about 1000× larger than monolithic synthesis and showing favorable interactions with reactive-synthesis backends. The work demonstrates that modular synthesis can mitigate state explosion in GR(1) DES control and opens avenues for smarter heuristics, projection strategies, and extension to broader LTL classes.

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.

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

TL;DR

The paper tackles the scalability problem in synthesizing discrete-event controllers with LTL goals for modular DES by introducing a compositional framework that builds safe subcontrollers for subplants and minimizes controlled subplants via observational equivalence. It formalizes a synthesis tuple and two preservation transformations (Composition and Partial Synthesis) to iteratively reduce the plant size while preserving the solution set, culminating in a live controller for the remaining subproblem. Implemented in MTSA and evaluated on GR(1) DES benchmarks, the approach achieves substantial scalability gains, solving problems up to about 1000× larger than monolithic synthesis and showing favorable interactions with reactive-synthesis backends. The work demonstrates that modular synthesis can mitigate state explosion in GR(1) DES control and opens avenues for smarter heuristics, projection strategies, and extension to broader LTL classes.

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.

Paper Structure

This paper contains 27 sections, 6 theorems, 11 figures, 1 table, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Overview
  4. Overview without Minimization.
  5. Safe Controllers.
  6. Controlled Subplant.
  7. After the First Iteration.
  8. Introducing Minimization.
  9. Compositional Synthesis
  10. Composition
  11. Partial Synthesis
  12. Compositional Synthesis Algorithm
  13. Evaluation
  14. Compositional Synthesis of DES for GR(1) goals
  15. GR(1) DES Synthesis via Reactive Synthesis
  16. ...and 12 more sections

Key Result

theorem thmcountertheorem

Let $\varphi$ be an LTL formula, $\Sigma_c$ a set of controllable events, and $T$, $T'$ synthesis tuples $(\mathcal{M}, \mathcal{C}, \mu)$ and $(\mathcal{M'}, \mathcal{C}, \mu)$ respectively. If $\mathcal{M}_1$ and $\mathcal{M}_2$ are a partition of $\mathcal{M}$ such as $\mathcal{M'} = M \cup \math

Figures (11)

  • Figure 1: Modular plant for a control problem $\mathcal{E}$ with $\mathcal{M} = \{M_1, M_2, M_3\}$, GR(1) goal $\varphi = \text{$\square$}\text{$\lozenge$} uA1 \implies \text{$\square$} \text{$\lozenge$} cG1 \wedge \text{$\square$} \text{$\lozenge$} cG2$ and controllable alphabet $\Sigma_c = \{cG1, cG2, c1, c2\}$.
  • Figure 2: Parallel composition of subplant $\mathcal{M}' = \{M_1, M_2\} \subset \mathcal{M}$, i.e., $M_1 \| M_2$.
  • Figure 3: Safe Controller $(\mathcal{M}_1 \| M_2)_{\hbox{\scriptsize safe}}$ for subplant $M_1 \| M_2$, $\varphi' = \text{$\square$}\text{$\lozenge$} uA1 \implies \top \wedge \text{$\square$}\text{$\lozenge$} cG2$, controllable events $\Sigma_c \cup \{u3\}$, and $\mu = \emptyset$.
  • Figure 4: Controlled Subplant $(M_1 || M_2)_{\hbox{\scriptsize cont}}$ built from the safe controller $(M_1 || M_2)_{\hbox{\scriptsize safe}}$ in Fig. \ref{['fig:safe-controller']} by adding $u3$ transitions from state 0 and state 4 to a deadlock state
  • Figure 5: Controller $(M_3 \| (M_1 \| M_2)_{cont})_{live}$ for Fig.11.
  • ...and 6 more figures

Theorems & Definitions (24)

  • definition thmcounterdefinition: Labelled Transition System
  • definition thmcounterdefinition: Parallel composition
  • definition thmcounterdefinition: Controllably reachable
  • definition thmcounterdefinition: Controllably reachable
  • definition thmcounterdefinition: Legal LTS
  • definition thmcounterdefinition: Linear Temporal Logic (LTL) formula
  • definition thmcounterdefinition: Control Problem
  • definition thmcounterdefinition: Winning States
  • definition thmcounterdefinition: Generalised Reactivity(1) Piterman:2006:SRD
  • definition thmcounterdefinition: Synthesis observation equivalence mohajerani_framework_2014
  • ...and 14 more