Hyper pattern matching

Fuente: arXiv
Guardado en:
Detalles Bibliográficos
Autores principales: Waga, Masaki, André, Étienne
Formato: Preprint
Publicado: 2025
Materias:
Acceso en línea:
Etiquetas: Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
_version_ 1866908452839751680
author Waga, Masaki
André, Étienne
author_facet Waga, Masaki
André, Étienne
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2507_12102
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Hyper pattern matching
Waga, Masaki
André, Étienne
Formal Languages and Automata Theory
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.
title Hyper pattern matching
topic Formal Languages and Automata Theory
url https://arxiv.org/abs/2507.12102