Cyber-physical systems (CPS) research continues to advance the integration of computation, communication, and control into safety-critical and large-scale infrastructures. The ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), held as part of CPS-IoT Week, has long been a premier venue for disseminating these advances and fostering interdisciplinary dialogue. This special issue contains a selection of original papers, which extend earlier results presented at the 15th ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS) that took place in Hong Kong from May 13–16, 2024, as part of CPS-IoT Week 2024. They cover different aspects of CPS research, reflecting both methodological rigor and practical impact.

Customizing autonomous vehicles to align with user preferences while ensuring safety may significantly impact their adoption. Collecting user preference data by asking a large number of comparison questions can be demanding. In this work, we use active learning along with temporal logic descriptions of constraints to enable safe learning of preferences with a reduced number of questions. We take a Bayesian inference approach combined with Weighted Signal Temporal Logic (WSTL), resulting in a WSTL formula that can rank signals based on user preferences and be used for correct-and-custom-by-construction control synthesis. Our method is practical for formulas and signals with various complexity since we compute STL-related values offline. We provide an upper bound for the number of answers in disagreement with user answers. We demonstrate the performance of our method both on synthetic data and by human subject experiments in an immersive driving simulator. We consider two driving scenarios, one involving a vehicle approaching a pedestrian crossing and the other with an overtake maneuver. Our results over synthetic experiments with ground truth weight valuation show that our query selection algorithm converges faster than random query selection. Human subject study results show an average agreement of 94% with user answers during training, and 79% during validation (which increases to 86% when restricted to high confidence results).

In this work, we propose a safety-guaranteed personalization for autonomous vehicles by incorporating Signal Temporal Logic (STL) into preference learning problem. We propose a new variant of STL called Parametric Weighted Signal Temporal Logic with a new quantitative semantics, namely weighted robustness. Given a set of pairwise preferences, and by using gradient-based optimization methods, we learn a set of valuations for weights that reflect preferences such that preferred ones have greater weighted robustness value than their non-preferred matches. Traditional STL formulas fail to incorporate preferences due its complex nature. Our initial results with data from a human-subject on an intersection with stop sign driving scenario, in which the participant is asked their preferred driving behavior from pairs of vehicle trajectories, indicate that we can learn a new weighted STL formula that captures preferences while also encoding correctness.

Stable human movement is often defined as movement that does not lead to falling. The set of such movements is too broad to be encompassed by traditional notions of stability in control theory, such as stability about equilibria or trajectories. We propose framing the region of stable human movement, which we call the stabilizable region, as the backward reachable set of a controlled invariant set. We focus on sit-to-stand, which requires a high level of coordination and is a common setting for falls. Using tools from the hybrid systems community, we compute the stabilizable region for sit-to-stand under varying environmental and physiological conditions. We validate our results with a dataset of humans performing perturbed sit-to-stand.

This paper addresses the problem of controlling an unknown dynamical system to safely reach a target set. We assume we have a priori access to a finite set of uncertain linear systems, to which the unknown system belongs to. This set can contain models for different failure or operational modes or potential environmental conditions. Given a desired exploration-exploitation profile, we provide a bilinear optimization based solution to this control synthesis problem. Our approach provides a family of controllers that enable adaptation based on data observed at run-time to automatically trade off model detection and reachability objectives while maintaining safety. We demonstrate the approach with several examples.

Backward reachability analysis is essential to synthesizing controllers that ensure the correctness of closed-loop systems. This article is concerned with developing scalable algorithms that underapproximate the backward reachable sets, for discrete-time uncertain linear and nonlinear systems. Our algorithm sequentially linearizes the dynamics and uses constrained zonotopes for set representation and computation. The main technical ingredient of our algorithm is an efficient way to underapproximate the Minkowski difference between a constrained zonotopic minuend and a zonotopic subtrahend, which consists of all possible values of the uncertainties and the linearization error. This Minkowski difference needs to be represented as a constrained zonotope to enable subsequent computation, but, as we show, it is impossible to find a polynomial-size representation for it in polynomial time. Our algorithm finds a polynomial-size underapproximation in polynomial time. We further analyze the conservatism of this underapproximation technique and show that it is exact under some conditions. Based on the developed Minkowski difference technique, we detail two backward reachable set computation algorithms to control the linearization error and incorporate nonconvex state constraints. Several examples illustrate the effectiveness of our algorithms.

