Runtime Semantic Discovery for Evolving Action Alphabets

1 Introduction

• Fixed-alphabet monitors can become obsolete when updates, reconfigurations, or architectural changes alter observable actions despite unchanged functional intent.Frequent adaptation with limited human supervision makes manually revising specifications or rebuilding models costly or slow.Source: §1 · p. 1
• The approach infers possible semantic continuity from actions’ local trace contexts, then defines a hierarchy of k-neighbor equivalences as a runtime-computable comparison criterion.It is intended as a practical structural invariant, not a replacement for trace equivalence or bisimulation.Source: §1 · p. 1
• The framework targets alphabet evolution such as action renaming, splitting, and fusing, using neighbor preservation as evidence of a shared monitoring-relevant role.The aim is candidate correspondence, not full semantic equivalence.Source: §1 · p. 1
• The paper’s contributions include local action similarity generalized to k-neighbor equivalence and an abstraction framework for comparing systems with different observable alphabets.The framework captures renaming, splitting, fusing, and more general many-to-many mappings.Source: §1 · p. 2
• Neighbor-based equivalence is framed as a source of candidate mappings that can support monitor and specification adaptation, rather than a complete characterization of behavioral preservation.The paper aims to isolate what can be inferred incrementally and online from observed execution context.Source: §1 · p. 2

2 Motivating Example

• The Secure Information Retrieval example monitors that messages are encrypted before being sent, with Encryptor marking the encryption step.After component replacement, the system may expose CryptoEngine instead, requiring the specification’s action to change.Source: §2 · p. 2
• Changing Encryptor to CryptoEngine can leave the original monitor unable to recognize the action associated with the same functional intent.The example updates the LTL requirement by substituting CryptoEngine for Encryptor.Source: §2 · p. 2
• The motivating question is whether runtime monitoring can identify same-role actions across one-to-many or many-to-one changes without rebuilding a full behavioral model.The proposed intuition is to compare local contexts in execution traces.Source: §2 · p. 2

3.1 Incremental and adaptive verification

• Incremental verification reuses prior verification effort after system changes, whereas this work assumes only runtime action streams and uses local trace regularities rather than source changes or global models.The compared incremental approaches may rely on modular encapsulation, anticipated changes, or syntax-driven comparison [3] [17].Source: §3.1 · p. 2

3.2 Runtime verification under variation

• Existing runtime-verification approaches address richer action domains or externally specified updates, but do not infer correspondences between evolving action labels directly from runtime observations.Register-automata approaches still assume a known monitoring structure [12], while adaptive updates typically assume the transformation is known.Source: §3.2 · pp. 2–3

3.3 Behavioural equivalences and action refinement

• Global behavioral equivalences compare overall behavior, whereas action refinement is typically top-down and design-time; this work instead reconstructs candidate action correspondences at runtime from observed trace contexts rather than predefined relations.Source: §3.3 · p. 3

3.4 Process mining and evolution-aware monitoring

• Process mining reconstructs models from logs, whereas this approach restricts itself to local context that can be extracted incrementally and used online.That restriction sacrifices expressive power but better fits runtime-verification constraints; version-transition methods instead assume a suitable new specification is available.Source: §3.4 · p. 3
• The paper positions its contribution as an orthogonal, runtime-computable criterion for relating actions across alphabet evolution to support monitoring continuity.It addresses the earlier problem of recovering plausible action-vocabulary correspondences when no new specification is yet available.Source: §3.4 · p. 3

4 Methodology

• The method compares preceding and following trace contexts to identify plausible monitoring-relevant correspondences without reconstructing a global model.Similar contexts make an updated action a plausible, not proven, match for a previously known action.Source: §4 · p. 4
• The criterion supplies evidence for candidate correspondences, not proof of strong semantic sameness or full behavioural equivalence.It can be applied incrementally to observed traces without knowing the transformation that produced the updated system.Source: §4 · p. 4
• The framework targets renaming, replacement by alternatives (splitting), abstraction of multiple actions into one (fusing), sequence refinement, and multi-mapping.These are conceptual evolution classes, not correspondences assumed to be known at runtime.Source: §4 · p. 4
• The framework formalizes trace-neighbour contexts and k-neighbour contexts to compare systems with equal or partially different observable alphabets.The evolution classes identify intended scenarios; they do not themselves define action correspondences.Source: §4 · p. 4

