An official website of the United States government
Multi-agent systems (MASs) consisting of a number of autonomous agents that communicate, coordinate, and jointly sense the environment to achieve complex missions can be found in a variety of applications such as robotics, smart cities, and internet-of-things applications. Modeling and monitoring MAS requirements to guarantee overall mission objectives, safety, and reliability is an important problem. Such requirements implicitly require reasoning about diverse sensing and communication modalities between agents, analysis of the dependencies between agent tasks, and the spatial or virtual distance between agents. To capture such rich MAS requirements, we model agent interactions via multiple directed graphs, and introduce a new logic –Spatio-Temporal Logic with Graph Operators(STL-GO). The key innovation in STL-GO are graph operators that enable us to reason about the number of agents along either the incoming or outgoing edges of the underlying interaction graph that satisfy a given property of interest; for example, the requirement that an agent should sense at least two neighboring agents whose task graphs indicate the ability to collaborate. We then propose novel distributed monitoring conditions for individual agents that use only local information to determine whether or not an STL-GO specification is satisfied. We compare the expressivity of STL-GO against existing spatio-temporal logic formalisms, and demonstrate the utility of STL-GO and our distributed monitors in a bike-sharing and a multi-drone case study.
more »
« less
This content will become publicly available on October 31, 2026
Distributionally Robust Predictive Runtime Verification under Spatio-Temporal Logic Specifications
Cyber-physical systems (CPS) designed in simulators, often consisting of multiple interacting agents (e.g., in multi-agent formations), behave differently in the real-world. We would like to verify these systems during runtime when they are deployed. Thus, we propose robust predictive runtime verification (RPRV) algorithms for: (1) general stochastic CPS under signal temporal logic (STL) tasks, and (2) stochastic multi-agent systems (MAS) under spatio-temporal logic tasks. The RPRV problem presents the following challenges: (1) there may not be sufficient data on the behavior of the deployed CPS, (2) predictive models based on design phase system trajectories may encounter distribution shift during real-world deployment, and (3) the algorithms need to scale to the complexity of MAS and be applicable to spatio-temporal logic tasks. To address these challenges, we assume knowledge of an upper bound on the statistical distance (in terms of anf-divergence) between the trajectory distributions of the system at deployment and design time. We are motivated by our prior work where we proposed an accurate and an interpretable RPRV algorithm for general CPS, which we here extend to the MAS setting and spatio-temporal logic tasks. Specifically, we use a learned predictive model to estimate the system behavior at runtime androbust conformal predictionto obtain probabilistic guarantees by accounting for distribution shifts. Building on our prior work, we perform robust conformal prediction over the robust semantics of spatio-temporal reach and escape logic (STREL) to obtain centralized RPRV algorithms for MAS. We empirically validate our results in a drone swarm simulator, where we show the scalability of our RPRV algorithms to MAS and analyze the impact of different trajectory predictors on the verification result. To the best of our knowledge, these are the first statistically valid algorithms for MAS under distribution shift.
more »
« less
- Award ID(s):
- 2417075
- PAR ID:
- 10647738
- Publisher / Repository:
- ACM
- Date Published:
- Journal Name:
- ACM Transactions on Cyber-Physical Systems
- Volume:
- 9
- Issue:
- 4
- ISSN:
- 2378-962X
- Page Range / eLocation ID:
- 1 to 26
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
We propose a predictive runtime monitoring framework that forecasts the distribution of future positions of mobile robots in order to detect and avoid impending property violations such as collisions with obstacles or other agents. Our approach uses a restricted class of temporal logic formulas to represent the likely intentions of the agents along with a combination of temporal logic-based optimal cost path planning and Bayesian inference to compute the probability of these intents given the current trajectory of the robot. First, we construct a large but finite hypothesis space of possible intents represented as temporal logic formulas whose atomic propositions are derived from a detailed map of the robot’s workspace. Next, our approach uses real-time observations of the robot’s position to update a distribution over temporal logic formulae that represent its likely intent. This is performed by using a combination of optimal cost path planning and a Boltzmann noisy rationality model. In this manner, we construct a Bayesian approach to evaluating the posterior probability of various hypotheses given the observed states and actions of the robot. Finally, we predict the future position of the robot by drawing posterior predictive samples using a Monte-Carlo method. We evaluate our framework using two different trajectory datasets that contain multiple scenarios implementing various tasks. The results show that our method can predict future positions precisely and efficiently, so that the computation time for generating a prediction is a tiny fraction of the overall time horizon.more » « less
-
Uncertainty in safety-critical cyber-physical systems can be modeled using a finite number of parameters or parameterized input signals. Given a system specification in Signal Temporal Logic (STL), we would like to verify that for all (infinite) values of the model parameters/input signals, the system satisfies its specification. Unfortunately, this problem is undecidable in general.Statistical model checking(SMC) offers a solution by providing guarantees on the correctness of CPS models by statistically reasoning on model simulations. We propose a new approach for statistical verification of CPS models for user-provided distribution on the model parameters. Our technique uses model simulations to learnsurrogate models, and usesconformal inferenceto provide probabilistic guarantees on the satisfaction of a given STL property. Additionally, we can provide prediction intervals containing the quantitative satisfaction values of the given STL property for any user-specified confidence level. We compare this prediction interval with the interval we get using risk estimation procedures. We also propose a refinement procedure based on Gaussian Process (GP)-based surrogate models for obtaining fine-grained probabilistic guarantees over sub-regions in the parameter space. This in turn enables the CPS designer to choose assured validity domains in the parameter space for safety-critical applications. Finally, we demonstrate the efficacy of our technique on several CPS models.more » « less
-
Cyber-Physical Systems (CPS) are integrations of computation, networking, and physical processes. The autonomy and self-adaptation capabilities of CPS mark a significant evolution from traditional control systems. Machine learning significantly enhances the functionality and efficiency of Cyber-Physical Systems (CPS). Large Language Models (LLM), like GPT-4, can augment CPS’s functionality to a new level by providing advanced intelligence support. This fact makes the applications above potentially unsafe and thus untrustworthy if deployed to the real world. We propose a comprehensive and general assurance framework for LLM-enabled CPS. The framework consists of three modules: (i) the context grounding module assures the task context has been accurately grounded (ii) the temporal Logic requirements specification module forms the temporal requirements into logic specifications for prompting and further verification (iii) the formal verification module verifies the output of the LLM and provides feedback as a guideline for LLM. The three modules execute iteratively until the output of LLM is verified. Experiment results demonstrate that our assurance framework can assure the LLM-enabled CPS.more » « less
-
Zhang, Ying (Ed.)ABSTRACT Treponema pallidum, the causative agent of syphilis, poses a significant global health threat. Its strict reliance on host-derived nutrients and difficulties inin vitrocultivation have impeded detailed metabolic characterization. In this study, we present iTP251, the first genome-scale metabolic model ofT. pallidum, reconstructed and extensively curated to capture its unique metabolic features. These refinements included the curation of key reactions such as pyrophosphate-dependent phosphorylation and pathways for nucleotide synthesis, amino acid synthesis, and cofactor metabolism. The model demonstrated high predictive accuracy, validated by a MEMOTE score of 92%. To further enhance its predictive capabilities, we developed ec-iTP251, an enzyme-constrained version of iTP251, incorporating enzyme turnover rate and molecular weight information for all reactions having gene-protein-reaction associations. Ec-iTP251 provides detailed insights into protein allocation across carbon sources, showing strong agreement with proteomics data (Pearson’s correlation of 0.88) in the central carbon pathway. Moreover, the thermodynamic analysis revealed that lactate uptake serves as an additional ATP-generating strategy to utilize unused proteomes, albeit at the cost of reducing the driving force of the central carbon pathway by 27%. Subsequent analysis identified glycerol-3-phosphate dehydrogenase as an alternative electron sink, compensating for the absence of a conventional electron transport chain while maintaining cellular redox balance. These findings highlightT. pallidum’s metabolic adaptations for survival and redox balance in nutrient-limited, extracellular host environments, providing a foundation for future research into its unique bioenergetics. IMPORTANCEThis study advances our understanding ofTreponema pallidum, the syphilis-causing pathogen, through the reconstruction of iTP251, the first genome-scale metabolic model for this organism, and its enzyme-constrained version, ec-iTP251. The work addresses the challenges of studyingT. pallidum, an extracellular, host-adapted pathogen, due to its strict dependence on host-derived nutrients and challenges inin vitrocultivation. Validated with strong agreement to proteomics data, the model demonstrates high predictive reliability. Key insights include unique metabolic adaptations such as lactate uptake for ATP production and alternative redox-balancing mechanisms. These findings provide a robust framework for future studies aimed at unraveling the pathogen's survival strategies and identifying potential metabolic vulnerabilities.more » « less
