We present the proof-of-concept tool formalSpec for semi-automatic translation of system requirements from controlled natural language into hybrid automata. These can be automatically integrated as monitor automata with an existing SpaceEx system model.

This paper proposes a simplified hybrid model of a freight train equipped with an air brake. The control of such a system and the enforcement of numerous safety constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems. Category: industrial Difficulty: high

In this paper, we provide a toolchain that facilitates the integration of formal verification techniques into model-based design. Applying verification tools to industrially relevant models requires three main ingredients: a formal model, a formal verification method, and a set of formal specifications. Our focus is on hybrid automata as the model and on reachability analysis as the method. Much progress has been made towards developing efficient and scalable reachability algorithms tailored to hybrid automata. However, it is not easy to encode rich formal specifications such that they can be interpreted by existing tools for reachability. Herein, we consider specifications expressed in pattern templates which are predefined properties with placeholders for state predicates. Pattern templates are close to the natural language and can be easily understood by both expert and non-expert users. We provide (i) formal definitions for selected patterns in the formalism of hybrid automata and (ii) monitors which encode the properties as the reachability of an error state. By composing these monitors with the formal model under study, the property can be checked by off-the-shelf fully automated verification tools. We illustrate the workflow on an electromechanical brake use case.

This paper proposes a simplified nonlinear model of a wind turbine equipped with a switching controller. The composition of wind turbine and controller results in a hybrid system. The control of such a system and the enforcement of numerous safety and performance constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems. Category: industrial Difficulty: high

This paper proposes a simplified nonlinear model of a wind turbine equipped with a switching controller. The composition of wind turbine and controller results in a hybrid system. The control of such a system and the enforcement of numerous safety and performance constraints constitute a relevant benchmark to evaluate tools for proving safety requirements in hybrid systems.

We consider the problem of constructing decentralized state feedback controllers for linear continuous-time systems. Different from existing approaches, where the topology of the controller is fixed a priori, the topology of the controller is part of the optimization problem. Structure optimization is done in terms of a minimization of the required feedback links and subject to a predefined bound on the tolerable loss of the achieved H-infinity-performance of the decentralized controller compared to an H-infinity-optimal centralized controller. We develop a computationally efficient formulation of the decentralized control problem by convex relaxations which makes it attractive for practical applications. The proposed design algorithm is applied to design sparse wide area control of a 3-area, 6-machine power system. (C) 2013 Elsevier Ltd. All rights reserved.

This paper considers the robust design of sparse relative sensing networks subject to a given H∞-performance constraint. The topology design considers heterogenous agents over weighted graphs. We develop a robust counterpart to the uncertain optimization problem and formulate the sparsity constraint via a convex ℓ1-relaxation. We also demonstrate how this relaxation can be used to embed additional performance criteria, such as the maximization of the algebraic connectivity of the relative sensing network.

We present an ℓ1-control scheme for multivariable pitch control in full load region. Two decoupled linear time-invariant models are derived using Coleman transformation and gain scheduling to design collective and individual pitch controllers independently. Individual pitch control is used to decrease the blade root bending moment. A new ℓ1-control setup for collective pitch control taking into account the collective bending moment in Coleman mode is presented. This further decreases the blade root bending moment while rotor speed is maintained constant above rated wind conditions. Simulations with a full nonlinear aeroelastic model over the whole load region show the applicability of the proposed control strategy and lifetime weighted damage equivalent loads are computed. Compared to classical collective and individual pitch control, a significant load reduction is achieved without losses in energy production.

This paper considers the problem of designing sparse relative sensing networks (RSN) subject to a given ℌ ∞ -performance constraint. The topology design considers homogeneous and heterogeneous agents over weighted graphs. We develop a computationally efficient formulation of the sparse topology design via a convex ℓ 1 -relaxation. This makes the proposed algorithm attractive for practical applications. We also demonstrate how this relaxation can be used to embed additional performance criteria, such as maximization of the algebraic connectivity of the RSN.

We consider the problem of constructing decentralized state feedback controllers for linear continuous-time systems. Different from existing approaches, where the topology of the controller is fixed a-priori, the topology of the controller is part of the optimization problem. Structure optimization is done in terms of a minimization of the required feedback and subject to a predefined bound on the tolerable loss of the achieved H∞-performance of the decentralized controller compared to an H∞-optimal centralized controller. We develop a computationally efficient formulation of the decentralized control problem by convex relaxations which makes it attractive for practical applications.

