Deep Learning Temporal Logic Specifications

This thesis seeks to explain a new method of extracting temporal logic formulas from time series data using machine learning. Two strategies were followed during the development of this research: first, a generative adversarial network was combined with already-existing temporal logic extraction code by Belta. This was achieved by injecting temporal logic formula-generating code into the discriminator within the generative adversarial network. This approach proved infeasible due to the difficulty of moving data back and forth between TensorFlow and MATLAB, so the next approach used recurrent neural networks to create custom layers where each layer represented an atom or a temporal logic operation. The layers' weights were then trained to decide which atoms and operators produced the most accurate formula; this was done by comparing the RNN outputs with formula robustness values calculated by Breach, a temporal logic monitor. We tested our implementations and established that for the tested operators, we are able to extract temporal logic formulas from the trained network. The original intended significance of this research was in allowing autonomous vehicles to describe their decision-making processes via formulas that can be checked by experts. The goal was to avoid the "black box" effect currently in place, in which the results of a network's decision-making process can be checked for quality, but the method of making decisions is not easily parsed. Being able to understand the reasons behind choices a network is making, in the case of autonomous vehicles, would add greatly to such vehicles' safety and make them more viable for general use. The values used for training data during this project were simulated distance signals from unmanned aerial vehicles over time, but this concept could be expanded to cover the full complexity of an autonomous vehicle's produced signals, such as position, velocity, and acceleration, in order to more effectively leverage the research enclosed here. ; Key Words: Machine ...