Parametric Timed Pattern Matching
Masaki Waga, Étienne André, Ichiro Hasuo
TL;DR
This work addresses parametric timed pattern matching: identifying, for a concrete timed log, the intervals (t, t′) and parameter valuations v for which a timing specification holds on the log. It presents two frameworks: (i) a model-checking-based approach using parametric timed automata (PTAs) and reachability synthesis, and (ii) a dedicated online method (ParamMONAA) with skip-based optimizations to improve efficiency and enable runtime monitoring. The first approach provides general decidability via EF_synth and OptParamSynth, while the second delivers significant performance gains in practice through skipping techniques inspired by string matching. Experimental results on automotive-like benchmarks (Gear, Accel, Blowup, and OnlyTiming) show the dedicated method often far outperforms the model-checking route, though both enable online analysis and output rich parametric results. The work also introduces MakeSymbolic and TW2PTA constructions to transform the problem into a synchronized product whose parameter-synthesis yields the complete match set, and provides correctness and termination proofs alongside practical optimizations and future directions for expressivity and visualization of parametric matches.
Abstract
Given a log and a specification, timed pattern matching aims at exhibiting for which start and end dates a specification holds on that log. For example, "a given action is always followed by another action before a given deadline". This problem has strong connections with monitoring real-time systems. We address here timed pattern matching in the presence of an uncertain specification, i.e., that may contain timing parameters (e.g., the deadline can be uncertain or unknown). We want to know for which start and end dates, and for what values of the timing parameters, a property holds. For instance, we look for the minimum or maximum deadline (together with the corresponding start and end dates) for which the property holds. We propose two frameworks for parametric timed pattern matching. The first one is based on parametric timed model checking. In contrast to most parametric timed problems, the solution is effectively computable. The second one is a dedicated method; not only we largely improve the efficiency compared to the first method, but we further propose optimizations with skipping. Our experiment results suggest that our algorithms, especially the second one, are efficient and practically relevant.