In this paper, we present a compositional condition for ensuring safety of a collection of interacting systems modeled by inter-triggering hybrid automata (ITHA). ITHA is a modeling formalism for representing multi-agent systems in which each agent is governed by individual dynamics but can also interact with other agents through triggering actions. These triggering actions result in a jump/reset in the state of other agents according to a global resolution function. A sufficient condition for safety of the collection, inspired by responsibility-sensitive safety, is developed in two parts: self-safety relating to the individual dynamics, and responsibility relating to the triggering actions. The condition relies on having an over-approximation method for the resolution function. We further show how such over-approximations can be obtained and improved via communication. We use two examples, a job scheduling task on parallel processors and a highway driving example, throughout the paper to illustrate the concepts. Finally, we provide a comprehensive evaluation on how the proposed condition can be leveraged for several multi-agent control and supervision examples.

In this paper, we study feedback dynamical systems with memoryless controllers under imperfect information. We develop an algorithm that searches for “adversarial scenarios”, which can be thought of as the strategy for the adversary representing the noise and disturbances, that lead to safety violations. The main challenge is to analyze the closed-loop system's vulnerabilities with a potentially complex or even unknown controller in the loop. As opposed to commonly adopted approaches that treat the system under test as a black-box, we propose a synthesis-guided approach, which leverages the knowledge of a plant model at hand. This hence leads to a way to deal with gray-box systems (i.e., with known plant and unknown controller). Our approach reveals the role of the imperfect information in the violation. Examples show that our approach can find non-trivial scenarios that are difficult to expose by random simulations. This approach is further extended to incorporate model mismatch and to falsify vision-in-the-loop systems against finite-time reach-avoid specifications.

We consider abstraction-based design of output-feedback controllers for dynamical systems with a finite set of inputs and outputs against specifications in linear-time temporal logic. The usual procedure for abstraction-based controller design (ABCD) first constructs a finite-state abstraction of the underlying dynamical system, and second, uses reactive synthesis techniques to compute an abstract state-feedback controller on the abstraction. In this context, our contribution is two-fold: (I) we define a suitable relation between the original system and its abstraction which characterizes the soundness and completeness conditions for an abstract state-feedback controller to be refined to a concrete output-feedback controller for the original system, and (II) we provide an algorithm to compute a sound finite-state abstraction fulfilling this relation.

This paper introduces inter-triggering hybrid automata, a formalism to represent multi-agent systems where each agent is represented as a hybrid automaton and agents interact by triggering discrete transitions (jumps and resets) on their "neighboring" agents. Using this formalism, we define responsibility-sensitive safety as respecting one another's invariances while triggering jumps and resets. This allows us to make a formal connection between responsibility and robust controlled invariant sets for individual agents, therefore leading to a compositional verification framework for the safety of the overall multi-agent system. We discuss several advantages of this viewpoint and illustrate it on a highway driving example.

In many multirobot applications, planning trajectories in a way to guarantee that the collective behavior of the robots satisfies a certain high-level specification is crucial. Motivated by this problem, we introduce counting temporal logics-formal languages that enable concise expression of multirobot task specifications over possibly infinite horizons in this article. We first introduce a general logic called counting linear temporal logic plus (cLTL+), and propose an optimization-based method that generates individual trajectories such that satisfaction of a given cLTL+ formula is guaranteed when these trajectories are synchronously executed. We then introduce a fragment of cLTL+, called counting linear temporal logic (cLTL), and show that a solution to a planning problem with cLTL constraints can be obtained more efficiently if all robots have identical dynamics. In the second part of this article, we relax the synchrony assumption and discuss how to generate trajectories that can be asynchronously executed, while preserving the satisfaction of the desired cLTL+ specification. In particular, we show that when the asynchrony between robots is bounded, the method presented in this article can be modified to generate robust trajectories. We demonstrate these ideas with an experiment and provide numerical results that showcase the scalability of the method.

In this work we consider control problems for discrete-time dynamical systems with safety constraints. As opposed to the existing work on similar problems, we assume that the system at run-time can preview some of the future uncontrolled inputs (e.g., disturbances). In order to develop a control synthesis technique that can leverage such preview information, we introduce a mathematical construct called Preview Automaton that incorporates system dynamics with the prior knowledge on the structure of the preview. We propose an algorithm to find the maximum controlled invariant set for the Preview Automaton. Although Preview Automaton can be equivalently represented by a Finite Transition System, for which existing control synthesis methods can be applied, we show that exploiting the structure of the Preview Automaton results in more efficient solution algorithms. These ideas are demonstrated with a lane-keeping problem, where we show that existence of the preview information allows the vehicle to safely navigate roads with larger curvature, whereas the problem becomes infeasible when no preview information is available.

