Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata
Pith reviewed 2026-05-25 13:36 UTC · model grok-4.3
The pith
Timed symbolic weighted automata enable the first online quantitative timed pattern matching over semirings.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
The central claim is that quantitative timed pattern matching can be performed online for the first time by constructing timed symbolic weighted automata to encode the specifications and then applying shortest-distance computations on the corresponding weighted zone graph together with dynamic programming, all within a semiring framework that supports arbitrary quantitative measures.
What carries the argument
Timed symbolic weighted automata, which encode quantitative timed specifications, together with their weighted zone graphs whose shortest-path distances supply the quantitative verdicts via dynamic programming.
If this is right
- Quantitative satisfaction degrees become available incrementally before the entire signal arrives.
- The same algorithm applies to any semiring, supporting measures such as costs, probabilities, or other algebraic quantities.
- Experimental evaluation shows the method remains practical for specifications that include explicit time bounds.
- The combination of zone-graph shortest paths and dynamic programming yields an online monitor that returns verdicts on the fly.
Where Pith is reading between the lines
- The online property could support integration with control loops that react to partial satisfaction degrees rather than waiting for complete traces.
- Different semirings could be swapped to match domain-specific needs such as energy consumption or probabilistic reliability without changing the core algorithm.
- The tractability of the zone graph for a given automaton size and semiring would determine whether the method scales to larger systems.
Load-bearing premise
Any quantitative specification of interest can be represented by a timed symbolic weighted automaton whose weighted zone graph admits tractable shortest-distance computation in an online setting.
What would settle it
A concrete timed quantitative property for which no timed symbolic weighted automaton exists, or an input trace on which the weighted zone graph grows large enough to prevent real-time online processing.
Figures
read the original abstract
Monitoring of a signal plays an essential role in the runtime verification of cyber-physical systems. Qualitative timed pattern matching is one of the mathematical formulations of monitoring, which gives a Boolean verdict for each sub-signal according to the satisfaction of the given specification. There are two orthogonal directions of extension of the qualitative timed pattern matching. One direction on the result is quantitative: what engineers want is often not a qualitative verdict but the quantitative measurement of the satisfaction of the specification. The other direction on the algorithm is online checking: the monitor returns some verdicts before obtaining the entire signal, which enables to monitor a running system. It is desired from application viewpoints. In this paper, we conduct these two extensions, taking an automata-based approach. This is the first quantitative and online timed pattern matching algorithm to the best of our knowledge. More specifically, we employ what we call timed symbolic weighted automata to specify quantitative specifications to be monitored, and we obtain an online algorithm using the shortest distance of a weighted variant of the zone graph and dynamic programming. Moreover, our problem setting is semiring-based and therefore, general. Our experimental results confirm the scalability of our algorithm for specifications with a time-bound.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper claims to introduce the first quantitative and online timed pattern matching algorithm. It employs timed symbolic weighted automata (TSWA) to specify quantitative specifications and obtains an online algorithm via shortest-distance computation on a weighted variant of the zone graph combined with dynamic programming. The framework is semiring-based for generality across quantitative measures, and experimental results are reported to confirm scalability for time-bounded specifications.
Significance. If the central claims hold, the work would represent a notable contribution to runtime verification of cyber-physical systems by simultaneously extending qualitative timed pattern matching in both the quantitative and online directions. The semiring generality is a clear strength, as is the provision of experimental evidence for scalability. These elements support potential practical impact if the algorithmic details are fully justified.
major comments (1)
- [Abstract] Abstract and algorithm description: the claim that an online algorithm is obtained 'using the shortest distance of a weighted variant of the zone graph and dynamic programming' is load-bearing for the contribution, yet no complexity bound, argument for bounded zone growth in the incremental/online regime, or analysis of semiring operation costs is supplied. This leaves the modeling assumption that quantitative specifications can be faithfully and efficiently represented by TSWA unsupported.
Simulated Author's Rebuttal
We thank the referee for the careful reading and constructive feedback. We address the single major comment below.
read point-by-point responses
-
Referee: [Abstract] Abstract and algorithm description: the claim that an online algorithm is obtained 'using the shortest distance of a weighted variant of the zone graph and dynamic programming' is load-bearing for the contribution, yet no complexity bound, argument for bounded zone growth in the incremental/online regime, or analysis of semiring operation costs is supplied. This leaves the modeling assumption that quantitative specifications can be faithfully and efficiently represented by TSWA unsupported.
Authors: We agree that the current manuscript does not supply an explicit complexity bound, a formal argument for bounded zone growth under incremental/online processing, or an analysis of semiring operation costs. The algorithm is described via shortest-distance computation on the weighted zone graph combined with dynamic programming, and scalability is supported only by experiments on time-bounded specifications. We will add a new subsection to the algorithm section that (i) states the per-step complexity in terms of the number of zones and semiring operations, (ii) argues that time-bounded specifications keep the active zone set finite and incrementally manageable, and (iii) clarifies the representational assumptions on TSWA. These additions will be included in the revised version. revision: yes
Circularity Check
No circularity: algorithm is a direct construction from standard automata and graph techniques.
full rationale
The paper presents a new algorithm for quantitative online timed pattern matching by defining timed symbolic weighted automata and constructing an online monitor via shortest-distance computation on a weighted zone graph combined with dynamic programming over semirings. No equations, definitions, or claims in the provided text reduce any result to a fitted parameter, self-referential definition, or load-bearing self-citation chain; the derivation is self-contained against external benchmarks in automata theory and does not rename known results or smuggle ansatzes via citation.
Axiom & Free-Parameter Ledger
axioms (1)
- standard math Semiring operations are associative, commutative, and distributive in the standard algebraic sense.
invented entities (1)
-
timed symbolic weighted automata
no independent evidence
Reference graph
Works this paper leans on
-
[1]
A Kleene theorem for timed automata
Eugene Asarin, Paul Caspi, and Oded Maler. A Kleene theorem for timed automata. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997 , pages 160--171. IEEE Computer Society, 1997
work page 1997
-
[2]
Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci. , 126(2):183--235, 1994
work page 1994
-
[3]
Time robustness in MTL and expressivity in hybrid system falsification
Takumi Akazaki and Ichiro Hasuo. Time robustness in MTL and expressivity in hybrid system falsification. In Daniel Kroening and Corina S. Pasareanu, editors, Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II , volume 9207 of , pages 356--374. Springer, 2015
work page 2015
-
[4]
Offline timed pattern matching under uncertainty
\' E tienne Andr \' e , Ichiro Hasuo, and Masaki Waga. Offline timed pattern matching under uncertainty. In 23rd International Conference on Engineering of Complex Computer Systems, ICECCS 2018, Melbourne, Australia, December 12-14, 2018 , pages 10--20. IEEE Computer Society, 2018
work page 2018
-
[5]
Fainekos, and Sriram Sankaranarayanan
Yashwanth Annpureddy, Che Liu, Georgios E. Fainekos, and Sriram Sankaranarayanan. S-taliro: A tool for temporal logic falsification for hybrid systems. In Parosh Aziz Abdulla and K. Rustan M. Leino, editors, Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint European Con...
work page 2011
-
[6]
On the quantitative semantics of regular expressions over real-valued signals
Alexey Bakhirkin, Thomas Ferr \` e re, Oded Maler, and Dogan Ulus. On the quantitative semantics of regular expressions over real-valued signals. In FORMATS , volume 10419 of Lecture Notes in Computer Science , pages 189--206. Springer, 2017
work page 2017
-
[7]
Online timed pattern matching using automata
Alexey Bakhirkin, Thomas Ferr \` e re, Dejan Nickovic, Oded Maler, and Eugene Asarin. Online timed pattern matching using automata. In David N. Jansen and Pavithra Prabhakar, editors, Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Beijing, China, September 4-6, 2018, Proceedings , volume 11022 of Lecture Notes...
work page 2018
-
[8]
Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015
Ezio Bartocci and Rupak Majumdar, editors. Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings , volume 9333 of Lecture Notes in Computer Science . Springer, 2015
work page 2015
-
[9]
A decision tree approach to data classification using signal temporal logic
Giuseppe Bombara, Cristian Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka, and Calin Belta. A decision tree approach to data classification using signal temporal logic. In Alessandro Abate and Georgios E. Fainekos, editors, Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-1...
work page 2016
-
[10]
Timed automata: Semantics, algorithms and tools
Johan Bengtsson and Wang Yi. Timed automata: Semantics, algorithms and tools. In J \" o rg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Lectures on Concurrency and Petri Nets, Advances in Petri Nets [This tutorial volume originates from the 4th Advanced Course on Petri Nets, ACPN 2003, held in Eichst \" a tt, Germany in September 2003. In addi...
work page 2003
-
[11]
Krishnendu Chatterjee, Thomas A. Henzinger, and Jan Otop. Quantitative monitor automata. In Xavier Rival, editor, Static Analysis - 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings , volume 9837 of Lecture Notes in Computer Science , pages 23--38. Springer, 2016
work page 2016
-
[12]
https://github.com/tprasadtp/cruise-control-simulink
tprasadtp/cruise-control-simulink: Simulink model for Cruise control system of a car with dynamic road conditions . https://github.com/tprasadtp/cruise-control-simulink
-
[13]
Sanjian Chen, Oleg Sokolsky, James Weimer, and Insup Lee. Data-driven adaptive safety monitoring using virtual subjects in medical cyber-physical systems: A glucose control case study. JCSE , 10(3), 2016
work page 2016
-
[14]
Deshmukh, Alexandre Donz \' e , Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A
Jyotirmoy V. Deshmukh, Alexandre Donz \' e , Shromona Ghosh, Xiaoqing Jin, Garvit Juniwal, and Sanjit A. Seshia. Robust online monitoring of signal temporal logic. In Bartocci and Majumdar DBLP:conf/rv/2015 , pages 55--70
work page 2015
-
[15]
David L. Dill. Timing assumptions and verification of finite-state concurrent systems. In Joseph Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop, Grenoble, France, June 12-14, 1989, Proceedings , volume 407 of Lecture Notes in Computer Science , pages 197--212. Springer, 1989
work page 1989
-
[16]
Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata . Springer Publishing Company, Incorporated, 1st edition, 2009
work page 2009
-
[17]
Robust satisfaction of temporal logic over real-valued signals
Alexandre Donz \' e and Oded Maler. Robust satisfaction of temporal logic over real-valued signals. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, Formal Modeling and Analysis of Timed Systems - 8th International Conference, FORMATS 2010, Klosterneuburg, Austria, September 8-10, 2010. Proceedings , volume 6246 of Lecture Notes in Computer Scie...
work page 2010
-
[18]
Breach, A toolbox for verification and parameter synthesis of hybrid systems
Alexandre Donz \' e . Breach, A toolbox for verification and parameter synthesis of hybrid systems. In Tayssir Touili, Byron Cook, and Paul B. Jackson, editors, Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings , volume 6174 of Lecture Notes in Computer Science , pages 167--170. Springer, 2010
work page 2010
-
[19]
Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. , 410(42):4262--4291, 2009
work page 2009
-
[20]
Quantitative monitoring of STL with edit distance
Stefan Jaksic, Ezio Bartocci, Radu Grosu, Thang Nguyen, and Dejan Nickovic. Quantitative monitoring of STL with edit distance. Formal Methods in System Design , 53(1):83--112, 2018
work page 2018
-
[21]
An algebraic framework for runtime verification
Stefan Jaksic, Ezio Bartocci, Radu Grosu, and Dejan Nickovic. An algebraic framework for runtime verification. IEEE Trans. on CAD of Integrated Circuits and Systems , 37(11):2233--2243, 2018
work page 2018
-
[22]
A case study on runtime monitoring of an autonomous research vehicle (ARV) system
Aaron Kane, Omar Chowdhury, Anupam Datta, and Philip Koopman. A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In Bartocci and Majumdar DBLP:conf/rv/2015 , pages 102--117
work page 2015
-
[23]
St-lib: a library for specifying and classifying model behaviors
James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Alexandre Donze, Tomoya Yamaguchi, Hisahiro Ito, Tomoyuki Kaga, Shunsuke Kobuna, and Sanjit Seshia. St-lib: a library for specifying and classifying model behaviors. Technical report, SAE Technical Paper, 2016
work page 2016
-
[24]
Monitoring temporal properties of continuous signals
Oded Maler and Dejan Nickovic. Monitoring temporal properties of continuous signals. In Yassine Lakhnech and Sergio Yovine, editors, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tole...
work page 2004
-
[25]
Weighted Automata Algorithms , pages 213--254
Mehryar Mohri. Weighted Automata Algorithms , pages 213--254. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009
work page 2009
-
[26]
Efficient online monitoring of web-service slas
Franco Raimondi, James Skene, and Wolfgang Emmerich. Efficient online monitoring of web-service slas. In Mary Jean Harrold and Gail C. Murphy, editors, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008, Atlanta, Georgia, USA, November 9-14, 2008 , pages 170--180. ACM , 2008
work page 2008
-
[27]
On the definition of a family of automata
Marcel Paul Sch \" u tzenberger. On the definition of a family of automata. Information and Control , 4(2-3):245--270, 1961
work page 1961
-
[28]
Dogan Ulus, Thomas Ferr \` e re, Eugene Asarin, and Oded Maler. Timed pattern matching. In Axel Legay and Marius Bozga, editors, Formal Modeling and Analysis of Timed Systems - 12th International Conference, FORMATS 2014, Florence, Italy, September 8-10, 2014. Proceedings , volume 8711 of Lecture Notes in Computer Science , pages 222--236. Springer, 2014
work page 2014
-
[29]
Online timed pattern matching using derivatives
Dogan Ulus, Thomas Ferr \` e re, Eugene Asarin, and Oded Maler. Online timed pattern matching using derivatives. In Marsha Chechik and Jean - Fran c ois Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Sof...
work page 2016
-
[30]
Montre: A tool for monitoring timed regular expressions
Dogan Ulus. Montre: A tool for monitoring timed regular expressions. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I , volume 10426 of Lecture Notes in Computer Science , pages 329--335. Springer, 2017
work page 2017
-
[31]
Symbolic finite state transducers: algorithms and applications
Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bj rner. Symbolic finite state transducers: algorithms and applications. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012 , page...
work page 2012
-
[32]
Online parametric timed pattern matching with automata-based skipping
Masaki Waga and \' E tienne Andr \' e . Online parametric timed pattern matching with automata-based skipping. CoRR , abs/1903.07328, 2019
-
[33]
Symbolic monitoring against specifications parametric in time and data
Masaki Waga, \' E tienne Andr \' e , and Ichiro Hasuo. Symbolic monitoring against specifications parametric in time and data. In To appear in Proc. CAV'2019
work page 2019
-
[34]
A B oyer- M oore type algorithm for timed pattern matching
Masaki Waga, Takumi Akazaki, and Ichiro Hasuo. A B oyer- M oore type algorithm for timed pattern matching. In Martin Fr \" a nzle and Nicolas Markey, editors, Proceedings of the 14th International Conference on Formal Modeling and Analysis of Timed Systems ( FORMATS 2016) , volume 9884 of , pages 121--139. Springer, 2016
work page 2016
-
[35]
Efficient online timed pattern matching by automata-based skipping
Masaki Waga, Ichiro Hasuo, and Kohei Suenaga. Efficient online timed pattern matching by automata-based skipping. In Alessandro Abate and Gilles Geeraerts, editors, Formal Modeling and Analysis of Timed Systems - 15th International Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings , volume 10419 of Lecture Notes in Computer Scien...
work page 2017
-
[36]
MONAA: A tool for timed pattern matching with automata-based acceleration
Masaki Waga, Ichiro Hasuo, and Kohei Suenaga. MONAA: A tool for timed pattern matching with automata-based acceleration. In 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018 , pages 14--15. IEEE , 2018
work page 2018
-
[37]
, " * write output.state after.block = add.period write
ENTRY address author booktitle chapter doi edition editor eid howpublished institution journal key month note number organization pages publisher school series title type url volume year label INTEGERS output.state before.all mid.sentence after.sentence after.block FUNCTION init.state.consts #0 'before.all := #1 'mid.sentence := #2 'after.sentence := #3 '...
-
[38]
" write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION word.in bbl.in capitalize ":" * " " *...
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.