Data-Driven Verification under Signal Temporal Logic Constraints
- URL: http://arxiv.org/abs/2005.05040v1
- Date: Fri, 8 May 2020 08:32:30 GMT
- Title: Data-Driven Verification under Signal Temporal Logic Constraints
- Authors: Ali Salamati, Sadegh Soudjani, and Majid Zamani
- Abstract summary: 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 employ Bayesian inference techniques to associate a confidence value to the satisfaction of the property.
- Score: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
Related papers
- Modeling Unknown Stochastic Dynamical System Subject to External Excitation [4.357350642401934]
We present a numerical method for learning unknown nonautonomous dynamical system.
Our basic assumption is that the governing equations for the system are unavailable.
When a sufficient amount of such I/O data are available, our method is capable of learning the unknown dynamics.
arXiv Detail & Related papers (2024-06-22T06:21:44Z) - Data-Driven Reachability Analysis of Stochastic Dynamical Systems with
Conformal Inference [1.446438366123305]
We consider data-driven reachability analysis of discrete-time dynamical systems using conformal inference.
We focus on learning-enabled control systems with complex closed-loop dynamics.
arXiv Detail & Related papers (2023-09-17T07:23:01Z) - Interactive System-wise Anomaly Detection [66.3766756452743]
Anomaly detection plays a fundamental role in various applications.
It is challenging for existing methods to handle the scenarios where the instances are systems whose characteristics are not readily observed as data.
We develop an end-to-end approach which includes an encoder-decoder module that learns system embeddings.
arXiv Detail & Related papers (2023-04-21T02:20:24Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
We propose a method for synthesising controllers for Markov jump linear systems.
Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS.
We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
arXiv Detail & Related papers (2022-12-01T17:36:30Z) - Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression [11.729744197698718]
Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties.
We develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements.
arXiv Detail & Related papers (2021-12-31T05:10:05Z) - Supervised DKRC with Images for Offline System Identification [77.34726150561087]
Modern dynamical systems are becoming increasingly non-linear and complex.
There is a need for a framework to model these systems in a compact and comprehensive representation for prediction and control.
Our approach learns these basis functions using a supervised learning approach.
arXiv Detail & Related papers (2021-09-06T04:39:06Z) - Reconstructing a dynamical system and forecasting time series by
self-consistent deep learning [4.947248396489835]
We introduce a self-consistent deep-learning framework for a noisy deterministic time series.
It provides unsupervised filtering, state-space reconstruction, identification of the underlying differential equations and forecasting.
arXiv Detail & Related papers (2021-08-04T06:10:58Z) - Mining Interpretable Spatio-temporal Logic Properties for Spatially
Distributed Systems [0.7585262843303869]
We propose the first set of algorithms for unsupervised learning for temporal data.
We show that our method generates STREL formulas of bounded description using a complexity decision-tree approach.
We demonstrate the effectiveness of our approach on case studies from diverse domains such as urban transportation, green infrastructure, and air quality monitoring.
arXiv Detail & Related papers (2021-06-16T04:51:26Z) - Using Data Assimilation to Train a Hybrid Forecast System that Combines
Machine-Learning and Knowledge-Based Components [52.77024349608834]
We consider the problem of data-assisted forecasting of chaotic dynamical systems when the available data is noisy partial measurements.
We show that by using partial measurements of the state of the dynamical system, we can train a machine learning model to improve predictions made by an imperfect knowledge-based model.
arXiv Detail & Related papers (2021-02-15T19:56:48Z) - A Novel Anomaly Detection Algorithm for Hybrid Production Systems based
on Deep Learning and Timed Automata [73.38551379469533]
DAD:DeepAnomalyDetection is a new approach for automatic model learning and anomaly detection in hybrid production systems.
It combines deep learning and timed automata for creating behavioral model from observations.
The algorithm has been applied to few data sets including two from real systems and has shown promising results.
arXiv Detail & Related papers (2020-10-29T08:27:43Z) - Active Learning for Nonlinear System Identification with Guarantees [102.43355665393067]
We study a class of nonlinear dynamical systems whose state transitions depend linearly on a known feature embedding of state-action pairs.
We propose an active learning approach that achieves this by repeating three steps: trajectory planning, trajectory tracking, and re-estimation of the system from all available data.
We show that our method estimates nonlinear dynamical systems at a parametric rate, similar to the statistical rate of standard linear regression.
arXiv Detail & Related papers (2020-06-18T04:54:11Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.