We present Mixed-time Signal Temporal Logic ((Formula Presented)), a specification formalism which extends STL by capturing the discrete/ continuous time duality found in many cyber-physical systems (CPS), as well as mixed-signal electronic designs. In (Formula Presented), properties of components with continuous dynamics are expressed in STL, while specifications of components with discrete dynamics are written in LTL. To combine the two layers, we evaluate formulas on two traces, discrete- and continuous-time, and introduce two interface operators that map signals, properties and their satisfaction signals across the two time domains. We show that STL-mx has the expressive power of STL supplemented with an implicit T-periodic clock signal. We develop and implement an algorithm for monitoring STL-mx formulas and illustrate the approach using a mixed-signal example.
CITATION STYLE
Ferrère, T., Maler, O., & Ničković, D. (2019). Mixed-Time Signal Temporal Logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11750 LNCS, pp. 59–75). Springer. https://doi.org/10.1007/978-3-030-29662-9_4
Mendeley helps you to discover research relevant for your work.