ﻻ يوجد ملخص باللغة العربية
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.
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 co
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 syn
Temporal logics provide a formalism for expressing complex system specifications. A large body of literature has addressed the verification and the control synthesis problem for deterministic systems under such specifications. For stochastic systems
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 t
We consider the problem of stabilization of a linear system, under state and control constraints, and subject to bounded disturbances and unknown parameters in the state matrix. First, using a simple least square solution and available noisy measurem