This work considers the role that cycles play in consensus networks. We show how the presence of cycles improve the H2 performance of the consensus network. In particular, we provide an explicit combinatorial characterization relating the length of cycles to the improvement in the performance of the network. This analysis points to a general trade-off between the length of the cycle and how many edges the cycle shares with other cycles. These analytic results are then used to motivate a design procedure for consensus networks based on an ℓ1 relaxation. This relaxation method leads to sparse and {0, 1}-solutions for the design of consensus graphs. A feature of the ℓ1 relaxation is the ability to include weighting terms in the objective. The choice of weighting functions are related to the combinatorial properties of the graph. The applicability of this scheme is then shown via a set of numerical examples.

We address the design of structured controllers for linear discrete-time systems. Decentralized controllers are designed that use local measurements and a minimal number of additional measurement links between the subsystems and the controllers. The structure of the decentralized controller, i.e. the additional links between the subsystems and the controllers, is not specified in advance but included into the controller design. We consider static output feedback for multivariable subsystems and define a pattern matrix to deal with the block structure of the controller. We formulate this problem as a maximization of the degree of decentralization, subject to a given H∞-performance. For the resulting non-convex optimization problem, numerically tractable convex relaxations are provided and an example shows the effectiveness of this approach.

Abstract This paper introduces the concept of an ℓ0-system gain for discrete-time LTI systems. It is shown that the ℓ0-gain is characterized by the number of non-zero entries in the impulse response of the system and hence gives a natural extension of the notion of sparsity from signals to systems. With this newly introduced system gain, we give a system theoretic explanation of the sparse closed loop response of ℓ1-optimal controlled systems by showing that the ℓ1-optimal control problem is the best convex relaxation (in the sense of Lagrangian duality) of an appropriately defined ℓ0-optimal control problem.

We address the design of structured controllers for networks of interconnected multivariable discrete-time subsystems. Different from existing approaches, where the structure of the controller is fixed a priori, we aim to design decentralised controllers such that each subsystem has a controller, which may not only use the output of its own associated subsystem, but also selected outputs of other subsystems. The total number of all those additional outputs used is to be minimised, while satisfying a guaranteed level of H-infinity-performance. For the resulting non-convex optimisation problem, we first present a novel characterisation of the H-infinity-performance of the closed-loop system by means of a system augmentation approach. Then, stimulated from compressive sensing theory, we propose a weighted l(1)-minimisation to relax the l(0) objective function for structure optimisation. We develop an algorithm to deal with the relaxed decentralisation control problem, where the controller is obtained by iteratively solving convex optimisation problems. In addition, an iterative algorithm is developed to optimise the initial values such that the solvability of the decentralised control problem is further improved. Finally, an example is given to show the effectiveness of the proposed approaches.

LIDAR (Light detection and ranging) systems are able to provide preview information of wind disturbances at various distances in front of wind turbines. This information can be used to improve the control of wind turbines. This paper compares a predictive feedforward control structure combined with common PI controllers to a baseline controller and to an H∞ approach showing the advantage of look-ahead control to reduce wind turbine loads. The control design is verified by simulations with a turbulent wind field and a full nonlinear model of the wind turbine.

This paper addresses the problem of controller order reduction for linear discrete-time systems. The proposed approach considers the minimization of an upper bound on the ℓ∞-gain of the error between the system with the full controller and the system with the reduced controller. This upper bound is defined using the so-called star norm performance. The method considers explicitly time-domain performance as a reduction criterion, and thus making this approach suitable for the order reduction of the generally large order ℓ1-optimal controllers. A sufficient solvability condition is provided in terms of LMIs with an extra equality constraint, which generally leads to a non-convex feasibility problem. An iterative algorithm with local convergence is used to overcome this problem. A numerical example is provided to confirm the effectiveness of the proposed controller reduction scheme.

This paper addresses the design of decentralized controllers for linear discrete-time systems. We consider state feedback control for networks of scalar interconnected systems. The structure of the decentralized controller is not specified in advance but included into the controller design. Decentralized controllers are designed based on local measurement with minimal number of additional measurement links between the subsystems and the controllers. We formulate this problem as one of maximizing the degree of decentralization subject to a given error performance in terms of the H∞-norm between the system controlled by a centralized controller and the system controlled by the decentralized controller. For the resulting non-convex optimization problem, numerically tractable convex relaxations are provided and an example shows the effectiveness of this approach.