When deployed into real environments, control systems need to be able to operate when their sensor data can become 'missing' (e.g., a vehicle's radar system may incorrectly detect a falling leaf as a vehicle on the road, or a distributed control system may lose sensor data packets while attempting to transmit). Guaranteeing safety of such systems can be handled by enforcing boundedness of the state or the estimated state of a system during operation. The form of boundedness that we use within this work is called equalized recovery and the goal of this work is to find controllers or estimators that satisfy equalized recovery in the presence of missing data. Equalized recovery relaxes the notion of invariance and allows the system states to be in a larger set during missing data events as long as the states can be steered back to the original set. Prefix-based controllers and estimators are introduced to solve this problem and methods to synthesize them are presented.

In this work, we consider detectability analysis for faults in systems governed by switched affine dynamics. By a fault, we mean a sudden and permanent change in the system dynamics. Given the model of the healthy system, such a fault can be detected via a model invalidation approach, i.e., by collecting historic observations over a finite horizon and checking whether these observations can be generated by the healthy system model. Whenever the faulty system model is also available, it is possible to find T, the minimum length of the horizon, with which the fault is guaranteed to be detected eventually (with a T-delay at most). The main contribution of this work is to show the possibility of reducing the value of T, by augmenting the fault detectability analysis with additional linear temporal logic (LTL) constraints on the switching signals, if any. We express the LTL constraints (restricted in a finite horizon) with a nondeterministic finite automaton (NFA), which is then transformed into a set of mixed integer linear constraints that can be easily integrated in the detectability analysis.

This paper employs correct-by-construction control synthesis, in particular controlled invariant set computations, for falsification. Our hypothesis is that if it is possible to compute a “large enough” controlled invariant set either for the actual system model or some simplification of the system model, interesting corner cases for other control designs can be generated by sampling initial conditions from the boundary of this controlled invariant set. Moreover, if falsifying trajectories for a given control design can be found through such sampling, then the controlled invariant set can be used as a supervisor to ensure safe operation of the control design under consideration. In addition to interesting initial conditions, which are mostly related to safety violations in transients, we use solutions from a dual game, a reachability game for the safety specification, to find falsifying inputs. We also propose optimization-based heuristics for input generation for cases when the state is outside the winning set of the dual game. To demonstrate the proposed ideas, we consider case studies from basic autonomous driving functionality, in particular, adaptive cruise control and lane keeping. We show how the proposed technique can be used to find interesting falsifying trajectories for classical control designs like proportional controllers, proportional integral controllers and model predictive controllers, as well as an open source real-world autonomous driving package.

Modern control synthesis methods that are capable of delivering safety guarantees typically rely on finding invariant sets. Computing and/or representing such sets becomes intractable for high-dimensional systems and often constitutes the main bottleneck of computational procedures. In this paper we instead analytically study a particular high-dimensional system and propose a control strategy that we prove renders a set invariant whenever it is possible to do so. The control problem---the mode-counting problem with two modes in one dimension---is inspired by scheduling of thermostatically controlled loads (TCLs) and exhibits a trade-off between local safety constraints and a global counting constraint. We improve upon a control strategy from the literature to handle heterogeneity and derive sufficient conditions for the strategy to solve the problem at hand. In addition, we show that the conditions are also necessary for the problem to have a solution, which implies a type of optimality of the proposed control strategy. We outline more general problem instances where the same control strategy can be implemented and we give sufficient (but not necessary) conditions for the closed-loop system to satisfy its specification. We illustrate our results on a TCL scheduling example.

Given a large homogeneous collection of switched systems, we consider a novel class of safety constraints, called mode-counting constraints, that impose restrictions on the number of systems that are in a particular mode. We propose an approach for synthesizing correct-by-construction switching protocols to enforce such constraints over time. Our approach starts by constructing an approximately bisimilar abstraction of the individual system model. Then, we show that the aggregate behavior of the collection can be represented by a linear system, whose system matrices are induced by the transition graph of the abstraction. Finally, the control synthesis problem with mode-counting constraints is reduced to a cycle assignment problem on the transition graph. One salient feature of the proposed approach is its scalability; the computational complexity is independent of the number of systems involved. We illustrate this approach on the problem of coordinating a large collection of thermostatically controlled loads while ensuring a bound on the number of loads that are extracting power from the electricity grid at any given time.

Abstraction-based, hierarchical approaches to control synthesis from temporal logic specifications for dynamical systems have gained increased popularity over the last decade. Yet various issues commonly encountered and extensively dealt with in control systems have not been adequately discussed in the context of temporal logic control of dynamical systems, such as inter-sample behaviors of a sampled-data system, effects of imperfect state measurements and un-modeled dynamics, and the use of time-discretized models to design controllers for continuous-time dynamical systems. We discuss these issues in this paper. The main motivation is to demonstrate the possibility of accounting for the mismatches between a continuous-time control system and its various types of abstract models used for control synthesis. We do this by incorporating additional robustness measures in the abstract models. Such robustness measures are gained at the price of either increased non-determinism in the abstracted models or relaxed versions of the specification being realized. Under a unified notion of abstraction, we provide concrete means of incorporating these robustness measures and establish results that demonstrate their effectiveness in dealing with the above mentioned issues.

Modern aircraft increasingly rely on electric power for subsystems that have traditionally run on mechanical power. The complexity and safety-criticality of aircraft electric power systems have therefore increased, rendering the design of these systems more challenging. This work is motivated by the potential that correct-by-construction reactive controller synthesis tools may have in increasing the effectiveness of the electric power system design cycle. In particular, we have built an experimental hardware platform that captures some key elements of aircraft electric power systems within a simplified setting. We intend to use this platform for validating the applicability of theoretical advances in correct-by-construction control synthesis and for studying implementation-related challenges. We demonstrate a simple design workflow from formal specifications to auto-generated code that can run on software models and be used in hardware implementation. We show some preliminary results with different control architectures on the developed hardware testbed.

We investigate the robustness of reactive control protocols synthesized to guarantee system's correctness with respect to given temporal logic specifications. We consider uncertainties in open finite transition systems due to unmodeled transitions. The resulting robust synthesis problem is formulated as a temporal logic game. In particular, if the specification is in the so-called generalized reactivity [1] fragment of linear temporal logic, so is the augmented specification in the resulting robust synthesis problem. Hence, the robust synthesis problem belongs to the same complexity class with the nominal synthesis problem, and is amenable to polynomial time solvers. Additionally, we discuss reasoning about the effects of different levels of uncertainties on robust synthesizability and demonstrate the results on a simple robot motion planning scenario.

This paper describes TuLiP, a Python-based software toolbox for the synthesis of embedded control software that is provably correct with respect to an expressive subset of linear temporal logic (LTL) specifications. TuLiP combines routines for (1) finite state abstraction of control systems, (2) digital design synthesis from LTL specifications, and (3) receding horizon planning. The underlying digital design synthesis routine treats the environment as adversary; hence, the resulting controller is guaranteed to be correct for any admissible environment profile. TuLiP applies the receding horizon framework, allowing the synthesis problem to be broken into a set of smaller problems, and consequently alleviating the computational complexity of the synthesis procedure, while preserving the correctness guarantee.

This paper addresses the problem of segmenting a combination of linear subspaces and quadratic surfaces from sample data points corrupted by (not necessarily small) noise. Our main result shows that this problem can be reduced to minimizing the rank of a matrix whose entries are affine in the optimization variables, subject to a convex constraint imposing that these variables are the moments of an (unknown) probability distribution function with finite support. Exploiting the linear matrix inequality based characterization of the moments problem and appealing to well known convex relaxations of rank leads to an overall semi-definite optimization problem. We apply our method to problems such as simultaneous 2D motion segmentation and motion segmentation from two perspective views and illustrate that our formulation substantially reduces the noise sensitivity of existing approaches.

In this paper we propose a supervised 3D segmentation algorithm to locate the esophagus in thoracic CT scans using a variational framework. To address challenges due to low contrast, several priors are learned from a training set of segmented images. Our algorithm first estimates the centerline based on a spatial model learned at a few manually marked anatomical reference points. Then an implicit shape model is learned by subtracting the centerline and applying PCA to these shapes. To allow local variations in the shapes, we propose to use nonlinear smooth local deformations. Finally, the esophageal wall is located within a 3D level set framework by optimizing a cost function including terms for appearance, the shape model, smoothness constraints and an air/contrast model.

This paper presents a general method for segmenting a vector valued sequence into an unknown number of subsequences where all data points from a subsequence can be represented with the same affine parametric model. The idea is to cluster the data into the minimum number of such subsequences which, as we show, can be cast as a sparse signal recovery problem by exploiting the temporal correlation between consecutive data points. We try to maximize the sparsity (i.e. the number of zero elements) of the first order differences of the sequence of parameter vectors. Each non-zero element in the first order difference sequence corresponds to a change. A weighted l1norm based convex approximation is adopted to solve the change detection problem. We apply the proposed method to video segmentation and temporal segmentation of dynamic textures.