我们研究为非线性动力系统自动综合混合控制器的问题，该控制器需确保闭环系统满足任意 Linear Temporal Logic（线性时序逻辑）规范。此外，该规范还可考虑由外部环境或系统自身引发的逻辑上下文切换。最后，为保证可扩展性，我们希望避免传统的暴力时间与空间离散化方法。为此，我们提出一种新颖的两层策略综合方法：下层生成的控制器提供不变集和吸引域，上层逻辑层则以抽象方式利用这些集合。为实现这一目标，我们为上层和下层综合均提供了新技术。我们的新方法能够以可扩展的方式，同时利用状态空间控制技术的计算能力与有限博弈求解在处理复杂规范方面的智能。
英文摘要：
We consider the problem of automatically synthesizing a hybrid controller for non-linear dynamical systems which ensures that the closed-loop fulfills an arbitrary \emph{Linear Temporal Logic} specification. Moreover, the specification may take into account logical context switches induced by an external environment or the system itself. Finally, we want to avoid classical brute-force time- and space-discretization for scalability. We achieve these goals by a novel two-layer strategy synthesis approach, where the controller generated in the lower layer provides invariant sets and basins of attraction, which are exploited at the upper logical layer in an abstract way. In order to achieve this, we provide new techniques for both the upper- and lower-level synthesis.
Our new methodology allows to leverage both the computing power of state space control techniques and the intelligence of finite game solving for complex specifications, in a scalable way.
In previous work, linear time-invariant event-triggered control (ETC) systems were abstracted to finite-state systems that capture the original systems' sampling behaviour. It was shown that these abstractions can be employed for scheduling of communication traffic in networks of ETC loops. In this paper, we extend this framework to the class of nonlinear homogeneous systems, however adopting a different approach in a number of steps. Finally, we discuss how the proposed methodology could be extended to general nonlinear systems.
Self-triggered control (STC) is a sample-and-hold control method aimed at reducing communications within networked-control systems; however, existing STC mechanisms often maximize how late the next sample is, and as such they do not provide any sampling optimality in the long-term. In this work, we devise a method to construct self-triggered policies that provide near-maximal average inter-sample time (AIST) while respecting given control performance constraints. To achieve this, we rely on finite-state abstractions of a reference event-triggered control, in which early triggers are also allow…
Event-triggered control (ETC) is a major recent development in cyber-physical systems due to its capability of reducing resource utilization in networked devices. However, while most of the ETC literature reports simulations indicating massive reductions in the sampling required for control, no method so far has been capable of quantifying these results. In this work, we propose an approach through finite-state abstractions to do formal quantification of the traffic generated by ETC of linear systems, in particular aiming at computing its smallest average inter-sample time (SAIST). The method …
Recently, there have been efforts towards understanding the sampling behaviour of event-triggered control (ETC), for obtaining metrics on its sampling performance and predicting its sampling patterns. Finite-state abstractions, capturing the sampling behaviour of ETC systems, have proven promising in this respect. So far, such abstractions have been constructed for non-stochastic systems. Here, inspired by this framework, we abstract the sampling behaviour of stochastic narrow-sense linear periodic ETC (PETC) systems via Interval Markov Chains (IMCs). Particularly, we define functions over seq…
We provide a method to construct finite abstractions exactly bisimilar to linear systems under a modified periodic event-triggered control (PETC), when considering as output the inter-event times they generate. Assuming that the initial state lies on a known compact set, these finite-state models can exactly predict all sequences of sampling times until a specified Lyapunov sublevel set is reached. Based on these results, we provide a way to build tight models simulating the traffic of conventional PETC. These models allow computing tight bounds of the PETC average frequency and global exponen…
Event-triggered control (ETC) is claimed to provide enormous reductions in sampling frequency when compared to periodic sampling, but little is formally known about its generated traffic. This work shows that ETC can exhibit very complex, even chaotic traffic, especially when the triggering condition is aggressive in reducing communications. First, we characterize limit traffic patterns by observing invariant lines and planes through the origin, as well as their attractivity. Then, we present abstraction-based methods to compute limit metrics, such as limit average and limit inferior inter-sam…
This paper studies the reduction (abstraction) of finite-state transition systems for control synthesis problems. We revisit the notion of alternating simulation equivalence (ASE), a more relaxed condition than alternating bisimulations, to relate systems and their abstractions. As with alternating bisimulations, ASE preserves the property that the existence of a controller for the abstraction is necessary and sufficient for a controller to exist for the original system. Moreover, being a less stringent condition, ASE can reduce systems further to produce smaller abstractions. We provide an al…
Context-Triggered Robust MPC for Temporal Logic Specifications
Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）；Institute of Science and Technology Austria (ISTA)（奥地利科学技术研究院）；University of Birmingham（伯明翰大学）
We consider abstraction-based design of output-feedback controllers for non-linear dynamical systems against specifications over state-based predicates in linear-time temporal logic (LTL). In this context, our contribution is two-fold: (I) we generalize feedback-refinement relations for abstraction-based output-feedback control to systems with arbitrary predicate and observation maps, and (II) we introduce a new algorithm for the synthesis of abstract output-feedback controllers w.r.t. LTL specifications over unobservable state-based predicates. Our abstraction-based output-feedback controller…
We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original system and its abstraction which characterizes the …
Designing a Cyber-Physical System (CPS), including modeling the control components and services, is a challenging task. Using models and simulations during run-time is crucial for successfully implementing advanced control and prediction components. The complexity of designing an effective CPS system increases due to real-time constraints. Generating accurate predictions and making decisions using detailed models in various contexts is %can be computationally demanding and complex to manage within the available computational resources. Employing approximated models and switching to the most su…
In the context of networked control systems, event-triggered control (ETC) has emerged as a major topic due to its alleged resource usage reduction capabilities. However, this is mainly supported by numerical simulations, and very little is formally known about the traffic generated by ETC. This work devises a method to estimate, and in some cases to determine exactly, the minimum average inter-sample time (MAIST) generated by periodic event-triggered control (PETC) of linear systems. The method involves abstracting the traffic model using a bisimulation refinement algorithm and finding the cy…
We consider the computation of resilient controllers for perturbed non-linear dynamical systems w.r.t. linear-time temporal logic specifications. We address this problem through the paradigm of Abstraction-Based Controller Design (ABCD) where a finite state abstraction of the perturbed system dynamics is constructed and utilized for controller synthesis. In this context, our contribution is twofold: (I) We construct abstractions which model the impact of occasional high disturbance spikes on the system via so called disturbance edges. (II) We show that the application of resilient reactive syn…
The efficient utilization of available resources while simultaneously achieving control objectives is a primary motivation in the event-triggered control paradigm. In many modern control applications, one such objective is enforcing the safety of a system. The goal of this paper is to carry out this vision by combining event-triggered and safety-critical control design. We discuss how a direct transcription, in the context of safety, of event-triggered methods for stabilization may result in designs that are not implementable on real hardware due to the lack of a minimum interevent time. We pr…
Self-triggered control, a well-documented technique for reducing the communication overhead while ensuring desired system performance, is gaining increasing popularity. However, existing methods for self-triggered control require explicit system models that are assumed perfectly known a priori. An end-to-end control paradigm known as data-driven control learns control laws directly from data, and offers a competing alternative to the routine system identification-then-control method. In this context, the present paper puts forth data-driven self-triggered control schemes for unknown linear sys…
On the trade-off between control performance and communication cost in event-triggered control
ACCESS Linnaeus Centre, School of Electrical Engineering, KTH Royal Institute of Technology（皇家理工学院电气工程学院）；University of Notre Dame（圣母大学）；University of Newcastle（纽卡斯尔大学）
In systems where the ability to actuate is a scarce resource, e.g., spacecrafts, it is desirable to only apply a given controller in an intermittent manner--with periods where the controller is on and periods where it is off. Motivated by the event-triggered control paradigm, where state-dependent triggers are utilized in a sample-and-hold context, we generalize this concept to include state triggers where the controller is off thereby creating a framework for intermittent control. Our approach utilizes certificates--either Lyapunov or barrier functions--to design intermittent trigger laws tha…
In this work, we derive a region-based self-triggered control (STC) scheme for nonlinear systems with bounded disturbances and model uncertainties. The proposed STC scheme is able to guarantee different performance specifications (e.g. stability, boundedness, etc.), depending on the event-triggered control (ETC) triggering function that is chosen to be emulated. To deal with disturbances and uncertainties, we employ differential inclusions (DIs). By introducing ETC/STC notions in the context of DIs, we extend well-known results on ETC/STC to perturbed uncertain systems. Given these results, an…
Decentralized Dynamic Event-triggered Output-feedback Control of Stochastic Non-triangular Interconnected Systems with Unknown Time-varying Sensor Sensitivity
