Formal Methods for Safe Autonomy: Data-driven Verification, Synthesis, and Applications/ Chuchu Fan

Format:

Book

Author/Creator:

Fan, Chuchu, author.

Series:

ACM books - Collection 3 ; #59.

ACM books, 2374-6777 ; #59

Language:

English

Subjects (All):

Formal Methods for Safe Autonomy(Computer Science).

Genre:

Electronic books.

Physical Description:

1 PDF (xii, 172pages) LuaTEX

Edition:

First Edition

Place of Publication:

[New York, NY, USA] : Association for Computing Machinery; [2025].

System Details:

Mode of access: World Wide Web

System requirements: Adobe Acrobat Reader

Contents:

Preface

Acknowledgments

1 Introduction

1.1 Locally Optimal Guaranteed Reachability for Nonlinear Dynamics

1.2 Verification of Black-box Components with Probabilistic Guarantees

1.3 Approximate Partial Order Reduction for Distributed Autonomous Systems

1.4 Control Synthesis of Large-dimensional Systems

1.5 Summary of Contributions

1.6 Book Structure

2 Mathematical Preliminaries

2.1 Vectors and Matrices

2.2 Sets

2.3 Functions

3 Models of Autonomous Systems

3.1 Discrete-time Transition Systems

3.2 Trajectories and Closures

3.3 Dynamical Systems

3.4 Hybrid Systems

4 Data-driven Verification

4.1 Introduction

4.2 Related Work on Verification

4.3 Simulation and Reachtube

4.4 Discrepancy Function

4.5 Verification Algorithm

4.6 Summary

5 Computing Discrepancy

5.1 Introduction

5.2 Linear Models

5.3 Nonlinear Models: Optimization-based Approaches

5.4 Nonlinear Models: Local Discrepancy

5.5 Reachtube Computation for Hybrid System

5.6 Summary

6 Verification of Models with Black-box Components

6.1 Introduction

6.2 Hybrid Systems with Black-box Modules

6.3 Learning Discrepancy from Simulations

6.4 Example: ADAS and Autonomous Driving Control

6.5 Example: Analyzing Risk in Automatic Emergency Braking Systems

6.6 Other Examples: Powertrain, Spacecraft, and Gear Transmission

6.7 Formal Reasonings on Hybrid Systems with Black-box Modules

6.8 Experiments on Behavior Containment Reasoning

6.9 Summary

7 Approximate Partial Order Reduction

7.1 Introduction

7.2 Background

7.3 Independent Actions and Neighboring Executions

7.4 Effect of ɛ-Independent Traces

7.5 Reachability with Approximate POR

7.6 Experimental Evaluation of Approximate POR

7.7 Summary

8 Controller Synthesis for Linear Systems with Reach-avoid Specification

8.1 Introduction

8.2 Related Work on Synthesis

8.3 Bounded Controller Synthesis Problem on Discrete-time Linear Control Systems

8.4 Synthesis Algorithm

8.5 RealSyn Implementation and Evaluation

8.6 Summary

9 Conclusions

Bibliography

Author's Biography

Index

Other Format:

Print version:

ISBN:

3603288

9798400708664

9798400708640

Access Restriction:

Restricted for use by site license.