A Formal Framework for Noisy Runtime Verification

1 Introduction

• Competing definitions make it unclear both before and after the fact which properties can be monitored.The paper notes that monitoring depends on the chosen property being monitorable, but this is not obvious in advance or afterward.Source: §1 · p. 1
• Noisy channels motivate questions about which properties are immune to mutations and when monitoring remains trustworthy.Examples include out-of-order Mars Science Laboratory messages and spurious readings from dropped UAV telemetry.Source: §1 · pp. 1–2
• EDMon provides a framework for expressing, evaluating, and comparing noisy runtime verification concepts, and for proposing novel concepts and results.The paper also presents its framework as useful for further exploration of such concepts and results.Source: §1 · p. 2

1.1 Comparison With Prior Work

• EDMon’s contribution lies in adding distinctive dynamic elements and observation modals; its framing is quite similar to [6], but it differs primarily, though not exclusively, through careful attention to mutation.At present, EDMon is formulated in a propositional setting.Source: §1.1 · p. 2

1.2 Contributions

• EDMon formalizes three dominant monitorability concepts, an extended family of liveness classes, and central results connecting monitorability and liveness.The paper also claims results about immunity and its relations to liveness and monitorability, and points toward novel concepts across these topics.Source: §1.2 · pp. 2–3

2 Syntax and Semantics

• This section describes the syntax and semantics of EDMon.Source: §2 · p. 3
• The presentation begins with preliminary material.Source: §2 · p. 3
• Proofs of the preliminary lemmas are omitted because they are described as straightforward.Source: §2 · p. 3

2.1 Preliminaries

• S* denotes finite sequences over S, Sω denotes infinite sequences, and ε is the empty sequence.Source: §2.1 · p. 3
• The preliminaries define operations on sequence pairs and establish that shifting k times yields the first k terms of the trace.Lemma 3 states trace(shift^k(s, σ)) = trace(s, σ)^k.Source: §2.1 · p. 3
• Relations are defined with composition, inverse, and reflexive-transitive closure notation, and their product composition obeys a componentwise identity.Lemma 4 states (R1 × R2) ◦ (R3 × R4) = (R1 ◦ R3) × (R2 ◦ R4).Source: §2.1 · p. 3

2.2 Syntax

• EDMon adds a “determines” modality D, mutation modalities ⟨μ⟩, and observation modalities ⟨obs⟩ and ⟨obs*⟩ to LTL.These supply epistemic, dynamic, and monitorability machinery, respectively.Source: §2.2 · p. 4
• The grammar distinguishes four syntactic classes: LTL formulas, mutations, observations, and EDMon formulas.Mutations include st, loss, ooo, cor, and operators for union, composition, inverse, and iteration.Source: §2.2 · p. 4
• The grammar is stratified, so dynamic, observation, and epistemic modalities cannot occur within the scope of temporal modalities.For example, DXp is well-formed, whereas XDp is not.Source: §2.2 · p. 4
• The syntax uses abbreviations including F for “eventually,” G for “always,” and F≥nφ for φ happening at least n times.X is read as “next,” and D as “determines.”Source: §2.2 · p. 4

2.3 Semantics

• An EDMon point combines a finite sequence and an infinite trace suffix, representing a location at which formulas are evaluated.The semantics uses points in a structure with carrier Σ* × Σω.Source: §2.3 · p. 5
• Lift extends relations on finite sequences to points while requiring their infinite suffixes to be identical.The paper states that Lift is a homomorphism for the algebra of relations.Source: §2.3 · p. 5
• F≥nφ holds exactly when φ is true at n distinct shifts of the point.This gives the semantics of “φ will happen at least n times.”Source: §2.3 · p. 6
• For LTL formulas, the split between finite prefix and infinite suffix does not affect truth; only the combined trace matters.Thus EDMon evaluates LTL formulas on points just as ordinary LTL evaluates their represented traces.Source: §2.3 · p. 7
• Mutation relations are extended recursively from atomic mutations using composition, union, iteration, and inverse.The semantics of ⟨μ⟩A requires some mutation-related point to satisfy A.Source: §2.3 · p. 7

2.4 Understanding the Language

• A point represents the sensor’s lifetime trace and the finite prefix already transmitted to the monitor.The section uses modal sanity checks to show how these evaluations behave.Source: §2.4 · p. 8

2.4.1 Observation modals.

• An observation advances the transmitted prefix without changing the underlying trace, and ⟨obs*⟩A holds when A holds after some number of additional observations.For LTL formulas, the section states observation-invariance: sending information does not change their truth.Source: §2.4.1 · p. 8

2.4.2 Mutation modals.

• Mutation and observation only half commute: ⟨μ⟩⟨obs⟩A implies ⟨obs⟩⟨μ⟩A, but the converse can fail.The out-of-order example demonstrates the failure of the converse.Source: §2.4.2 · p. 8

2.4.3 Epistemic modals.

