Monitoring hyperproperties
From MaRDI portal
Publication:2008281
DOI10.1007/S10703-019-00334-ZzbMATH Open1425.68254DBLPjournals/fmsd/FinkbeinerHST19arXiv1807.00758OpenAlexW4286447266WikidataQ91736867 ScholiaQ91736867MaRDI QIDQ2008281FDOQ2008281
Marvin Stenger, Bernd Finkbeiner, Leander Tentrup, Christopher Hahn
Publication date: 25 November 2019
Published in: Formal Methods in System Design (Search for Journal in Brave)
Abstract: Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. HyperLTL extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express Hyperproperties. We investigate the runtime verification problem of HyperLTL formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions may grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that deciding monitorability of HyperLTL formulas is PSPACE-complete for input models (1) and (3). Deciding monitorability is PSPACE-complete for alternation-free HyperLTL formulas in input model (2). For every input model, we provide practical monitoring algorithms. We also present various optimization techniques. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimized the number of traces that need to be stored. Finally, we provide an optimization that succinctly represents the stored traces by sharing common prefixes. We evaluate our optimizations, showing that this leads to much more scalable monitoring, in particular, significantly lower memory consumption.
Full work available at URL: https://arxiv.org/abs/1807.00758
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Cites Work
- Optimized temporal monitors for SystemcC
- Parametric Trace Slicing and Monitoring
- Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors
- Checking finite traces using alternating automata
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- Title not available (Why is that?)
- Model Checking Information Flow in Reactive Systems
- Monitoring hyperproperties
- Rewriting-Based Runtime Verification for Alternation-Free HyperLTL
- Computer Aided Verification
Cited In (16)
- Program Repair for Hyperproperties
- Model checking hyperproperties for Markov decision processes
- Software Verification of Hyperproperties Beyond k-Safety
- Monitoring of Real-Time Properties
- Monitoring hyperproperties
- Verifying bounded subset-closed hyperproperties
- Bounded model checking for hyperproperties
- Efficient loop conditions for bounded model checking hyperproperties
- Explaining Hyperproperty Violations
- Runtime enforcement of hyperproperties
- Title not available (Why is that?)
- Synthesis from hyperproperties
- Monitoring hyperproperties with circuits
- Monitorable hyperproperties of nonterminating systems
- Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption
- Finite-word hyperlanguages
This page was built for publication: Monitoring hyperproperties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2008281)
