arXiv subjects

Miel Sharf

Publications and source records attributed to Miel Sharf.

17 recordsLinked to original sources

arXiv2022

Contract Composition for Dynamical Control Systems: Definition and Verification using Linear Programming

Designing large-scale control systems to satisfy complex specifications is hard in practice, as most formal methods are limited to systems of modest size. Contract theory has been proposed as a modular alternative to formal methods in control, in which specifications are defined by assumptions on the input to a component and guarantees on its output. However, current contract-based methods for control systems either prescribe guarantees on the state of the system, going against the spirit of contract theory, or can only support rudimentary compositions. In this paper, we present a contract-based modular framework for discrete-time dynamical control systems. We extend the definition of contracts by allowing the assumption on the input at a time $k$ to depend on outputs up to time $k-1$, which is essential when considering the feedback connection of an unregulated dynamical system and a controller. We also define contract composition for arbitrary interconnection topologies, under the pretence of well-posedness, and prove that this notion supports modular design, analysis and verification. This is done using graph theory methods, and specifically using the notions of topological ordering and backward-reachable nodes. Lastly, we use $k$-induction to present an algorithm for verifying vertical contracts, which are claims of the form "the conjugation of given component-level contracts is a stronger specification than a given contract on the integrated system". These algorithms are based on linear programming, and scale linearly with the number of components in the interconnected network. A numerical example is provided to demonstrate the scalability of the presented approach, as well as the modularity achieved by using it.

eess.SY↗

arXiv2022

Cluster Assignment in Multi-Agent Systems : Sparsity Bounds and Fault Tolerance

We study cluster assignment in homogeneous diffusive multi-agent networks. Given the number of clusters and agents within each cluster, we design the network graph ensuring the system will converge to the prescribed cluster configuration. Using recent results linking clustering and symmetries, we show that it is possible to design an oriented graph for which the action of the automorphism group of the graph has orbits of predetermined sizes, guaranteeing the network will converge to the prescribed cluster configuration. We provide bounds on the number of edges needed to construct these graphs along with a constructive approach for their generation. We also consider the robustness of the clustering process under agent malfunction.

eess.SY↗

arXiv2022

Cluster Assignment in Multi-Agent Systems

We study cluster assignment in multi-agent networks. We consider homogeneous diffusive networks, and focus on design of the graph that ensures the system will converge to a prescribed cluster configuration, i.e., specifying the number of clusters and agents within each cluster. Leveraging recent results from cluster synthesis, we show that it is possible to design an oriented graph such that the action of the automorphism group of the graph has orbits of predetermined sizes, guaranteeing that the network will converge to the prescribed cluster configuration. We provide upper and lower bounds on the number of edges that are needed to construct these graphs along with a constructive approach for generating these graphs. We support our analysis with some numerical examples.

eess.SY↗

arXiv2021

Economic Dispatch of a Single Micro-Gas Turbine Under CHP Operation with Uncertain Demands

This work considers the economic dispatch problem for a single micro-gas turbine, governed by a discrete state-space model, under combined heat and power (CHP) operation and coupled with a utility. If the exact power and heat demands are given, existing algorithms can be used to give a quick optimal solution to the economic dispatch problem. However, in practice, the power and heat demands can not be known deterministically, but are rather predicted, resulting in an estimate and a bound on the estimation error. We consider the case in which the power and heat demands are unknown, and present a robust optimization-based approach for scheduling the turbine's heat and power generation, in which the demand is assumed to be inside an uncertainty set. We consider two different choices of the uncertainty set relying on the $\ell^\infty$- and the $\ell^1$-norms, each with different advantages, and consider the associated robust economic dispatch problems. We recast these as robust shortest-path problems on appropriately defined graphs. For the first choice, we provide an exact linear-time algorithm for the solution of the robust shortest-path problem, and for the second, we provide an exact quadratic-time algorithm and an approximate linear-time algorithm. The efficiency and usefulness of the algorithms are demonstrated using a detailed case study that employs real data on energy demand profiles and electricity tariffs.

math.OC↗

arXiv2021

Verifying Contracts for Perturbed Control Systems using Linear Programming

Verifying specifications for large-scale control systems is of utmost importance, but can be hard in practice as most formal verification methods can not handle high-dimensional dynamics. Contract theory has been proposed as a modular alternative to formal verification in which specifications are defined by assumptions on the inputs to a component and guarantees on its outputs. In this paper, we present linear-programming-based tools for verifying contracts for control systems. We first consider the problem of verifying contracts defined by time-invariant inequalities for unperturbed systems. We use $k$-induction to show that contract verification can be achieved by considering a collection of implications between inequalities, which are then recast as linear programs. We then move our attention to perturbed systems. We present a comparison-based framework, verifying that a perturbed system satisfies a contract by checking that the corresponding unperturbed system satisfies a robustified (and $ε$-approximated) contract. In both cases, we present explicit algorithms for contract verification, proving their correctness and analyzing their complexity. We also demonstrate the verification process for two case studies, one considering a two-vehicle autonomous driving scenario, and one considering formation control of a multi-agent system.

