Automated Temporal Logic Synthesis of Time Series Data and Its Applications
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
Temporal logic, adding temporal operators to propositional logics, reasons about a time line. It has been used to define properties of systems evolving through time. Temporal logic is important for many applications, such as formal verifications where the system is formally verified against specifications defined as temporal logic formulas.
However, to produce temporal logic specifications itself has become a problem. In most systems, especially large and complex ones, it is difficult for researchers to manually define the specifications as many system properties are emerging and not predictable. Therefore, temporal logic property synthesis is becoming an attractive field.
In this thesis proposal, we propose to develop an end-to-end framework that synthesize temporal logic properties from input time series data. Unlike the existing works, synthesizing properties to classify data, our framework focuses on the interpretation of data, to reveal the behaviour of the data in a human understandable way.
We apply the framework to biological pathway models to synthesize properties describing their behaviours, of both single species and relationship of multiple species. The applications demonstrates that the synthesized properties describes the behaviour of the models faithfully.