FEANICSES 2022 Workshop

This talk presents my recent research on analysis, design, and model reduction of consensus networked dynamical systems.

Many natural and engineered systems operate over protocols or dynamics over networks. The consensus algorithm is a famous distributed information-sharing protocol over a network, used in many applications ranging from wind farm optimization, robotics and autonomous spacecraft, sensor networks and compressed sensing, and multi-agent systems. It is therefore important to understand how the structure of the network affects control-theoretic properties of the collective system, e.g., robustness measures, which allows one to design better, e.g., more robust, consensus networks.

The study of networked dynamical systems typically involves dealing with high-dimensional models that grow in size and complexity with increasing number of agents. Thus, it is desirable to find lower-order approximant network models that exhibit similar input-output behavior. Traditional model reduction approaches for centralized systems need to be adapted to ensure the preservation of the structure of networked systems.

In the first part of the talk, I look at the H∞-performance problem of the edge agreement protocol for networks of single-integrator agents operating on independent time scales, connected by weighted edges, and corrupted by exogenous disturbances. The H∞-norm relates to how finite-energy disturbances cause the system to deviate from consensus, and has found use in combating time delays in consensus problems as well as in distributed state estimation over sensor networks. The edge agreement protocol, or edge consensus, is a minimal representation of consensus when only relative measurements across edges in the network are available to the agents. I give H∞-norm expressions and bounds that can be used to derive new insights on the network’s performance in terms of the effect of time scales and edge weights on disturbance rejection. Finally, I show how to use the proposed bounds to formulate a convex optimization problem for network design via time scale and edge weight selection. The interest in analyzing networks that contain non-homogeneous agents operating on different time scales stems from examples and applications such as coupled oscillators, neuronal networks, social networks, and epidemic networks.

In the second part of the talk, I discuss model reduction approaches for consensus network systems based on a given clustering of the underlying graph. Typical reduction approaches for networked dynamical systems focus on optimizing the clustering to be used for constructing the reduced order system. Then, after the optimal clustering is found, the reduced network system is constructed via projection using the corresponding clustering characteristic matrix. Here, I consider a given graph clustering for a consensus network system and construct a parameterized reduced consensus network system, where the parameters to be optimized are the edge weights and nodal time-scales. Both H∞- and H2-approaches are discussed to select the reduced network parameters such that the corresponding approximation errors are minimized. Unlike the network design problems in the first part, the model reduction problems are nonlinear, which requires separately optimizing the nodal time scales while fixing the edge weights or vice versa and the use of an iterative method for handling bilinear matrix inequality constraints.

joint work with Arvind Adimoolam

Networked control systems (NCS) are widely used in real world applications because of their advantages, such as remote operability and reduced installation costs. However, they are prone to various inaccuracies in execution like delays, packet dropouts, inaccurate sensing and quantization errors. To ensure safety of NCS, their models have to be verified under the consideration of aforementioned uncertainties. In this work, we tackle the problem of verifying safety of models of NCS under uncertain sampling time, inaccurate output measurement or estimation, and unknown disturbance input. Unbounded-time safety verification requires approximation of reachable sets by invariants, whose computation involves set operations. We extend zonotopes to the complex valued domain by a representation called complex zonotope, which can capture contraction along complex eigenvectors for determining invariants. We demonstrate the efficiency of our algorithm on benchmark examples.

We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek's higher-dimensional automata and Alur and Dill's timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.

The interest of our formalism is in modeling and analysing systems which exhibit both real-time behavior and concurrency. Most existing formalisms for real-time modeling identify concurrency and interleaving, which is problematic (as we shall argue). When abstaining from doing so, one is forced to abandon the notion, almost universal in real-time formalisms, that switches are immediate; fortunately (and surprisingly) we are able to show that this does not cause too much trouble.

Formal verification is widely used to perform safety analysis. The quality of the result depends on the expressiveness of the verified properties, which is known to be time consuming. A trade of between efficiency and precision should be found. For that, we propose methods to accelerate convergence in the case of static analysis by abstract interpretation. These methods are based on statistical and convex analysis methods.

In the VV4RTOS activity, GMV in Portugal is joined by Thales Alenia Space (TAS) in France, the french Ecole Nationale de l'Aviation Civile (ENAC), and the Systems Control and Optimization Laboratory (SYSCOP) from the Institut für Mikrosystemtechnik (IMTEK) in Germany, to develop and validate a framework for the verification & validation of spacecraft GNC systems based on embedded optimisation, tailored to handle different layers of abstraction, from G&C requirements down to hardware level. This is grounded on the parallel design and development of real-time optimisation-based G&C software, allowing to concurrently identity, develop, consolidate, and validate a set of engineering practices and analysis & verification tools to ensure safe code execution of the designed G&C software as test cases but aimed at streamlining general industrial V&V processes.

In this talk, we present the objectives of the project, the technical approach being followed, as well as the ongoing developments of the consortium.

Aerodynamic effects can become dangerous when a drone follows a path at high speed, even in the absence of wind. We propose a method to compute a safe set that must contain the state and the reference to follow at all times. This set allows designing a reference governor control to make the drone follow its trajectory while respecting a set of constraints that includes polynomial constraints when aerodynamic effects are modeled.

Polynomial positivity over the real field is known to be decidable but even the best algorithms remain costly. An incomplete but often efficient alternative consists in looking for positivity witnesses as sum of squares decompositions. Such decompositions can in practice be obtained through convex optimization. Unfortunately, these methods only yield approximate solutions. Hence the need for formal verification of such witnesses. State of the art methods rely on heuristic roundings to exact solutions in the rational field. These solutions are then easy to verify in a proof assistant. However, this verification often turns out to be very costly, as rational coefficients may blow up during computations.

Nevertheless, overapproximations with floating-point arithmetic can be enough to obtain proofs at a much lower cost. Such overapproximations being non trivial, it is mandatory to formally prove that rounding errors are correctly taken into account. We develop a reflexive tactic for the Coq proof assistant allowing one to automatically discharge polynomial positivity proofs. The tactic relies on heavy computation involving multivariate polynomials, matrices and floating-point arithmetic. Benchmarks indicate that we are able to formally address positivity problems that would otherwise be untractable with other state of the art methods.

In this talk, we present FRET and CoCoSim, two NASA Ames open-source projects revolving around requirements authoring, analysis and formal verification. FRET provides a user-friendly framework for the creation of requirements with unambiguous semantics, through the power of it structured natural language. Additional features include the ability to manage, simulate and analyze requirements, as well as connect with external analysis tools, such as CoCoSim. CoCoSim is a MATLAB plugin for compositional verification of Simulink and Stateflow models, using the Assume-Guarantee paradigm. Its compilation scheme translates Simulink/Stateflow code into Lustre, enabling features such code and test-case generation using LustreC.

In this talk we will present the a summary of the current effort within the FEANICSES project: the results, methods and tools on the verification of regular dynamical systems and the extension to Neural Networks and Optimization-based guidance.

at 8pm, Au bon manger, next to ENSEEIHT, on Canal du Midi

At 8pm, le Cri de la Truffe, next to Esquirol.