Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

If At First You Don't Succeed: Extended Monitorability through Multiple Executions

Antonis Achilleos, Adrian Francalanza, Jasmine Xuereb

TL;DR

This work introduces a framework for extending runtime verification to branching-time properties by observing multiple executions of the same system. It formalizes a two-stage process—history aggregation across runs and history analysis via a determinism-aware proof system—within an instrumented labeled transition system, and proves key correctness properties (veracity, determinism, irrevocability) for multi-run monitors. The authors define an extended monitorable fragment $\textsc{sHML}^\vee_{\textsc{Det}}$ that is maximally expressive under deterministic internal actions and provide a synthesis function that constructs witness monitors from formulas. They instantiate the framework to actor-based systems, showing how deterministic and non-deterministic actions affect monitorability and deriving lower bounds on the number of required executions from property structure. The results advance practical runtime verification by enabling robust monitoring of complex branching-time properties and offer methods for tool support and future grey-box extensions.

Abstract

This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited to a single system execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal mu-calculus, a well-studied foundational logic that is used by state-of-the-art model checkers. Our results show that the proposed setup can systematically extend previously established monitorability limits for branching-time properties. We then validate our results by instantiating them to verify actor-based systems. We also prove bounds that capture the correspondence between the syntactic structure of a property and the number of required system runs.

If At First You Don't Succeed: Extended Monitorability through Multiple Executions

TL;DR

This work introduces a framework for extending runtime verification to branching-time properties by observing multiple executions of the same system. It formalizes a two-stage process—history aggregation across runs and history analysis via a determinism-aware proof system—within an instrumented labeled transition system, and proves key correctness properties (veracity, determinism, irrevocability) for multi-run monitors. The authors define an extended monitorable fragment that is maximally expressive under deterministic internal actions and provide a synthesis function that constructs witness monitors from formulas. They instantiate the framework to actor-based systems, showing how deterministic and non-deterministic actions affect monitorability and deriving lower bounds on the number of required executions from property structure. The results advance practical runtime verification by enabling robust monitoring of complex branching-time properties and offer methods for tool support and future grey-box extensions.

Abstract

This paper studies the extent to which branching-time properties can be adequately verified using runtime monitors. We depart from the classical setup where monitoring is limited to a single system execution and investigate the enhanced observational capabilities when monitoring a system over multiple runs. To ensure generality in our results, we focus on branching-time properties expressed in the modal mu-calculus, a well-studied foundational logic that is used by state-of-the-art model checkers. Our results show that the proposed setup can systematically extend previously established monitorability limits for branching-time properties. We then validate our results by instantiating them to verify actor-based systems. We also prove bounds that capture the correspondence between the syntactic structure of a property and the number of required system runs.
Paper Structure (35 sections, 108 theorems, 62 equations, 6 figures)

This paper contains 35 sections, 108 theorems, 62 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A Framework for Repeated Monitoring
  4. History Aggregation
  5. History Analysis
  6. Monitor Correctness
  7. Monitorability
  8. Actor Systems
  9. Actor Structural Equivalence and Silent Actions
  10. Deterministic and Non-deterministic Traceable Actions
  11. Establishing Bounds
  12. Related Work
  13. Conclusion
  14. LTS Properties
  15. History Analysis
  16. ...and 20 more sections

Key Result

Proposition 2.0

For all (closed) formulae $\varphi\!\in\!\textsc{recHML}\xspace$, if $p\xspace\!\in\!\llbracket\varphi\rrbracket$ and $p\xspace\!\equiv\! q\xspace$ then $q\xspace\!\in\!\llbracket\varphi\rrbracket$. ∎

Figures (6)

  • Figure 1: recHML in the Branching-Time Setting.
  • Figure 2: Monitors and Instrumentation
  • Figure 3: Proof System
  • Figure 4: Proof derivation showing that $m\xspace_1$ rejects $\{t_1,t_2\}$
  • Figure 5: Proof derivation showing that $m\xspace_1$ does not reject $\{t_1\}$
  • ...and 1 more figures

Theorems & Definitions (245)

  • Example 1.1
  • Example 1.2
  • Example 1.3
  • Example 1.4
  • Remark 1
  • Proposition 2.0: Behavioural Equivalence
  • Theorem 2.1: Monitorability FrancalanzaAI17:monitorability-branching
  • Example 2.1
  • Example 3.1
  • Example 3.2
  • ...and 235 more