Grid-based temporal logic inference

This paper introduces a new algorithm to infer temporal logic properties of a system from data consisting of a set of finite time system traces. We propose an algorithm that generates a Signal Temporal Logic formula by discretizing the entire domain and codomain of the system traces. Unlike many popular inference algorithms which require labeled data that represents whether a trace exhibits a desired behavior (positive) or not (negative), this approach only requires positive traces to infer temporal logic properties. We present two case studies to illustrate the efficiency and accuracy of the proposed algorithm. The first is a biological network consisting of a genetic logic circuit in a bacterial cell. The second is a fault detection problem in automotive powertrain systems. We also compare the performance of the algorithm with an existing inference algorithm.

I. Introduction

Testing and verification are very important steps in designing complex systems. Many verification techniques use a formal specification that describes admissible behaviors of a system during its execution in a mathematically unambiguous manner [1]. For this reason, specifications are expressed using appropriate logics, and Signal Temporal Logic (STL) has emerged as a rich specification language for describing continuous-time systems [2]. Traditionally, specifications are formulated by expert designers in a tedious and error-prone process. More recent methods involve learning the specifications directly from the execution traces of systems.