The research conducted in conjunction with this award provides new insights into the mechanisms behind cardiac defibrillation, demonstrating that a dynamically expanding electrical wavefront originating at the heart's surface plays a critical role in disrupting fibrillatory scroll waves. Our findings suggest that heart size, specifically the surface-to-volume ratio, may significantly impact defibrillation efficacy, offering potential for more targeted and effective treatment strategies for ventricular fibrillation, with broader implications for improving defibrillation techniques and outcomes in clinical settings.

We also conducted innovative research on resilient CPS.  Resiliency is the ability to quickly recover from a violation and avoid future violations for as long as possible. Such a property is of fundamental importance for Cyber-Physical Systems (CPS), and yet, until now, there is no widely agreed-upon formal treatment of CPS resiliency. We present an STL-based framework for reasoning about resiliency in CPS in which resiliency has a syntactic characterization in the form of an STL-based Resiliency Specification (SRS). Given an arbitrary STL formula φ,time bounds α and β, the SRS of φ, R_α,β(φ),is the STL formula ~φ U_[0,α] G_[0,β) φ, specifying that recovery from a violation of φ occur within time α (recoverability), and subsequently that φ be maintained for duration β (durability). These R-expressions, which are atoms in our SRS logic, can be combined using STL operators, allowing one to express composite resiliency specifications, e.g., multiple SRSs must hold simultaneously, or the system must eventually be resilient.

We define a quantitative semantics for SRSs in the form of a Resilience Satisfaction Value (ReSV) function r and prove its soundness and completeness w.r.t. STL's Boolean semantics. The r-value for R_α,β(φ) atoms is a singleton set containing a pair quantifying recoverability and durability. The r-value for a composite SRS formula results in a set of non-dominated recoverability-durability pairs, given that the ReSVs of subformulas might not be directly comparable (e.g., one subformula has superior durability but worse recoverability than another). To the best of our knowledge, this is the first multi-dimensional quantitative semantics for an STL-based logic. Two case studies demonstrate the practical utility of our approach.

Another key result of the project is the introduction of the concept of Spatial Predictive Control (SPC) to solve the following problem: given a collection of agents (e.g., drones) with positional low-level controllers (LLCs) and a mission-specific distributed cost function, how can a distributed controller achieve and maintain cost-function minimization without a plant model and only positional observations of the environment?  Our fully distributed SPC controller is based strictly on the position of the agent itself and on those of its neighboring agents. This information is used in every time-step to compute the gradient of the cost function and to perform a spatial look-ahead to predict the best next target position for the LLC.  Using a high-fidelity simulation environment, we show that SPC outperforms the most closely related class of controllers, Potential Field Controllers, on the drone flocking problem. We also show that SPC is able to cope with a potential sim-to-real transfer gap by demonstrating its performance on real hardware, namely our implementation of flocking using nine Crazyflie 2.1 drones.

Last Modified: 12/08/2024
Modified by: Scott A Smolka