Table of Contents
Fetching ...

Falsification of Autonomous Systems in Rich Environments

Khen Elimelech, Morteza Lahijanian, Lydia E. Kavraki, Moshe Y. Vardi

TL;DR

This paper tackles falsification of autonomous CPS with neural-network controllers operating in rich, uncertain environments. It reframes the problem as meta-planning in a meta-state space that couples environment mutations with system simulation, enabling incremental computation and efficient search via sampling-based planning (notably RRT). A standardized environment-based testing model is introduced, and meta-planning is shown to outperform baselines in a running autonomous-car scenario, reducing both the number of tested environments and the per-test simulation effort. The work paves the way for scalable, domain-agnostic falsification with potential for domain-knowledge integration and future probabilistic guarantees for failure estimation in open environments.

Abstract

Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of ``black-box testing'' rely on repeated system simulations to find a falsifying counterexample of a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort (NN inference queries) needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well-trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically-defined, open environments, which yield high-dimensional, simulation-dependent sensor observations. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for a ``meta-system,'' which wraps and encapsulates the examined system; we call this approach: meta-planning. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT) and can gradually integrate domain knowledge to improve the search. We support the suggested approach with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches.

Falsification of Autonomous Systems in Rich Environments

TL;DR

This paper tackles falsification of autonomous CPS with neural-network controllers operating in rich, uncertain environments. It reframes the problem as meta-planning in a meta-state space that couples environment mutations with system simulation, enabling incremental computation and efficient search via sampling-based planning (notably RRT). A standardized environment-based testing model is introduced, and meta-planning is shown to outperform baselines in a running autonomous-car scenario, reducing both the number of tested environments and the per-test simulation effort. The work paves the way for scalable, domain-agnostic falsification with potential for domain-knowledge integration and future probabilistic guarantees for failure estimation in open environments.

Abstract

Validating the behavior of autonomous Cyber-Physical Systems (CPS) and Artificial Intelligence (AI) agents, which rely on automated controllers, is an objective of great importance. In recent years, Neural-Network (NN) controllers have been demonstrating great promise. Unfortunately, such learned controllers are often not certified and can cause the system to suffer from unpredictable or unsafe behavior. To mitigate this issue, a great effort has been dedicated to automated verification of systems. Specifically, works in the category of ``black-box testing'' rely on repeated system simulations to find a falsifying counterexample of a system run that violates a specification. As running high-fidelity simulations is computationally demanding, the goal of falsification approaches is to minimize the simulation effort (NN inference queries) needed to return a falsifying example. This often proves to be a great challenge, especially when the tested controller is well-trained. This work contributes a novel falsification approach for autonomous systems under formal specification operating in uncertain environments. We are especially interested in CPS operating in rich, semantically-defined, open environments, which yield high-dimensional, simulation-dependent sensor observations. Our approach introduces a novel reformulation of the falsification problem as the problem of planning a trajectory for a ``meta-system,'' which wraps and encapsulates the examined system; we call this approach: meta-planning. This formulation can be solved with standard sampling-based motion-planning techniques (like RRT) and can gradually integrate domain knowledge to improve the search. We support the suggested approach with an experimental study on falsification of an obstacle-avoiding autonomous car with a NN controller, where meta-planning demonstrates superior performance over alternative approaches.

Paper Structure

This paper contains 48 sections, 10 equations, 7 figures, 1 table, 3 algorithms.

Figures (7)

  • Figure 1: Our running example: an autonomous car acting in an "obstructed track" environment, whose parameters define the track shape, while its elements are the obstacles, which are organized in the "obstacle collection." The car trajectory is in green. At each state, the car observes the track using a lidar sensor; the observation image of the area highlighted in red is shown on the right. The car NN-controller is trained to take in the stream observation images and steer the car to the end of the track while avoiding collision.
  • Figure 2: Testing models used for falsification of autonomous car system.
  • Figure 3: The meta-system model.
  • Figure 4: Comparing the simulation of a scene (environment and initial state), and of the scene after locally mutating it by moving the brown obstacle. The simulation progress is indicated using the green background. The environment mutation only affects the system trajectory starting from timestamp $T$, at which the mutation was observed, and the original observation history was compromised. Thus, to evaluate the mutated scene (calculate the new meta-state), it is enough to run a partial simulation, from car state at timestamp $T$.
  • Figure 5: Solving the meta-planning problem: a forward search-tree, where meta-states (nodes) represent simulated scenes, and meta-controls (edges) represent scene mutation followed by incremental re-simulation.
  • ...and 2 more figures