eess.SY↗

arXiv2021

A Characterization of All Passivizing Input-Output Transformations of a Passive-Short System

Passivity theory is one of the cornerstones of control theory, as it allows one to prove stability of a large-scale system while treating each component separately. In practice, many systems are not passive, and must be passivized in order to be included in the framework of passivity theory. Input-output transformations are the most general tool for passivizing systems, generalizing output-feedback and input-feedthrough. In this paper, we classify all possible input-output transformations that map a system with given shortage of passivity to a system with prescribed excess of passivity. We do so by using the connection between passivity theory and cones for SISO systems, and using the S-lemma for MIMO systems. We also present several possible applications of our results, including simultaneous passivation of multiple systems or with respect to multiple equilibria, as well as optimization problems such as $\mathcal{L}_2$-gain minimization. We also exhibit our results in a case study about synchronization in a network of non-passive faulty agents.

eess.SY↗

arXiv2021

Assume/Guarantee Contracts for Dynamical Systems: Theory and Computational Tools

Modern engineering systems include many components of different types and functions. Verifying that these systems satisfy given specifications can be an arduous task, as most formal verification methods are limited to systems of moderate size. Recently, contract theory has been proposed as a modular framework for defining specifications. In this paper, we present a contract theory for discrete-time dynamical control systems relying on assume/guarantee contracts, which prescribe assumptions on the input of the system and guarantees on the output. We then focus on contracts defined by linear constraints, and develop efficient computational tools for verification of satisfaction and refinement based on linear programming. We exemplify these tools in a simulation example, proving a certain safety specification for a two-vehicle autonomous driving setting.

eess.SY↗

arXiv2021

Model-Free Practical Cooperative Control for Diffusively Coupled Systems

In this paper, we develop a data-based controller design framework for diffusively coupled systems with guaranteed convergence to an $ε$-neighborhood of the desired formation. The controller is comprised of a fixed controller with an adjustable gain on each edge. Via passivity theory and network optimization we not only prove that there exists a gain attaining the desired formation control goal, but we present a data-based method to find an upper bound on this gain. Furthermore, by allowing for additional experiments, the conservatism of the upper bound can be reduced via iterative sampling schemes. The introduced scheme is based on the assumption of passive systems, which we relax by discussing different methods for estimating the systems' passivity shortage, as well as applying transformations passivizing them. Finally, we illustrate the developed model-free cooperative control scheme with a case study.

eess.SY↗

arXiv2021

Verifying Compositional Refinement of Assume/Guarantee Contracts using Linear Programming

Verifying specifications for large-scale modern engineering systems can be a time-consuming task, as most formal verification methods are limited to systems of modest size. Recently, contract-based design and verification has been proposed as a modular framework for specifications, and linear-programming-based techniques have been presented for verifying that a given system satisfies a given contract. In this paper, we extend this assume/guarantee framework by presenting necessary and sufficient conditions for a collection of contracts on individual components to refine a contract on the composed system. These conditions can be verified by solving linear programs, whose number grows linearly with the number of specifications defined by the contracts. We exemplify the tools developed using a case study considering safety in a car-following scenario, where noise and time-varying delay are considered.

eess.SY↗

arXiv2020

A Geometric Method for Passivation and Cooperative Control of Equilibrium-Independent Passivity-Short Systems

Equilibrium-independent passive-short (EIPS) systems are a class of systems that satisfy a passivity-like dissipation inequality with respect to any forced equilibria with non-positive passivity indices. This paper presents a geometric approach for finding a passivizing transformation for such systems, relying on their steady-state input-output relation and the notion of projective quadratic inequalities (PQIs). We show that PQIs arise naturally from passivity-shortage characteristics of an EIPS system, and the set of their solutions can be explicitly expressed. We leverage this connection to build an input-output mapping that transforms the steady-state input-output relation to a monotone relation, and show that the same mapping passivizes the EIPS system. We show that the proposed transformation can be implemented through a combination of feedback, feed-through, post- and pre-multiplication gains. Furthermore, we consider an application of the presented passivation scheme for the analysis of networks comprised of EIPS systems. Numerous examples are provided to illustrate the theoretical findings.

eess.SY↗

arXiv2020

On the Sample Complexity of Data-Driven Inference of the $\mathcal{L}_2$-gain

