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

• URL: http://arxiv.org/abs/2506.16557v1
• Date: Thu, 19 Jun 2025 19:23:15 GMT
• Title: Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control
• Authors: Hernán Gagliardi, Victor Braberman, Sebastian Uchitel,
• Abstract summary: We present a compositional approach to controller synthesis of discrete event system controllers.<n>We exploit the modular structure of the plant to be controlled, given as a set of labelled transition systems.
• Score: 0.0
• License: http://creativecommons.org/publicdomain/zero/1.0/
• 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.

Related papers

• Autonomous Control Leveraging LLMs: An Agentic Framework for Next-Generation Industrial Automation [0.0]
  We introduce a unified agentic framework that leverages large language models (LLMs) for both discrete fault-recovery planning and continuous process control.<n>Our results demonstrate that, with structured feedback and modular agents, LLMs can unify high-level symbolic planningand low-level continuous control.
  arXiv  Detail & Related papers  (2025-07-03T11:20:22Z)
• Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives [2.7038841665524846]
  This work studies the problem of synthesizing optimal policies for perception-related objectives in environments modeled by partially observable Markov decision processes.<n>Our solution is to transform the mboxsc-iLTL objectives into reachability objectives by constructing the product of the belief MDP and a deterministic finite automaton built from the sc-iLTL objective.<n>To overcome the scalability challenge due to the product, we introduce a Monte Carlo Tree Search (MCTS) method that converges in probability to the optimal policy.
  arXiv  Detail & Related papers  (2025-06-27T22:02:07Z)
• SymRTLO: Enhancing RTL Code Optimization with LLMs and Neuron-Inspired Symbolic Reasoning [18.40402135952776]
  This paper presents SymRTLO, a novel neuron-symbolic RTL optimization framework.<n>A symbolic module is proposed for analyzing and optimizing finite state machine (FSM) logic.<n> Experiments on the RTL-Rewriter benchmark with Synopsys Design Compiler and Yosys show that SymRTLO improves power, performance, and area (PPA) by up to 43.9%, 62.5%, and 51.1%, respectively.
  arXiv  Detail & Related papers  (2025-04-14T16:15:55Z)
• Predictable and Performant Reactive Synthesis Modulo Theories via Functional Synthesis [1.1797787239802762]
  We show how to generate correct controllers from temporal logic specifications using classical reactive handles (propositional) as a specification language. We also show that our method allows responses in the sense that the controller can optimize its outputs in order to always provide the smallest safe values.
  arXiv  Detail & Related papers  (2024-07-12T15:23:27Z)
• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  We propose a novel decomposition algorithm based on modes. The input to our algorithm is the original specification and the description of the modes. We show how to generate sub-specifications automatically and we prove that if all sub-problems are realizable the full specification is realizable.
  arXiv  Detail & Related papers  (2023-12-14T08:01:35Z)
• Large Language Models as General Pattern Machines [64.75501424160748]
  We show that pre-trained large language models (LLMs) are capable of autoregressively completing complex token sequences. Surprisingly, pattern completion proficiency can be partially retained even when the sequences are expressed using tokens randomly sampled from the vocabulary. In this work, we investigate how these zero-shot capabilities may be applied to problems in robotics.
  arXiv  Detail & Related papers  (2023-07-10T17:32:13Z)
• MULTIGAIN 2.0: MDP controller synthesis for multiple mean-payoff, LTL and steady-state constraints [41.94295877935867]
  We present MULTIGAIN 2.0, a major extension to the controller synthesis tool MULTIGAIN. It is built on top of the probabilistic model checker PRISM.
  arXiv  Detail & Related papers  (2023-05-26T08:59:51Z)
• Learning Bounded Context-Free-Grammar via LSTM and the Transformer:Difference and Explanations [51.77000472945441]
  Long Short-Term Memory (LSTM) and Transformers are two popular neural architectures used for natural language processing tasks. In practice, it is often observed that Transformer models have better representation power than LSTM. We study such practical differences between LSTM and Transformer and propose an explanation based on their latent space decomposition patterns.
  arXiv  Detail & Related papers  (2021-12-16T19:56:44Z)
• Deep Reinforcement Learning for Wireless Scheduling in Distributed Networked Control [37.10638636086814]
  We consider a joint uplink and downlink scheduling problem of a fully distributed wireless control system (WNCS) with a limited number of frequency channels.<n>We develop a deep reinforcement learning (DRL) based framework for solving it.<n>To tackle the challenges of a large action space in DRL, we propose novel action space reduction and action embedding methods.
  arXiv  Detail & Related papers  (2021-09-26T11:27:12Z)
• Learning Optimal Strategies for Temporal Tasks in Stochastic Games [23.012106429532633]
  We introduce a model-free reinforcement learning (RL) approach to derive controllers from given specifications. We learn optimal control strategies that maximize the probability of satisfying the specifications against the worst-case environment behavior.
  arXiv  Detail & Related papers  (2021-02-08T16:10:50Z)
• Policy Analysis using Synthetic Controls in Continuous-Time [101.35070661471124]
  Counterfactual estimation using synthetic controls is one of the most successful recent methodological developments in causal inference. We propose a continuous-time alternative that models the latent counterfactual path explicitly using the formalism of controlled differential equations.
  arXiv  Detail & Related papers  (2021-02-02T16:07:39Z)
• Gaussian Process-based Min-norm Stabilizing Controller for Control-Affine Systems with Uncertain Input Effects and Dynamics [90.81186513537777]
  We propose a novel compound kernel that captures the control-affine nature of the problem. We show that this resulting optimization problem is convex, and we call it Gaussian Process-based Control Lyapunov Function Second-Order Cone Program (GP-CLF-SOCP)
  arXiv  Detail & Related papers  (2020-11-14T01:27:32Z)
• LTLf Synthesis on Probabilistic Systems [0.0]
  synthesis is used to find a policy that maximizes the probability of achieving this behavior. No tools exist to solve policy synthesis for behaviors given finite-trace properties. We present two algorithms for solving this problem: the first via reduction of Markov Processes and the second native tools for automatonf.
  arXiv  Detail & Related papers  (2020-09-23T01:26:47Z)
• Learning Stabilizing Controllers for Unstable Linear Quadratic Regulators from a Single Trajectory [85.29718245299341]
  We study linear controllers under quadratic costs model also known as linear quadratic regulators (LQR) We present two different semi-definite programs (SDP) which results in a controller that stabilizes all systems within an ellipsoid uncertainty set. We propose an efficient data dependent algorithm -- textsceXploration -- that with high probability quickly identifies a stabilizing controller.
  arXiv  Detail & Related papers  (2020-06-19T08:58:57Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.