Search

Optimization-based falsification employs stochastic optimization algorithms to search for error input of hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely time staging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval to another, incrementally constructing an input signal candidate. Our experiments show that time staging can dramatically increase performance in some realistic examples. We also present theoretical results that suggest the kinds of models and specifications for which time staging is likely to be effective., In Proceedings SNR 2021, arXiv:2207.04391

Reinforcement learning (RL) is an attractive way to implement high-level decision-making policies for autonomous driving, but learning directly from a real vehicle or a high-fidelity simulator is variously infeasible. We therefore consider the problem of transfer reinforcement learning and study how a policy learned in a simple environment using WiseMove can be transferred to our high-fidelity simulator, W ise M ove . WiseMove is a framework to study safety and other aspects of RL for autonomous driving. W ise M ove accurately reproduces the dynamics and software stack of our real vehicle. We find that the accurately modelled perception errors in W ise M ove contribute the most to the transfer problem. These errors, when even naively modelled in WiseMove , provide an RL policy that performs better in W ise M ove than a hand-crafted rule-based policy. Applying domain randomization to the environment in WiseMove yields an even better policy. The final RL policy reduces the failures due to perception errors from 10% to 2.75%. We also observe that the RL policy has significantly less reliance on velocity compared to the rule-based policy, having learned that its measurement is unreliable.

We present and analyse an algorithm that quickly finds falsifying inputs for hybrid systems. Our method is based on a probabilistically directed tree search, whose distribution adapts to consider an increasingly fine-grained discretization of the input space. In experiments with standard benchmarks, our algorithm shows comparable or better performance to existing techniques, yet it does not build an explicit model of a system. Instead, at each decision point within a single trial, it makes an uninformed probabilistic choice between simple strategies to extend the input signal by means of exploration or exploitation. Key to our approach is the way input signal space is decomposed into levels, such that coarse segments are more probable than fine segments. We perform experiments to demonstrate how and why our approach works, finding that a fully randomized exploration strategy performs as well as our original algorithm that exploits robustness. We propose this strategy as a new baseline for falsification and conclude that more discriminative benchmarks are required.

We consider the problem of verifying complex learned controllers using distillation. In contrast to previous work, we require that the distilled model maintains behavioural fidelity with an oracle, defining the notion of non-divergent path length (NPL) as a metric. We demonstrate that current distillation approaches with proven accuracy bounds do not have high expected NPL and can be out-performed by naive behavioural cloning. We thus propose a distillation algorithm that typically gives greater expected NPL, improved sample efficiency, and more compact models. We prove properties of NPL maximization and demonstrate the performance of our algorithm on deep Q-network controllers for three standard learning environments that have been used in this context: Pong, CartPole and MountainCar.