CISPA
Browse
cispa_all_3654.pdf (360.25 kB)

A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation

Download (360.25 kB)
journal contribution
posted on 2023-11-29, 18:05 authored by Bernd FinkbeinerBernd Finkbeiner, Martin Fränzle, Florian KohnFlorian Kohn, Paul Kröger
Signal Temporal Logic is a linear-time temporal logic designed for classifying the time-dependent signals originating from continuous-state or hybrid-state dynamical systems according to formal specifications. It has been conceived as a tool for systematizing the monitoring of cyber-physical systems, supporting the automatic translation of complex safety specifications into monitoring algorithms, faithfully representing their semantics. Almost all algorithms hitherto suggested do, however, assume perfect identity between the sensor readings, informing the monitor about the system state and the actual ground truth. Only recently have Visconti et al. addressed the issue of inexact measurements, taking up the simple model of interval-bounded per-sample error that is unrelated, in the sense of chosen afresh, across samples. We expand their analysis by decomposing the error into an unknown yet fixed offset and an independent per-sample error and show that in this setting, monitoring of temporal properties no longer coincides with collecting Boolean combinations of state predicates evaluated in each time instant over best-possible per-sample state estimates, but can be genuinely more informative in that it infers determinate truth values for monitoring conditions that interval-based evaluation remains inconclusive about. For the model-free as well as for the linear model-based case, we provide optimal evaluation algorithms based on affine arithmetic and SAT modulo theory, solving over linear arithmetic. The resulting algorithms provide conclusive monitoring verdicts in many cases where state estimations inherently remain inconclusive. In their model-based variants, they can simultaneously address the issues of uncertain sensing and partial observation.

History

Preferred Citation

Bernd Finkbeiner, Martin Fränzle, Florian Kohn and Paul Kröger. A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation. In: Algorithms. 2022.

Primary Research Area

  • Threat Detection and Defenses

Legacy Posted Date

2022-05-06

Journal

Algorithms

Open Access Type

  • Gold

Sub Type

  • Article

BibTeX

@article{cispa_all_3654, title = "A Truly Robust Signal Temporal Logic: Monitoring Safety Properties of Interacting Cyber-Physical Systems under Uncertain Observation", author = "Finkbeiner, Bernd and Fränzle, Martin and Kohn, Florian and Kröger, Paul", journal="{Algorithms}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC