New results
A Modular Structural Analysis of DAE Systems
In 29, a new modular structural analysis algorithm has been proposed that takes full advantage of the object tree structure of a DAE model. The bedrock of this method is a novel concept of structural analysis-aware interface for components. The essence of a component interface is to capture the necessary information about a Modelica class that needs to be exposed, in order to perform the structural analysis of a component comprising instances of the former class, while hiding away useless information regarding the equations and all protected features it may contain.
In order to compute a component interface, one has to be able to perform the structural analysis of the possibly non-square DAE system that this component encapsulates, and to use the interfaces of the components it aggregates in this analysis. We base our algorithm on Pryce’s
Putting all of this together, it is then possible to perform a modular structural analysis, in which structural analysis is performed at the class level, and the results can then be instantiated for each component of the system model, knowing its context. Hence, structural information at the system level is derived from composing the result of component-level analysis. Modular structural analysis yields huge gains in terms of memory usage and computational costs, as the analysis of a single large-scale DAE is replaced with that of multiple smaller subsystems. Moreover, the analysis is performed at the class level, meaning that a single structural analysis is needed for all system components that are instances of the same class.
In 2024, the modular structural analysis algorihtm has been fully implemented (see Section 7.1.2) and tested against several scalability benchmarks from the literature 45, 78. This experimental work confirms that the algorithm has an empirical complexity that is logarithmic in the size of the model, provided the model has a low tree-width, as it is often the case for energy network infrastructures.
Fault Diagnosability Analysis of Multi-Mode Systems
This work has been conducted in collaboration with the University of Linköping (Sweden) on the topic of system diagnosis, based on multimode DAE systems.
Fault detection and diagnosis are important for the health monitoring of physical systems. Model-based approaches for single-mode, smooth, systems are a well-established field, supported by a large body of literature covering various approaches like structural methods 35, parity space techniques, and observer-based methods 66.
While single-mode systems are often described using differential algebraic equations (DAEs), the modeling of non-smooth physical systems yields switched DAEs, also known as multimode DAEs (mDAEs), which combine continuous behaviors, defined as solutions of a set of DAE systems, with discrete mode changes 89, 28. Direct application of traditional fault diagnosis methods to all possible configurations of multi-mode systems quickly becomes intractable, as the number of modes tends to be exponential in the size of the system. The method proposed by 69 works around this issue by coupling a mode estimation algorithm with a single-mode diagnosis methodology, akin to just-in-time compilation in computer science. This approach unfortunately puts the burden on solving mode estimation problems, which often turn out to be intractable for the same reason.
Structural fault detectability and isolability are a graph-based method to evaluate diagnosability properties on DAEs 62. It is based on the Dulmage-Mendelsohn decomposition (DM), a building block of the structural analysis of equation systems. In 11, we show how its extension to multimode systems, introduced in 4, can be applied in the context of structural fault detectability and isolability of mmDAEs 64. Building upon our previous research studies, the methods presented in this paper represent advancements in diagnostic methodologies for multi-mode systems, providing novel ways to study the diagnosability of multi-mode systems without enumerating their modes.
The case study used throughout this article is a model of a reconfigurable battery system, in which switching strategies enable to produce an AC output without relying on a central inverter 22. This model is parameterized by the number of battery cells, so that both the inherent complexity associated with the diagnostics of such systems and the scalability of our approaches can be addressed.
Automated Reasoning For The Existence Of Darboux Polynomials
Darboux polynomials are particular algebraic invariants that play an important role in the integrability theory of ordinary differential equations (ODEs). Computation of Darboux polynomials is a central problem in the Prelle-Singer procedure for computing elementary first integrals of planar systems of polynomial ODEs [12], which yields a systematic method for computing elementary closed-form solutions (whenever these exist) to an important class of ordinary differential equations. Owing to this important application, algorithms for generating Darboux polynomials have received considerable attention in computer algebra. More recently, Darboux polynomials have found application in the area of formal safety verification of cyber-physical systems, where the problem of their automatic generation is encountered in the broader context of searching for invariant (and positively invariant) sets.
Darboux generation algorithms are semi-decision procedures enumerating all Darboux polynomials up to a certain fixed bound on the total degree. The bound is eventually increased until finding a (not necessarily irreducible) Darboux polynomial or reaching memory and/or time limits. Theoretically, the existence of a bound on the total degree of irreducible Darboux polynomials is, as of today, an open problem when
Given a polynomial ordinary differential equation (ODE), we devise generic polynomial reduction algorithms to automatically investigate the intertwined relationship between the total degree of (nontrivial) Darboux polynomials and the polynomials defining the ODE. By generic we mean that both the coefficients and the multidegree of the involved polynomials are symbolic. We use Newton polytopes as a light-weight abstraction to select optimal weight monomial orders improving the efficiency of the involved computations. The method works by inferring necessary conditions on both the coefficients and the multidegree for the polynomial to be Darboux. These conditions are then used, via constants’ propagation, to restrict the shape of the generic candidate, pinpointing which monomials ought to be preserved by removing the superfluous ones. In some relevant cases, we are able to automatically prove the nonexistence of (nontrivial) Darboux polynomials providing a new toolbox to prove and formally certify that some limit cycles are not algebraic. 10
Solution concepts for linear piecewise affine or switched differential-algebraic equations
The standard approach for dealing with (continuous) differential-algebraic equations (DAEs) is to solve the algebraic constraints—either manually or with the aid of computer algebra systems—in terms of a subset of the variables. These solutions are then substituted into the remaining differential equations, which results in a lower-dimensional ordinary differential equation (ODE). However, this approach does not account for the response to inconsistent initial conditions. Additionally, the presence of discontinuities complicates the global solution of the algebraic constraints, as different constraints may be active in different regions of the state-space. This leads to locally defined ODEs with different sets of variables, creating ambiguity in how solutions should be “glued” together when their variables differ. As a result, there is currently no theoretical foundation for studying discontinuous DAEs. Without such a foundation, subsequent studies—such as numerical simulations, stability analyses, and controller designs—lack a sound justification.
As a starting point for investigating discontinuous DAEs, we focus on linear piecewise affine systems (PWA-DAEs), described by
Pacti: Assume-Guarantee Contracts for Efficient Compositional Analysis and Design
Contract-based design is a method to facilitate modular design of systems. While there has been substantial progress in the theory of contracts, there has been less progress on practical algorithms for the algebraic operations in the theory. In this paper, we present (1) principles to implement a contract-based design tool at scale and (2) Pacti, a tool that can efficiently compute these operations. We illustrate the use of Pacti in a variety of case studies. 8