Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userA Specification-Guided Framework for Temporal Logic Control of Nonlinear Systems
128
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
This paper proposes a specification-guided framework for control of nonlinear systems with linear temporal logic (LTL) specifications. In contrast with well-known abstraction-based methods, the proposed framework directly characterizes the winning set, i.e., the set of initial conditions from which a given LTL formula can be realized, over the continuous state space of the system via a monotonic operator. Following this characterization, an algorithm is proposed to practically approximate the operator via an adaptive interval subdivision scheme, which yields a finite-memory control strategy. We show that the proposed algorithm is sound for full LTL specifications, and robustly complete for specifications recognizable by deterministic Buchi automata (DBA), the latter in the sense that control strategies can be found whenever the given specification can be satisfied with additional bounded disturbances. Without having to compute and store the abstraction and the resulting product system with the DBA, the proposed method is more memory efficient, which is demonstrated by complexity analysis and performance tests. A pre-processing stage is also devised to reduce computational cost via a decomposition of the specification. We show that the proposed method can effectively solve real-world control problems such as jet engine compressor control and motion planning for manipulators and mobile robots.
rate research
Read More
We propose algorithms for performing model checking and control synthesis for discrete-time uncertain systems under linear temporal logic (LTL) specifications. We construct temporal logic trees (TLT) from LTL formulae via reachability analysis. In contrast to automaton-based methods, the construction of the TLT is abstraction-free for infinite systems, that is, we do not construct discrete abstractions of the infinite systems. Moreover, for a given transition system and an LTL formula, we prove that there exist both a universal TLT and an existential TLT via minimal and maximal reachability analysis, respectively. We show that the universal TLT is an underapproximation for the LTL formula and the existential TLT is an overapproximation. We provide sufficient conditions and necessary conditions to verify whether a transition system satisfies an LTL formula by using the TLT approximations. As a major contribution of this work, for a controlled transition system and an LTL formula, we prove that a controlled TLT can be constructed from the LTL formula via control-dependent reachability analysis. Based on the controlled TLT, we design an online control synthesis algorithm, under which a set of feasible control inputs can be generated at each time step. We also prove that this algorithm is recursively feasible. We illustrate the proposed methods for both finite and infinite systems and highlight the generality and online scalability with two simulated examples.
We study the problem of controlling multi-agent systems under a set of signal temporal logic tasks. Signal temporal logic is a formalism that is used to express time and space constraints for dynamical systems. Recent methods to solve the control synthesis problem for single-agent systems under signal temporal logic tasks are, however, subject to a high computational complexity. Methods for multi-agent systems scale at least linearly with the number of agents and induce even higher computational burdens. We propose a computationally-efficient control strategy to solve the multi-agent control synthesis problem that results in a robust satisfaction of a set of signal temporal logic tasks. In particular, a decentralized feedback control law is proposed that is based on time-varying control barrier functions. The obtained control law is discontinuous and formal guarantees are provided by nonsmooth analysis. Simulations show the efficacy of the presented method.
A framework for the event-triggered control synthesis under signal temporal logic (STL) tasks is proposed. In our previous work, a continuous-time feedback control law was designed, using the prescribed performance control technique, to satisfy STL tasks. We replace this continuous-time feedback control law by an event-triggered controller. The event-triggering mechanism is based on a maximum triggering interval and on a norm bound on the difference between the value of the current state and the value of the state at the last triggering instance. Simulations of a multi-agent system quantitatively show the efficacy of using an event-triggered controller to reduce communication and computation efforts.
This paper studies the robust satisfiability check and online control synthesis problems for uncertain discrete-time systems subject to signal temporal logic (STL) specifications. Different from existing techniques, this work proposes an approach based on STL, reachability analysis, and temporal logic trees. Firstly, a real-time version of STL semantics and a tube-based temporal logic tree are proposed. We show that such a tree can be constructed from every STL formula. Secondly, using the tube-based temporal logic tree, a sufficient condition is obtained for the robust satisfiability check of the uncertain system. When the underlying system is deterministic, a necessary and sufficient condition for satisfiability is obtained. Thirdly, an online control synthesis algorithm is designed. It is shown that when the STL formula is robustly satisfiable and the initial state of the system belongs to the initial root node of the tube-based temporal logic tree, it is guaranteed that the trajectory generated by the controller satisfies the STL formula. The effectiveness of the proposed approach is verified by an automated car overtaking example.
This paper focuses on developing a new paradigm motivated by investigating the consensus problem of networked Lagrangian systems with time-varying delay and switching topologies. We present adaptive controllers with piecewise continuous or arbitrary times differentiable control torques for realizing consensus of Lagrangian systems, extending the results in the literature. This specific study motivates the formulation of a new paradigm referred to as forwardstepping, which is shown to be a systematic tool for solving various nonlinear control problems. One distinctive point associated with forwardstepping is that the order of the reference dynamics is typically specified to be equal to or higher than that of the original nonlinear system, and the reference dynamics and the nonlinear system are governed by a differential/dynamic-cascaded structure. The order invariance or increment of the specified reference dynamics with respect to the nonlinear system and their differential/dynamic-cascaded structure expands significantly the design freedom and thus facilitates the seeking of solutions to many nonlinear control problems which would otherwise often be intractable.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