• Determination and observation also only half commute, while determination and mutation fully commute because they act on different coordinates.The example shows that after observing the next tick, a monitor can determine whether q holds then, without being able to determine beforehand that it will observe q.Source: §2.4.3 · p. 9

2.5 Whence Monitors?

• A μ-sufficient surrogate B for A satisfies the validity condition ⟨μ⟩B→A.It identifies received messages that guarantee A was true of the sender.Source: §2.5 · p. 10
• Conjoining an arbitrary C to a surrogate preserves sufficiency but can make the monitor act less often and miss cases when it ought to act.The proposed weakest surrogate is [μ−]A, which is implied by every surrogate and is itself a surrogate.Source: §2.5 · p. 10
• The weakest-surrogate solution is constrained because existing monitors cannot handle EDMon formulas and the theoretical monitoring procedure remains unclear.The authors say these two problems can be solved together in a range of cases, but defer the full solution and give a case study.Source: §2.5 · p. 10
• For k≥1 and l≥0, if ⟨cor^l⟩A→F≥kB is valid, then A→F≥k+lB is valid for LTL A and propositional B.Theorem 19 gives the corresponding negative-frequency implication: validity of ⟨cor^l⟩A→¬F≥k+lB entails validity of A→¬F≥kB.Source: §2.5 · p. 11
• For propositional B, ⟨cor^l⟩F≥k+lB→F≥kB and ⟨cor^l⟩¬F≥kB→¬F≥k+lB are EDMon-valid.These results yield the corresponding weakest corruption-sufficient surrogates for the frequency properties.Source: §2.5 · pp. 11–12
• When [μ−]A is equivalent to an LTL formula, existing systems can monitor it in a well-defined way, and EDMon certifies that monitoring is sound and optimal.The authors present this as a route to implementable solutions to monitorability problems.Source: §2.5 · pp. 10, 12

2.6 Monitoring on Multiple Channels

• Multiple channels may monitor the same instrument, and different noise types may arise on different channels.Source: §2.6 · p. 12
• A joint prediction from reordering and corrupting channels can support trusting the first n−1 parts when both give the same prediction for the next n ticks.The section presents this as a partial, not-quite-but-nearly correct rephrasing.Source: §2.6 · p. 13
• Dual monitoring can combine information from two streams to support inferences beyond what either stream captures alone.The section presents several such EDMon-valid results, while leaving further examples to the reader.Source: §2.6 · p. 13

3 EDMon’s NRV-adequacy

• EDMon is presented as a framework that captures important NRV concepts and many of their main results.The section identifies monitorability, liveness classes, and immunity as the concepts it will address.Source: §3 · p. 13

3.1 Monitorability

• EDMon models s-monitorability, with judgments made relative to a received string and verdicts reflecting whether further observations could determine the property.The authors restrict attention to classical, s-, and weak monitorability, excluding four-valued monitorability as outside EDMon’s scope.Source: §3.1 · pp. 13–14

3.1.2 Classical Monitorability.

• A is classically monitorable iff P⟨obs∗⟩(D A∨D¬A) is EDMon-valid iff A is s-monitorable for all s∈Σ∗.Classical monitorability requires that no prefix be ugly; unlike s-monitorability, it gives a single property-level judgment.Source: §3.1.2 · p. 15

3.1.3 Weak Monitorability.

• A is weakly monitorable iff D A∨D¬A is satisfiable iff A is s-monitorable for some s.Unlike classical monitorability’s requirement that no prefix be ugly, weak monitorability requires only some non-ugly prefix.Source: §3.1.3 · p. 16

3.2 Liveness Classes

• The section begins its liveness-class discussion with Peled and Havelund’s extended safety-liveness hierarchy, which tracks six properties.The cited passage introduces the hierarchy but does not yet report how EDMon captures its classes.Source: §3.2 · p. 16
• EDMon characterizes all six liveness classes: always or sometimes finitely refutable or satisfiable, and never finitely refutable or satisfiable.The classes distinguish whether finite prefixes can force satisfaction or refutation across all continuations, for some continuations, or never.Source: §3.2 · pp. 16–17

3.3 Further Property Classes

• EDMon can represent the five property classes introduced in: proximate, tolerant, permissive, inclusive, and exclusive.The paper restricts its discussion to formula-defined properties of interest.Source: §3.3 · p. 17, §3.3.1 · p. 17

3.3.1 The Classes.

• Blocked loss (bloss), which drops a finite sequence of states, is inexpressible using only loss, cor, st, and ooo.The authors argue that bloss can alter sequential rather than scattered states and sometimes changes more than two states at once; they also show that a prior “completeness” claim about combinations of mutations is false as strictly written.Source: §3.3.1 · pp. 17–18
• A property is inclusive, or its negation exclusive, exactly when it is equivalent to a conjunction of F-ed state descriptions over a finite atom set.The paper states these characterizations for finite S ⊆ At.Source: §3.3.1 · p. 18
• The paper corrects earlier class-inclusion claims for the trivial properties and gives EDMon-valid conditions for properties equivalent to conjunctions of F-ed state descriptions.Theorem 33 gives conditions involving bloss− and P for A and ¬A, respectively.Source: §3.3.1 · p. 19

