-
Efficient Automata-based Planning and Control under Spatio-Temporal Logic Specifications
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
The use of spatio-temporal logics in control is motivated by the need to impose complex spatial and temporal behavior on dynamical systems, and to control these systems accordingly. Synthesizing correct-by-design control laws is a challenging task resulting in computationally demanding methods. We consider efficient automata-based planning for continuous-time systems under signal interval temporal…
▽ More
The use of spatio-temporal logics in control is motivated by the need to impose complex spatial and temporal behavior on dynamical systems, and to control these systems accordingly. Synthesizing correct-by-design control laws is a challenging task resulting in computationally demanding methods. We consider efficient automata-based planning for continuous-time systems under signal interval temporal logic specifications, an expressive fragment of signal temporal logic. The planning is based on recent results for automata-based verification of metric interval temporal logic. A timed signal transducer is obtained accepting all Boolean signals that satisfy a metric interval temporal logic specification, which is abstracted from the signal interval temporal logic specification at hand. This transducer is modified to account for the spatial properties of the signal interval temporal logic specification, characterizing all real-valued signals that satisfy this specification. Using logic-based feedback control laws, such as the ones we have presented in earlier works, we then provide an abstraction of the system that, in a suitable way, aligns with the modified timed signal transducer. This allows to avoid the state space explosion that is typically induced by forming a product automaton between an abstraction of the system and the specification.
△ Less
Submitted 24 March, 2020; v1 submitted 24 September, 2019;
originally announced September 2019.
-
Decentralized Robust Control of Coupled Multi-Agent Systems under Local Signal Temporal Logic Tasks
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
Motivated by the recent interest in formal methods-based control of multi-agent systems, we adopt a bottom-up approach. Each agent is subject to a local signal temporal logic task that may depend on other agents behavior. These dependencies pose control challenges since some of the tasks may be opposed to each other. We first develop a local continuous feedback control law and identify conditions…
▽ More
Motivated by the recent interest in formal methods-based control of multi-agent systems, we adopt a bottom-up approach. Each agent is subject to a local signal temporal logic task that may depend on other agents behavior. These dependencies pose control challenges since some of the tasks may be opposed to each other. We first develop a local continuous feedback control law and identify conditions under which this control law guarantees satisfaction of the local tasks. If these conditions do not hold, we propose to use the developed control law in combination with an online detection & repair scheme, expressed as a local hybrid system. After detection of a critical event, a three-stage procedure is initiated to resolve the problem. The theoretical results are illustrated in simulations.
△ Less
Submitted 25 February, 2018; v1 submitted 22 September, 2017;
originally announced September 2017.
-
Prescribed Performance Control for Signal Temporal Logic Specifications
Authors:
Lars Lindemann,
Christos K. Verginis,
Dimos V. Dimarogonas
Abstract:
Motivated by the recent interest in formal methods-based control for dynamic robots, we discuss the applicability of prescribed performance control to nonlinear systems subject to signal temporal logic specifications. Prescribed performance control imposes a desired transient behavior on the system trajectories that is leveraged to satisfy atomic signal temporal logic specifications. A hybrid cont…
▽ More
Motivated by the recent interest in formal methods-based control for dynamic robots, we discuss the applicability of prescribed performance control to nonlinear systems subject to signal temporal logic specifications. Prescribed performance control imposes a desired transient behavior on the system trajectories that is leveraged to satisfy atomic signal temporal logic specifications. A hybrid control strategy is then used to satisfy a finite set of these atomic specifications. Simulations of a multi-agent system, using consensus dynamics, show that a wide range of specifications, i.e., formation, sequencing, and dispersion, can be robustly satisfied.
△ Less
Submitted 19 September, 2017; v1 submitted 21 March, 2017;
originally announced March 2017.
-
Robust Motion Planning employing Signal Temporal Logic
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
Motion planning classically concerns the problem of accomplishing a goal configuration while avoiding obstacles. However, the need for more sophisticated motion planning methodologies, taking temporal aspects into account, has emerged. To address this issue, temporal logics have recently been used to formulate such advanced specifications. This paper will consider Signal Temporal Logic in combinat…
▽ More
Motion planning classically concerns the problem of accomplishing a goal configuration while avoiding obstacles. However, the need for more sophisticated motion planning methodologies, taking temporal aspects into account, has emerged. To address this issue, temporal logics have recently been used to formulate such advanced specifications. This paper will consider Signal Temporal Logic in combination with Model Predictive Control. A robustness metric, called Discrete Average Space Robustness, is introduced and used to maximize the satisfaction of specifications which results in a natural robustness against noise. The comprised optimization problem is convex and formulated as a Linear Program.
△ Less
Submitted 6 March, 2017;
originally announced March 2017.
-
Robust Control for Signal Temporal Logic Specifications using Average Space Robustness
Authors:
Lars Lindemann,
Dimos V. Dimarogonas
Abstract:
Control systems that satisfy temporal logic specifications have become increasingly popular due to their applicability to robotic systems. Existing control methods, however, are computationally demanding, especially when the problem size becomes too large. In this paper, a robust and computationally efficient model predictive control framework for signal temporal logic specifications is proposed.…
▽ More
Control systems that satisfy temporal logic specifications have become increasingly popular due to their applicability to robotic systems. Existing control methods, however, are computationally demanding, especially when the problem size becomes too large. In this paper, a robust and computationally efficient model predictive control framework for signal temporal logic specifications is proposed. We introduce discrete average space robustness, a novel quantitative semantic for signal temporal logic, that is directly incorporated into the cost function of the model predictive controller. The optimization problem entailed in this framework can be written as a convex quadratic program when no disjunctions are considered and results in a robust satisfaction of the specification. Furthermore, we define the predicate robustness degree as a new robustness notion. Simulations of a multi-agent system subject to complex specifications demonstrate the efficacy of the proposed method.
△ Less
Submitted 15 January, 2019; v1 submitted 24 July, 2016;
originally announced July 2016.
-
The ZEUS Forward Plug Calorimeter with Lead-Scintillator Plates and WLS Fiber Readout
Authors:
A. Bamberger,
S. Böttcher,
I. Bohnet,
J. P. Fernández,
F. Goebel,
P. Göttlicher,
A. Gabareen,
G. García,
N. Gendner,
R. Graciani,
M. Hauser,
D. Horstmann,
M. Inuzuka,
M. Kasemann,
B. Löhr,
R. Lewis,
H. Lim,
L. Lindemann,
P. Markun,
M. Martínez,
T. Neumann,
I. H. Park,
J. del Peso,
H. Raach,
A. Savin
, et al. (9 additional authors not shown)
Abstract:
A Forward Plug Calorimeter (FPC) for the ZEUS detector at HERA has been built as a shashlik lead-scintillator calorimeter with wave length shifter fiber readout. Before installation it was tested and calibrated using the X5 test beam facility of the SPS accelerator at CERN. Electron, muon and pion beams in the momentum range of 10 to 100 GeV/c were used. Results of these measurements are present…
▽ More
A Forward Plug Calorimeter (FPC) for the ZEUS detector at HERA has been built as a shashlik lead-scintillator calorimeter with wave length shifter fiber readout. Before installation it was tested and calibrated using the X5 test beam facility of the SPS accelerator at CERN. Electron, muon and pion beams in the momentum range of 10 to 100 GeV/c were used. Results of these measurements are presented as well as a calibration monitoring system based on a $^{60}$Co source.
△ Less
Submitted 21 December, 1999; v1 submitted 20 December, 1999;
originally announced December 1999.