5 Neighbour Equivalence

• Over finite LTS traces, each action is characterized by its immediate predecessor and successor contexts, with the representation retaining each action’s own context set.The action-to-context association matters because collapsing contexts into an unlabelled union would lose the central action’s identity.Source: §5 · p. 5
• Trace equivalence implies neighbour equivalence, but not conversely: immediate contexts can hide repeated-block lengths and long-range dependencies.The examples show that systems can have the same neighbour sets but different trace languages.Source: §5 · p. 5
• The k-neighbour equivalences form a strict hierarchy: agreement at k+1 implies agreement at k, while the reverse can fail at every level.Projection from wider windows yields narrower contexts; extending the repeated-block construction witnesses strictness.Source: §5 · p. 6
• For differing alphabets, maximal subtraces over unshared actions become atomic lifted tokens before abstraction, masking internal sequence length while preserving local structure.This supports sequence refinement, such as the example where action c is replaced by sequence ef.Source: §5 · pp. 6–7
• Equivalence modulo the abstraction requires matching abstract boundary contexts for unshared parts and matching local abstract contexts for shared actions.The two conditions compare systems while ignoring differences internal to unshared fragments.Source: §5 · p. 7

• Because both conditions hold, the example systems S0 and S3 are neighbour equivalent modulo μV.Source: §5 · p. 8
• Neighbour equivalence modulo μV covers renaming, splitting, fusing, and many-to-many correspondences, identifying locally functionally similar actions under the chosen abstraction.When behaviour is refined while functionality is maintained, refined actions may share a monitoring-relevant role; inferred correspondences can guide monitoring adaptation and continuity.Source: §5 · p. 8

6 Monitor and Specification Adaptation

• For pure renaming, replacing the old action with its correctly corresponding new action preserves its intended monitoring role.This claim assumes the alphabet change is observationally a pure renaming.Source: §6 · p. 8
• For splitting, a disjunction of new actions can substitute for the old action when they are alternative observable realizations of the same step.The heuristic is suited to actions monitored as witnesses of a system step; soundness depends on the formula’s occurrences of the old action.Source: §6 · p. 8
• Sequence adaptation expands an old action using LTL Next, but is restricted to cases where that action witnesses an abstract step.The passage cautions that this substitution is not strictly sound for arbitrary LTL formulas.Source: §6 · p. 8
• Fusing adaptation uses neighbour contexts to distinguish which old action a fused action represents, assuming the old actions had pairwise disjoint local contexts.It is a context-sensitive heuristic, not a generally sound translation for arbitrary LTL formulas.Source: §6 · p. 9
• Although the framework supports structural M-to-N mappings, a general LTL rule for them is non-trivial, so complex adaptations can be composed or guide manual rewriting.For cases where direct syntactic composition is not straightforward, neighbour compatibility narrows the plausible correspondences.Source: §6 · p. 9
• The framework is most naturally suited to direct translations such as renaming, splitting, and selected sequence expansions, while serving as a diagnostic guide for fusing and multi-mapping.The aim is to make manual updates more systematic and evidence-based, not to provide rigid fully automated translation for arbitrary alphabet changes.Source: §6 · pp. 8–9

7 Conclusions and Future Work

• Neighbour contexts provide local structural evidence for comparing systems with equal or partially different alphabets without reconstructing a global behavioural model.The approach includes neighbour equivalence and its k-neighbour generalisation, compared through abstraction.Source: §7 · p. 9
• Neighbour equivalence is strictly weaker than trace equivalence and supports candidate correspondences, while fusing generally needs semantic information beyond local neighbour preservation.The conclusion identifies renaming and controlled splitting as more natural applications.Source: §7 · p. 9
• The framework contributes trace-computable local equivalences and a runtime-friendly way to narrow possible monitor and specification adaptations as action vocabularies change.The paper relates the local equivalences precisely to stronger behavioural notions such as trace equivalence.Source: §7 · p. 9
• Future work includes adding frequencies or probabilistic profiles, identifying fragments with provably sound adaptation rules, and empirically evaluating cost and correspondence accuracy under imperfect traces.The paper reports that framework implementation has begun.Source: §7 · p. 9