3.4 Immunity

• True-false immunity to a mutation is equivalent to EDMon-validity of preservation conditions for D A and D¬A under the mutation and its inverse.The theorem expresses immunity through four validity conditions, covering both truth and falsity evidence across mutation-related states.Source: §3.4 · p. 20
• A verdict is trustworthy when, across mutation-related traces, receiving that verdict on one trace guarantees the same verdict on the related trace.The definition applies to verdicts ⊤, ⊥, and ?.Source: §3.4 · p. 20
• ⊤ is trustworthy iff D_A → [μ−]D_A is EDMon-valid, and ⊥ is trustworthy iff D_¬A → [μ−]D_¬A is EDMon-valid.Theorem 37 also characterizes trustworthiness of ?, but the supplied passage does not include its full condition.Source: §3.4 · p. 20
• True-false immunity to a mutation holds iff ⊤, ⊥, and ? are all trustworthy for the property with respect to that mutation.This is Corollary 38.Source: §3.4 · p. 20

4.1 Relationship With Other Logics

• EDMon validates every propositional tautology instance and preserves validity under conjunction, implication, mutation, observation, D, and the listed LTL operators.The listed LTL operators are X and G.Source: §4.1 · p. 21
• Two LLTL identities are EDMon-valid: the stated G-based implication and the recursive characterization of until.The until identity is (𝜙1 U 𝜙2) ↔ (𝜙2 ∨ (𝜙1 ∧ X(𝜙1 U 𝜙2))).Source: §4.1 · p. 21
• Every well-formed EDMon substitution of a PDL theorem is EDMon-valid, with allowed substitutions depending on the axiom’s grammatical form.Mutations, observations, and D are permitted for some axioms, while others allow only mutations or mutations and observations.Source: §4.1 · p. 22

4.2 General Modal Features

• The closure (c st ∪ d cor ∪ loss)* relates every pair of nonempty strings, but does not relate the empty string to any nonempty string.The text notes that replacing st, which duplicates an existing element, with insertion instead yields the universal relation.Source: §4.2 · p. 24
• For k ≥ 0, DX^k p ∨ DX^k ¬p holds exactly when |s| > k; its negation holds exactly when |s| ≤ k, identifying initial points at k = 0.The formula ¬(D p ∨ D ¬p) is true exactly at initial points and is called init.Source: §4.2 · p. 24
• The mutation (loss ∪ cor ∪ st)* has an S5-like axiom, whereas (loss ∪ loss−)* has proper S5 logic, distinguishing their modal behavior.The section identifies the latter mutation’s relation as universal on Σ*, unlike the former.Source: §4.2 · pp. 24–25

4.3 Specialized Validities

• GM7 factors paired diamond modalities out of a conjunction when the result is mediated by a third diamond modality.Theorem 62 states this validity for all A and B in LLTL.Source: §4.3 · pp. 25–26

4.4 Putting the Validities to Work

• True-false immunity to μ is equivalent to immunity to μ∗, proving Theorem 2 of in EDMon.Theorem 63 establishes the equivalence.Source: §4.4 · pp. 26–27
• If a verdict is trustworthy for A with respect to μ, it remains trustworthy for A with respect to μ∗.The result applies to each verdict v in {⊤, ⊥, ?}.Source: §4.4 · p. 27
• The temporary operator bloss can be dispensed with in characterizing Tolr and Perm, using loss-based formulations instead.The argument equates the relevant validity conditions for bloss− and (loss−)∗, then for loss−.Source: §4.4 · p. 27
• Trustworthiness does not generally imply tolerance: ⊤ is vacuously trustworthy for Gp although Gp is not tolerant, and the dual case holds for ⊥ and Fp.Theorem 65 identifies these as false directions in the related biconditionals discussed from.Source: §4.4 · p. 27
• If A is tolerant, ⊤ is trustworthy for A with respect to loss; if A is permanent, ⊥ is trustworthy for A with respect to loss.These are the valid directions established in Theorem 66.Source: §4.4 · p. 27
• For A in LLTL, if D A and D¬A are both preserved under cor, exactly one of D A, D¬A, or both possible is valid.Theorem 67 gives an EDMon version of Theorem 11 in, combining syntactic and semantic reasoning.Source: §4.4 · p. 28

• EDMon makes comparison easier and makes the available options visible.Source: §5 · p. 28
• Some mistakes remain outside EDMon's scope.Source: §5 · p. 28
• EDMon is insufficiently expressive for many hyperproperties, which concern relations among sets of traces.Source: §5 · p. 28
• The scheme can extend monitorability beyond LTL; HyperLTL [9] is one basis for adding mutation modalities.Source: §5 · p. 28
• The HyperLTL sketch interprets existential trace quantification over some trace and universal quantification over every trace.Source: §5 · p. 28
• Coupling HyperLTL with the described techniques promises new ways to consider a broader palette of data-security concerns.Source: §5 · p. 29