Data-Driven Verification under Signal Temporal Logic Constraints
We consider systems under uncertainty whose dynamics are partially unknown. Our aim is to study satisfaction of temporal logic properties by trajectories of such systems. We express these properties as signal temporal logic formulas and check if the probability of satisfying the property is at least a given threshold. Since the dynamics are parameterized and partially unknown, we collect data from the system and employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property. The main novelty of our approach is to combine both data-driven and model-based techniques in order to have a two-layer probabilistic reasoning over the behavior of the system: one layer is related to the stochastic noise inside the system and the next layer is related to the noisy data collected from the system. We provide approximate algorithms for computing the confidence for linear dynamical systems.
Code (0)
등록된 구현이 없습니다.
Tasks
Bayesian InferenceSimilar Papers 제목 키워드 기반
ROVER: Regulator-Driven Robust Temporal Verification of Black-Box Robot Policies
We present a novel, regulator-driven approach for the temporal verification of black-box autonomous robot policies, inspired by real-world certification processes where regulators often evaluate observable behavior witho…
Robot NavigationSynchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-…
Elliptical Slice Sampling for Probabilistic Verification of Stochastic Systems with Signal Temporal Logic Specifications
Autonomous robots typically incorporate complex sensors in their decision-making and control loops. These sensors, such as cameras and Lidars, have imperfections in their sensing and are influenced by environmental condi…
Decision MakingMotion PlanningWhen Visibility Outpaces Verification: Delayed Verification and Narrative Lock-in in Agentic AI Discourse
Agentic AI systems-autonomous entities capable of independent planning and execution-reshape the landscape of human-AI trust. Long before direct system exposure, user expectations are mediated through high-stakes public …
Time-Contrastive Learning Based DNN Bottleneck Features for Text-Dependent Speaker Verification
In this paper, we present a time-contrastive learning (TCL) based bottleneck (BN)feature extraction method for speech signals with an application to text-dependent (TD) speaker verification (SV). It is well-known that sp…
Contrastive LearningSpeaker VerificationText-Dependent Speaker Verification