Lately, data-driven control has become a widespread area of research. A few recent big-data based approaches for data-driven control of nonlinear systems try to use classical input-output techniques to design controllers for systems for which only a finite number of (input-output) samples are known. These methods focus on using the given data to compute bounds on the $\mathcal{L}_2$-gain or on the shortage of passivity from finite input-output data, allowing for the application of the small gain theorem or the feedback theorem for passive systems. One question regarding these methods asks about their sample complexity, namely how many input-output samples are needed to get an approximation of the operator norm or of the shortage of passivity. We show that the number of samples needed to estimate the operator norm of a system is roughly the same as the number of samples required to approximate the system in the operator norm.

eess.SY↗

arXiv2019

Network Identification for Diffusively-Coupled Systems with Minimal Time Complexity

The theory of network identification, namely identifying the (weighted) interaction topology among a known number of agents, has been widely developed for linear agents. However, the theory for nonlinear agents using probing inputs is far less developed, relying on dynamics linearization, and thus cannot be applied to networks with non-smooth or discontinuous dynamics. We use global convergence properties of the network, which can be assured using passivity theory, to present a network identification method for nonlinear agents. We do so by linearizing the steady-state equations rather than the dynamics, achieving a sub-cubic time algorithm for network identification. We also study the problem of network identification from a complexity theory standpoint, showing that the presented algorithms are optimal in terms of time complexity. We demonstrate the presented algorithm in two case studies with discontinuous dynamics.

eess.SY↗

arXiv2019

Network Feedback Passivation of Passivity-Short Multi-Agent Systems

In this paper, we propose a network-optimization framework for the analysis of multi-agent systems with passive-short agents. We consider the known connection between diffusively-coupled maximally equilibrium-independent passive systems, and network optimization, culminating in a pair of dual convex network optimization problems, whose minimizers are exactly the steady-states of the closed-loop system. We propose a network-based regularization term to the network optimization problem and show that it results in a network-based feedback using only relative outputs. We prove that if the average of the passivity indices is positive, then we convexify the problem, passivize the agents, and that steady-states of the augmented system correspond to the minimizers of the regularized network optimization problem. We also suggest a hybrid approach, in which only a subset of agents sense their own output, and show that if the set is nonempty, then we can always achieve the same correspondence as above, regardless of the passivity indices. We demonstrate our results on a traffic model with non-passive agents and limited GNSS reception.

eess.SY↗

arXiv2019

Symmetry-Induced Clustering in Multi-Agent Systems using Network Optimization and Passivity

This work studies the effects of a weak notion of symmetry on diffusively-coupled multi-agent systems. We focus on networks comprised of agents and controllers which are maximally equilibrium independent passive, and show that these converge to a clustered steady-state, with clusters corresponding to certain symmetries of the system. Namely, clusters are computed using the notion of the exchangeability graph. We then discuss homogeneous networks and the cluster synthesis problem, namely finding a graph and homogeneous controllers forcing the agents to cluster at prescribed values.

eess.SY↗

arXiv2018

Network Identification: A Passivity and Network Optimization Approach

The theory of network identification, namely identifying the interaction topology among a known number of agents, has been widely developed for linear agents over recent years. However, the theory for nonlinear agents remains less extensive. We use the notion maximal equilibrium-independent passivity (MEIP) and network optimization theory to present a network identification method for nonlinear agents.We do so by introducing a specially designed exogenous input, and exploiting the properties of networked MEIP systems. We then specialize on LTI agents, showing that the method gives a distributed cubic-time algorithm for network reconstruction in that case. We also discuss different methods of choosing the exogenous input, and provide an example on a neural network model.

math.OC↗

arXiv2018

Analysis and Synthesis of MIMO Multi-Agent Systems Using Network Optimization

This work studies analysis and synthesis problems for diffusively coupled multi-agent systems. We focus on networks comprised of multi-input multi-output nonlinear systems that posses a property we term maximal equilibrium-independent cyclically monotonone passivity (MEICMP), which is an extension of recent passivity results. We demonstrate that networks comprised of MEICMP systems are related to a pair of dual network optimization problems. In particular, we show that the steady-state behavior of the multi-agent system correspond to the minimizers of appropriately defined network optimization problems. Exploiting this connection between the dynamic networked system and static optimization problems, we propose a synthesis procedure for designing the coupling controllers in the network to achieve a desired output state for the network. We provide detailed examples of dynamical networked systems satisfying these properties and demonstrate the results for a network of damped planar oscillators.

math.OC↗

arXiv2017

On Certain Properties of Convex Functions

This note deals with certain properties of convex functions. We provide results on the convexity of the set of minima of these functions, the behaviour of their subgradient set under restriction, and optimization of these functions over an affine subspace.

math.OC↗