Automated Temporal Logic Synthesis Of Time Series Data And Its Applications
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
Temporal logic, which adds temporal operators to propositional logic, reasons about a timeline. It has been used to define specifications of systems. 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 most systems, especially large and complex ones, it is difficult for researchers to fully cover the behaviors by manually defined specifications as many system specifications are emerging and not predictable. Therefore, temporal logic specification synthesis is becoming an attractive field.
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. First, for users with enough background knowledge to determine the structures of interest, we have a convolutional neural network to classify data into pre-defined structures. Second, for those without background knowledge, we develop a data-based automatic composition method to scan through the data and composite structures according to data changes. 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.
The framework has been developed as an extendable software available on GitHub. We use CUDA GPU to accelerate the most time-consuming procedure, statistical model checking. With its loosely coupled modular design, the users can easily extend it with different logic choices, objective functions, optimization algorithms and so on.
Based on different purposes, there are two directions of temporal logic synthesis in state of the art: interpretation to reveal the behavior of data in a human-understandable way and classification to determine whether data belong to a particular system. In the direction of interpretation, we apply the framework to biological pathway models to synthesize specifications describing their behaviors in biochemical reactions. The applications demonstrate that the synthesized specifications describe the behaviors of the models faithfully. 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. As temporal logic only classifies two classes by its acceptance or rejection, we also explore one of its major competitors, spiking neural network (SNN) -the next-generation and low power neural network -to provide a more comprehensive view of the field.