Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userZonotope-based Controller Synthesis for LTL Specifications
120
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic abstract
This paper studies the controller synthesis problem for Linear Temporal Logic (LTL) specifications using (constrained) zonotope techniques. To begin with, we implement (constrained) zonotope techniques to partition the state space and further to verify whether the LTL specification can be satisfied. Once the LTL specification can be satisfied, the next step is to design a controller to guarantee the satisfaction of the LTL specification for dynamic systems. Based on the verification of the LTL specification, an abstraction-based control design approach is proposed in this paper: a novel abstraction construction is developed first, then finite local abstract controllers are designed to achieve the LTL specification, and finally the designed abstract controllers are combined and refined as the controller for the original system. The proposed control design strategy is illustrated via a numerical example from autonomous robots.
rate research
Read More
Given a Markov decision process (MDP) and a linear-time ($omega$-regular or LTL) specification, the controller synthesis problem aims to compute the optimal policy that satisfies the specification. More recently, problems that reason over the asymptotic behavior of systems have been proposed through the lens of steady-state planning. This entails finding a control policy for an MDP such that the Markov chain induced by the solution policy satisfies a given set of constraints on its steady-state distribution. This paper studies a generalization of the controller synthesis problem for a linear-time specification under steady-state constraints on the asymptotic behavior. We present an algorithm to find a deterministic policy satisfying $omega$-regular and steady-state constraints by characterizing the solutions as an integer linear program, and experimentally evaluate our approach.
We show that given a desired closed-loop response for a system, there exists an affine subspace of controllers that achieve this response. By leveraging the existence of this subspace, we are able to separate controller design from closed-loop design by first synthesizing the desired closed-loop response and then synthesizing a controller that achieves the desired response. This is a useful extension to the recently introduced System Level Synthesis framework, in which the controller and closed-loop response are jointly synthesized and we cannot enforce controller-specific constraints without subjecting the closed-loop map to the same constraints. We demonstrate the importance of separating controller design from closed-loop design with an example in which communication delay and locality constraints cause standard SLS to be infeasible. Using our new two-step procedure, we are able to synthesize a controller that obeys the constraints while only incurring a 3% increase in LQR cost compared to the optimal LQR controller.
Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades. It consists in the synthesis of a controller that reacts to environments inputs satisfying a given temporal logic specification. Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability. In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (LTLEBR), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from LTLEBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification. We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.
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 investigates the online motion coordination problem for a group of mobile robots moving in a shared workspace, each of which is assigned a linear temporal logic specification. Based on the realistic assumptions that each robot is subject to both state and input constraints and can have only local view and local information, a fully distributed multi-robot motion coordination strategy is proposed. For each robot, the motion coordination strategy consists of three layers. An offline layer pre-computes the braking area for each region in the workspace, the controlled transition system, and a so-called potential function. An initialization layer outputs an initially safely satisfying trajectory. An online coordination layer resolves conflicts when one occurs. The online coordination layer is further decomposed into three steps. Firstly, a conflict detection algorithm is implemented, which detects conflicts with neighboring robots. Whenever conflicts are detected, a rule is designed to assign dynamically a planning order to each pair of neighboring robots. Finally, a sampling-based algorithm is designed to generate local collision-free trajectories for the robot which at the same time guarantees the feasibility of the specification. Safety is proven to be guaranteed for all robots at any time. The effectiveness and the computational tractability of the resulting solution is verified numerically by two case studies.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
