AUTOMATED TEMPORAL LOGIC SYNTHESIS OF TIME SERIES DATA AND ITS APPLICATIONS

Abstract

Temporal logic is important for many applications, such as formal verification where the system is formally verified against specifications defined as temporal logic formulas. However, given a system, producing temporal logic specifications for it is a challenging task.

In this thesis, we propose a framework to synthesize bounded linear temporal logic (BLTL) formulas from time series data and focus on making the formulas human-understandable. The framework adopts a commonly used two-step workflow: structure synthesis to generate parameterized formulas and parameter synthesis to concretize the parameters. For structure synthesis, we propose two methods for different use cases. For parameter synthesis, we solve it as an optimization problem by simulated annealing. We propose an innovative objective function to guide the optimization that balances both the statistical significance and interpretation quality of the synthesized formulas.

In the direction of interpretation, we apply the framework to biological pathway models to synthesize specifications describing their behaviors in biochemical reactions. In the direction of classification, we apply the framework to classify electrocardiogram (ECG) beats. Experiments show that our framework outperforms existing machine learning methods in individual patient classification where data are few.