PaperlayerView exact revision on arXiv

Source-linked AI summary

Feedback Refinement Relations for the Synthesis of Symbolic Controllers

Gunther Reissig, Alexander Weber, Matthias Rungger

arXiv:1503.03715v3math.OCcs.LOeess.SY

TL;DR

The paper addresses practical and theoretical problems in abstraction-based controller refinement, especially exact-state requirements and refinement complexity. It introduces feedback refinement relations and associated abstraction methods, obtaining robust correct-by-design controllers using quantized state information and static quantizers, with canonical abstractions demonstrated computationally.

  • Problem

    Abstraction-based refinement can require exact concrete states and embed very large abstractions in refined controllers, hindering practical implementation.

  • Method

    The paper introduces feedback refinement relations and constructs abstractions for perturbed nonlinear control systems using state covers and attainable-set over-approximations.

  • Results

    The framework synthesizes controllers that robustly and provably enforce specifications under uncertainties and disturbances, using quantized state information and a static quantizer.

  • Takeaways & Limitations

    Feedback refinement relations provide necessary and sufficient conditions for the targeted controller refinement properties and support canonical abstraction construction.

Abstract

from arXiv · show

We present an abstraction and refinement methodology for the automated controller synthesis to enforce general predefined specifications. The designed controllers require quantized (or symbolic) state information only and can be interfaced with the system via a static quantizer. Both features are particularly important with regard to any practical implementation of the designed controllers and, as we prove, are characterized by the existence of a feedback refinement relation between plant and abstraction. Feedback refinement relations are a novel concept introduced in this paper. Our work builds on a general notion of system with set-valued dynamics and possibly non-deterministic quantizers to permit the synthesis of controllers that robustly, and provably, enforce the specification in the presence of various types of uncertainties and disturbances. We identify a class of abstractions that is canonical in a well-defined sense, and provide a method to efficiently compute canonical abstractions. We demonstrate the practicality of our approach on two examples.

I. Introduction

The paper develops abstraction-based controller synthesis that resolves state-information and refinement-complexity issues through feedback refinement relations, while supporting robust specifications under uncertainty.

  • Automated synthesis merges controller design and verification to produce controllers that provably enforce formal specifications on plants.
  • Existing abstraction workflows lift infinite systems to finite abstractions, solve an abstract control problem, and refine the controller back to the concrete system.
  • Simulation-based refinement can require exact concrete states and produce refined controllers containing very large abstractions, creating implementation obstacles.
  • Feedback refinement relations connect abstract controllers to plants through a static quantizer and are necessary as well as sufficient for the targeted refinement properties.
  • The framework supports set-valued dynamics and possibly nondeterministic quantizers, enabling robust enforcement amid plant uncertainties, input disturbances, and state-measurement errors.
  • The paper identifies canonical abstractions, provides a computation method for perturbed nonlinear sampled systems, and demonstrates practicality on autonomous-vehicle path planning and aircraft landing.

II. Notation

