Formal Methods for Autonomous Systems

• URL: http://arxiv.org/abs/2311.01258v1
• Date: Thu, 2 Nov 2023 14:18:43 GMT
• Title: Formal Methods for Autonomous Systems
• Authors: Tichakorn Wongpiromsarn, Mahsa Ghasemi, Murat Cubuktepe, Georgios Bakirtzis, Steven Carr, Mustafa O. Karabag, Cyrus Neary, Parham Gohari, Ufuk Topcu
• Abstract summary: Formal methods have played a key role in establishing the correctness of safety-critical systems. Main building blocks of formal methods are models and specifications. We consider correct-by-construction synthesis under various formulations.
• Score: 21.989467515686858
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal methods refer to rigorous, mathematical approaches to system development and have played a key role in establishing the correctness of safety-critical systems. The main building blocks of formal methods are models and specifications, which are analogous to behaviors and requirements in system design and give us the means to verify and synthesize system behaviors with formal guarantees. This monograph provides a survey of the current state of the art on applications of formal methods in the autonomous systems domain. We consider correct-by-construction synthesis under various formulations, including closed systems, reactive, and probabilistic settings. Beyond synthesizing systems in known environments, we address the concept of uncertainty and bound the behavior of systems that employ learning using formal methods. Further, we examine the synthesis of systems with monitoring, a mitigation technique for ensuring that once a system deviates from expected behavior, it knows a way of returning to normalcy. We also show how to overcome some limitations of formal methods themselves with learning. We conclude with future directions for formal methods in reinforcement learning, uncertainty, privacy, explainability of formal methods, and regulation and certification.

Related papers

• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Towards Formal Fault Injection for Safety Assessment of Automated Systems [0.0]
  This paper introduces formal fault injection, a fusion of these two techniques throughout the development lifecycle. We advocate for a more cohesive approach by identifying five areas of mutual support between formal methods and fault injection.
  arXiv  Detail & Related papers  (2023-11-16T11:34:18Z)
• 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)
• Learning-Based Optimal Control with Performance Guarantees for Unknown Systems with Latent States [4.4820711784498]
  This paper proposes a novel method for the computation of an optimal input trajectory for unknown nonlinear systems with latent states. The effectiveness of the proposed method is demonstrated in a numerical simulation.
  arXiv  Detail & Related papers  (2023-03-31T11:06:09Z)
• In-Distribution Barrier Functions: Self-Supervised Policy Filters that Avoid Out-of-Distribution States [84.24300005271185]
  We propose a control filter that wraps any reference policy and effectively encourages the system to stay in-distribution with respect to offline-collected safe demonstrations. Our method is effective for two different visuomotor control tasks in simulation environments, including both top-down and egocentric view settings.
  arXiv  Detail & Related papers  (2023-01-27T22:28:19Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Structure-Preserving Learning Using Gaussian Processes and Variational Integrators [62.31425348954686]
  We propose the combination of a variational integrator for the nominal dynamics of a mechanical system and learning residual dynamics with Gaussian process regression. We extend our approach to systems with known kinematic constraints and provide formal bounds on the prediction uncertainty.
  arXiv  Detail & Related papers  (2021-12-10T11:09:29Z)
• A Review of Formal Methods applied to Machine Learning [0.6853165736531939]
  We review state-of-the-art formal methods applied to the emerging field of the verification of machine learning systems. We first recall established formal methods and their current use in an exemplar safety-critical field, avionic software. We then provide a comprehensive and detailed review of the formal methods developed so far for machine learning, highlighting their strengths and limitations.
  arXiv  Detail & Related papers  (2021-04-06T12:48:17Z)
• Proceedings Second Workshop on Formal Methods for Autonomous Systems [0.0]
  The goal of FMAS is to bring together leading researchers who are tackling the challenges of autonomous systems using formal methods. We are interested in the use of formal methods to specify, model, or verify autonomous or robotic systems; in whole or in part.
  arXiv  Detail & Related papers  (2020-12-02T13:08:57Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  We present a semi-formal verification approach for decision-making tasks based on interval analysis. Our method obtains comparable results over standard benchmarks with respect to formal verifiers. Our approach allows to efficiently evaluate safety properties for decision-making models in practical applications.
  arXiv  Detail & Related papers  (2020-10-19T11:18:06Z)
• 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.