Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient Reactive Synthesis

Xin Ye, Harald Ruess

TL;DR

GXU addresses realizability of an expressive LTL fragment tailored for embedded control and provides a structural, correct-by-construction synthesis workflow. The approach builds Mealy machines with monitors from GXU guarantees and reduces realizability to a polynomial-time $2QBF$ validity problem; unrealizable specs are repaired by mining environment assumptions using $Padoa$'s definability and $Craig$ interpolation. This yields a complete, polynomial-time realizability procedure for GXU, strictly surpassing GR(1) and GXW in expressiveness while remaining amenable to extension with clocks and data constraints. The methodology is demonstrated via case studies and discusses practical integration into PLC-like design flows.

Abstract

Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizability for GXU specifications is shown to be equivalent to solving a certain subclass of 2QBF satisfiability problems. These logical problems can be solved in cubic time in the size of GXU specifications. For unrealizable GXU specifications, stronger environment assumptions are mined from failed consistency checks based on Padoa's characterization of definability and Craig interpolation.

Efficient Reactive Synthesis

TL;DR

GXU addresses realizability of an expressive LTL fragment tailored for embedded control and provides a structural, correct-by-construction synthesis workflow. The approach builds Mealy machines with monitors from GXU guarantees and reduces realizability to a polynomial-time validity problem; unrealizable specs are repaired by mining environment assumptions using 's definability and interpolation. This yields a complete, polynomial-time realizability procedure for GXU, strictly surpassing GR(1) and GXW in expressiveness while remaining amenable to extension with clocks and data constraints. The methodology is demonstrated via case studies and discusses practical integration into PLC-like design flows.

Abstract

Our main result is a polynomial time algorithm for deciding realizability for the GXU sublogic of linear temporal logic. This logic is particularly suitable for the specification of embedded control systems, and it is more expressive than GR(1). Reactive control programs for GXU specifications are represented as Mealy machines, which are extended by the monitoring of input events. Now, realizability for GXU specifications is shown to be equivalent to solving a certain subclass of 2QBF satisfiability problems. These logical problems can be solved in cubic time in the size of GXU specifications. For unrealizable GXU specifications, stronger environment assumptions are mined from failed consistency checks based on Padoa's characterization of definability and Craig interpolation.
Paper Structure (6 sections, 1 theorem, 4 equations)

This paper contains 6 sections, 1 theorem, 4 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Propositional Logic.
  4. Quantified Propositional Logic.
  5. Linear Temporal Logic.
  6. GXU Logic

Key Result

lemma thmcounterlemma

Let $\varphi$ be a propositional formula, $X \subsetneq vars(\varphi)$, $v \in vars(\varphi) \setminus X$, and $\varphi'$ be the propositional formula obtained by replacing every variable $y \in vars(\varphi) \setminus X$ with a fresh variable $y'$. Then $v$ is defined by $\varphi$ in $X$ if and onl

Theorems & Definitions (3)

  • lemma thmcounterlemma: Padoa padoa1901essai
  • definition thmcounterdefinition: GXU Formulas
  • definition thmcounterdefinition: Reactive GXU Specifications