This section establishes notation for sets, intervals, signals, maps, relations, inverses, and composition used throughout the system-theoretic development.

  • Relative complements, real and integer sets, and closed, open, and half-open continuous or discrete intervals receive explicit notation.
  • Vector inequalities in R^n are interpreted component-wise, while set-valued and ordinary maps are distinguished by ⇒ and →.
  • Set-valued maps are identified with binary relations, and inverse mappings and function composition are defined explicitly.
  • The notation B∞ denotes signals taking values in B over intervals of the form [0; T[.

A. Systems

The paper generalizes dynamical systems with internal variables and set-valued dynamics so serial interconnections can represent nondeterministic behavior and disturbances.

  • Set-valued transition and output functions provide a unified description of disturbances and nondeterminism.
  • The basic system class is not closed under interconnection when composed states are restricted to products of component state alphabets.
  • Internal variables impose interconnection constraints and recover serially composed behavior within the generalized system form.
  • A system is defined as a septuple with nonempty state, input, internal-variable, and output sets, strict output dynamics, and a transition function.
  • The paper defines autonomous, static, Moore, and simple systems, and assumes throughout that the plant is simple.

B. System composition

The paper defines serial and feedback composition for systems, including quantizer interconnections, and characterizes the resulting closed loop under a Moore-controller condition.

  • Serial composition: Serial composition combines systems when the first output alphabet is contained in the second input alphabet, using product states and set-valued dynamics.
  • Serial composition: Input and state quantizers are modeled as strict static systems connected through serial composition, with state quantizers yielding quantized measurements.
  • Feedback composition: Feedback composition requires compatible input-output alphabets and a Moore second system, together with condition (Z) governing blocking behavior.
  • Feedback composition: The feedback closed loop uses product state, internal-variable, and output alphabets, with transition and output relations formed from both component systems.
  • Feedback composition: The Moore assumption prevents delay-free cycles, while condition (Z) helps preserve non-blocking behavior from concrete to abstract closed loops.
  • Feedback composition: The composed system is autonomous and Moore, and its solutions correspond exactly to compatible solutions of the two component systems.

IV. Motivation

The motivation section shows that standard abstraction-based refinement can require exact plant-state information or a more complex refined controller. Two examples demonstrate these issues for alternating simulation relations and related variants.

  • Scope of the issue: The examples indicate that the two drawbacks are intrinsic to alternating simulation, bisimulation, and approximate variants rather than to a particular refinement technique.The same concerns are relevant when symbolic state information and bounded refined-controller complexity are required.
  • Controller refinement: Abstraction-based controller design uses reproducibility of concrete closed-loop behavior by the abstract closed loop to transfer satisfied properties.The abstract system is used to provide evidence that corresponding properties hold for the concrete closed loop.
  • State information issue: Alternating simulation relations can make the refined controller require full concrete-state information rather than only symbolic observations.The first example shows that a symbolic controller cannot attain reproducibility for the illustrated plant and abstraction.
  • Refinement complexity issue: A static abstract controller may fail to refine to a static concrete controller even when the relation requires identical inputs.The second example constructs a contradiction in the abstract closed-loop dynamics despite the abstract and concrete controllers being static.
  • Refinement complexity issue: The second example attributes the failure to one-step transition requirements that do not preserve the history encoded by the abstract dynamics.The concrete plant may need a dynamic controller to provide information that its state does not encode.

V. Feedback Refinement Relations

The paper introduces feedback refinement relations as a new system relation for comparing systems in controller synthesis.

  • V. Feedback Refinement Relations: Feedback refinement relations are introduced as a novel means to compare systems in the context of controller synthesis.The section focuses on simple systems.

A. Definition and basic properties

This section defines system behavior and feedback refinement relations through state-dependent admissible inputs and successor-state conditions, then establishes reflexivity and transitivity.

  • A. Definition and basic properties: The behavior B(S) consists of finite or infinite input-output signals generated by solutions, including terminating signals when continuation becomes impossible.Finite signals are included when the terminal state-input pair has no successor.
  • A. Definition and basic properties: Admissible inputs are defined separately at each state through the state-dependent input set U_S(x).The image of a state subset under U_S is also defined for later relation statements.
  • A. Definition and basic properties: A feedback refinement relation Q requires every abstractly admissible input to be admissible concretely and to preserve all related concrete successors.The conditions are U_S2(x2) ⊆ U_S1(x1) and Q(F1(x1,u)) ⊆ F2(x2,u).
  • A. Definition and basic properties: Unlike alternating simulation, feedback refinement requires the same input u in both systems rather than merely an associated concrete input.Its successor condition also requires the abstract transition for every state related to a concrete successor.
  • A. Definition and basic properties: Feedback refinement is reflexive and transitive: identity relates a system to itself, and relations compose across three systems.If S1 ≼_Q S2 and S2 ≼_R S3, then S1 ≼_(R◦Q) S3.

B. Feedback composability and behavioral inclusion

The composability result shows how a feedback refinement relation supports controller composition and behavioral reproducibility when one system is treated as a plant and another as its abstraction.

  • B. Feedback composability and behavioral inclusion: Given a feedback refinement relation, the relevant composed systems are feedback composable with the controller, and both closed-loop behaviors are reproducible by the controller composed with the abstraction.The result applies to C × (Q ◦ S1) and (C ◦ Q) × S1 relative to C × S2.
  • B. Feedback composability and behavioral inclusion: When S1 is the plant and S2 its abstraction, Q can represent the measurement map available to a controller that observes the plant only through Q.Under this interpretation, Q ◦ S1 represents the system for which a controller is sought.

V.4 Theorem. Let Q be a feedback refinement relation from the system S1 to the system S2, and assume that the system C is feedback composable with S2. Then the following holds.

A feedback refinement relation transfers controller behavior between an abstraction and its plant while preserving feedback composability and closed-loop behavior. The relation is also necessary for the stated controller-refinement property.

  • Theorem: A feedback refinement relation ensures that plant-controller behavior can be reproduced through the abstraction and its quantized interconnection.The theorem’s proof establishes the required composability and behavior inclusions for both interconnection orders.
  • Necessity: The relation is necessary: if every controller composable with S2 transfers through Q while preserving behavior inclusion, then Q is a feedback refinement relation.This applies to simple systems with a strict relation Q.
  • Control problem: The synthesis framework defines control problems by requiring a controller to be feedback composable with the system and its closed loop to satisfy a specification.Specifications may be arbitrary subsets of output sequences, including properties beyond LTL.
  • Controller refinement: A concrete control problem can be solved indirectly through an abstract control problem whose solution induces a solution for the concrete system.The abstract specification is associated with the plant, abstraction, relation, and concrete specification.

B. Uncertainties and disturbances

The framework incorporates plant, input, measurement, and output disturbances into robust controller synthesis. It uses an auxiliary unperturbed problem, robust specifications, and canonical cover-based abstractions to preserve the target specification.

  • Robust synthesis: Robust synthesis accounts for plant uncertainties, input disturbances, and measurement errors through set-valued dynamics and quantization.The framework reduces robust controller synthesis to solving an auxiliary unperturbed control problem.
  • Robust synthesis: If the controller solves the auxiliary problem with robust specification ˆΣ1, the perturbed closed-loop behavior is a subset of the original specification Σ1.The auxiliary quantizer is ˆQ = Q ◦P2, incorporating measurement disturbances before quantization.
  • Measurement errors: Replacing the disturbed quantizer with an auxiliary transition map can admit behaviors that violate the specification.The example includes the behavior sequence (0, a), (1, c), (1, c), (1, c), . . . despite solving the alternative auxiliary problem.
  • Measurement errors: A deterministic quantizer is non-robust under nonzero measurement uncertainty because Q ◦P2 is deterministic only when ε = 0.Here P2 maps each state to a closed Euclidean ball of radius ε, while Q maps a partition of R^n.
  • Canonical abstractions: The set-membership relation with a cover-based abstraction is canonical, and the abstraction can be constructed from the plant and the chosen cover.The construction uses non-empty subsets covering the concrete state alphabet and transition over-approximation conditions.

B. Canonicity result

Under condition (C), the paper constructs a canonical intermediate abstraction whose state space covers the concrete state space and that preserves feedback refinement in both directions. This abstraction can be derived from the existing abstraction and quantizer alone.

  • Assumption: Condition (C) holds automatically for quotient abstractions and for several relations associated with deterministic attainable-set over-approximations.
  • Canonicity theorem: Condition (C) supports constructing a simple intermediate system S2, relation R, and specification Σ2 between the concrete and abstract control problems.
  • Canonicity theorem: The resulting refinement chain is (S1, Σ1) ≼∈ (S2, Σ2) ≼R (S3, Σ3), with X2 a cover of X1 by non-empty subsets.
  • Construction: Its states are non-empty quantizer fibers, while transitions are obtained by inverse-image propagation through the relation R.
  • Application: For sampled perturbed systems, abstractions built from covers and growth bounds satisfy the feedback refinement relation S1 ≼∈ S2.

C. A growth bound

The paper develops growth bounds for perturbed continuous-time systems by bounding neighboring-solution distances component-wise with matrix-valued Lipschitz inequalities. These bounds support attainable-set over-approximations and less conservative abstractions.

  • Construction: The growth-bound construction applies a matrix-valued Lipschitz inequality to over-approximate attainable sets of continuous-time perturbed control systems.
  • Theorem VIII.5: For continuously differentiable dynamics with bounded perturbations and suitable invariant convex sets, Theorem VIII.5 provides a growth bound β.
  • Computation: The required derivative bounds can be computed using interval arithmetic, after which evaluating β is straightforward.
  • Guarantee: If the initial distance satisfies |ξ1(0) − ξ2(0)| ≤ ρ(0), then the bound guarantees |ξ1(t) − ξ2(t)| ≤ ρ(t) throughout the sampling interval.
  • Periodic systems: Periodic dynamics can be exploited to obtain finite abstractions capable of reproducing solutions unbounded along period directions.

A. A path planning problem for an autonomous vehicle

The autonomous-vehicle example uses a sampled bicycle model to synthesize a controller that patrols between two target regions while avoiding obstacles. A canonical finite abstraction is constructed and solved, then refined to the concrete control problem.

  • Problem formulation: The vehicle follows a bicycle-model dynamics with position, orientation, rear-wheel velocity, and steering angle as its states and inputs.The state is x = (x1, x2, x3), while u1 and u2 denote rear-wheel velocity and steering angle.
  • Problem formulation: The control objective is infinite patrolling between two target regions while avoiding obstacles from a specified initial state.The sampled system uses sampling time τ = 0.3, with A1,r1 and A1,r2 as the two target regions.
  • Abstraction construction: A canonical abstraction is constructed using the system’s period and a growth bound that depends on the control input.The abstraction uses the period p = (0, 0, 2π), a finite input alphabet, and β(r, u) = e^L(u)τr.
  • Abstraction construction: The abstraction contains 37,266,181 transitions and is computed in 2.25 seconds on an Intel Core i7 2.9 GHz.The abstract specification marks cells intersecting the initial and obstacle regions and cells contained in the target regions.
  • Controller synthesis: The abstract control problem is solved within 0.54 seconds, and its solution is refined to the concrete system.The solution uses nested fixed-point iterations, with a Dijkstra-like algorithm for the inner fixed point.
  • Controller synthesis: The framework is intended to produce controllers using quantized state information and a static quantizer while accommodating uncertainties and disturbances.The conclusion also identifies canonical abstractions for perturbed nonlinear systems and notes that computational effort grows rapidly with plant dimension.
Loading 1503.03715v3…