arrow
Return

Hyper Pattern Matching

delete2026-01-01
delete0
PRE
AI
M
Masaki Waga *
É
Étienne André
DOI:10.1007/978-3-032-05435-7_22delete
deleteOriginal
deleteOriginal request for help
deleteShare
deleteSave
Abstract

Abstract

En 中文
In runtime verification, pattern matching, which searches for occurrences of a specific pattern within a word, provides more information than a simple violation detection of the monitored property, by locating concrete evidence of the violation. However, witnessing violations of some properties, particularly hyperproperties, requires evidence across multiple input words or different parts of the same word, which goes beyond the scope of conventional pattern matching. We propose here hyper pattern matching, a generalization of pattern matching over a set of words. Properties of interest include robustness and (non-)interference. As a formalism for patterns, we use nondeterministic asynchronous finite automata (NAAs). We first provide a naive algorithm for hyper pattern matching and then devise several heuristics for better efficiency. Although we prove the NP-completeness of the problem, our implementation HypPAu is able to address several case studies scalable in the length, number of words (or logs) and number of dimensions, suggesting the practical relevance of our approach.
Keywords:
runtime verification
hyperproperties
pattern matching

Journal

R
RUNTIME VERIFICATION, RV 2025
IF:
0
Papers:
27
Citations:
0

Organization

N
national institute of informatics (nii) - japan
Scholars:
453
Papers: 420
Citations: 0
K
kyoto university
Scholars:
7.6K
Papers: 3.0K
Citations: 0