pith. sign in

arxiv: 1906.12133 · v1 · pith:BWAGKJ2Inew · submitted 2019-06-28 · 💻 cs.FL

Online Quantitative Timed Pattern Matching with Semiring-Valued Weighted Automata

Pith reviewed 2026-05-25 13:36 UTC · model grok-4.3

classification 💻 cs.FL
keywords runtime verificationtimed pattern matchingweighted automataquantitative monitoringzone graphsemiringsonline algorithmscyber-physical systems
0
0 comments X

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.

The paper develops an online algorithm for quantitative timed pattern matching by representing specifications with timed symbolic weighted automata. Quantitative satisfaction is computed via shortest distances on a weighted variant of the zone graph using dynamic programming. This yields numerical measures of how well sub-signals satisfy the specification while processing the input incrementally. The approach is general because it works for any semiring and applies to runtime verification of cyber-physical systems where boolean verdicts are insufficient.

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

These are editorial extensions of the paper, not claims the author makes directly.

  • 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

Figures reproduced from arXiv: 1906.12133 by Masaki Waga.

Figure 1
Figure 1. Figure 1: Piecewise-constant signal σ (left) and an illustration of the quantitative matching function (M(σ, W))(t, t0 ) for [t, t0 ) ⊆ [0, 30.5) (right). In the right figure, the score in the white areas is −∞. The specification W is outlined in Example 1. In the right figure, the value at (3, 15) is 5. It shows that the score M(σ, W)  (3, 15), for the restriction σ [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example of a TSWA W = (A, κr) which is the pair of the TSA A (upper) and the cost function κr (lower). See Definition 5 for the precise definition. The right of [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Illustration of our online algorithm for quantitative timed pattern match [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: WSTTS S sym of the TSWA W in [PITH_FULL_IMAGE:figures/full_fig_p011_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Matching automaton Amatch for the TSA A shown in [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Overshoot: The set of input signals is generated by the cruise control model [cru]. The TSA is for the settling when the reference value of the velocity is changed from vref < 35 to vref > 35. The left and right maps are for the sup-inf and tropical semirings, respectively. rise > fall > > c1 < 20 c2 < 80 c1 < 20 c2 < 80 c1 < 20, c2 < 80 /c1 := 0 c1 < 20 c2 < 80 c1 < 20 c2 < 80 0 30 60 90120 t 0 30 60 90 t… view at source ↗
Figure 7
Figure 7. Figure 7: Ringing: The set of input signals is generated by the same model [cru] as that in Overshoot. The TSA is for the frequent rise and fall of the signal in 80 s. The constraints rise and fall are rise = v(t) − v(t − 10) > 10 and fall = v(t) − v(t − 10) < −10. The left and right maps are for the sup-inf and tropical semirings, respectively. vref < 35 |v − vref | < 10 vref > 35 |v − vref | > 10 > c < 10 > 450 55… view at source ↗
Figure 8
Figure 8. Figure 8: Overshoot (Unbounded): The set of input signals is generated by the same model [cru] as that in Overshoot. The TSA is almost the same as that in Overshoot, but the time-bound (c < 150) is removed. The left and right maps are for the sup-inf and tropical semirings, respectively. 0 20 40 60 80 100 120 140 0 1 2 3 4 5 6 Execution time [s] Number of entries of the signal [×10, 000] Overshoot, sup-inf Ringing s… view at source ↗
Figure 9
Figure 9. Figure 9: Change in execution time (left) and memory usage (right) for [PITH_FULL_IMAGE:figures/full_fig_p016_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Change in execution time (left) and memory usage (right) for [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Change in execution time (left) and memory usage (right) for [PITH_FULL_IMAGE:figures/full_fig_p017_11.png] view at source ↗
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.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

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)
  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

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback. We address the single major comment below.

read point-by-point responses
  1. 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

0 steps flagged

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

0 free parameters · 1 axioms · 1 invented entities

The central claim depends on the modeling power of timed symbolic weighted automata and the tractability of online shortest-distance computation on their zone graphs; these are introduced without external benchmarks or prior independent verification in the abstract.

axioms (1)
  • standard math Semiring operations are associative, commutative, and distributive in the standard algebraic sense.
    Required for the weighted automata and shortest-distance definitions to be well-formed.
invented entities (1)
  • timed symbolic weighted automata no independent evidence
    purpose: To encode quantitative timed specifications that support numeric satisfaction measures.
    New modeling formalism presented as the specification language for the monitoring problem.

pith-pipeline@v0.9.0 · 5729 in / 1299 out tokens · 32478 ms · 2026-05-25T13:36:35.665409+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [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

  2. [2]

    Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci. , 126(2):183--235, 1994

  3. [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

  4. [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

  5. [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...

  6. [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

  7. [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...

  8. [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

  9. [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...

  10. [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...

  11. [11]

    Henzinger, and Jan Otop

    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

  12. [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. [13]

    Data-driven adaptive safety monitoring using virtual subjects in medical cyber-physical systems: A glucose control case study

    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

  14. [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

  15. [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

  16. [16]

    Handbook of Weighted Automata

    Manfred Droste, Werner Kuich, and Heiko Vogler. Handbook of Weighted Automata . Springer Publishing Company, Incorporated, 1st edition, 2009

  17. [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...

  18. [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

  19. [19]

    Fainekos and George J

    Georgios E. Fainekos and George J. Pappas. Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. , 410(42):4262--4291, 2009

  20. [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

  21. [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

  22. [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

  23. [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

  24. [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...

  25. [25]

    Weighted Automata Algorithms , pages 213--254

    Mehryar Mohri. Weighted Automata Algorithms , pages 213--254. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009

  26. [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

  27. [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

  28. [28]

    Timed pattern matching

    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

  29. [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...

  30. [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

  31. [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...

  32. [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. [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

  34. [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

  35. [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...

  36. [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

  37. [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. [38]

    write newline

    " 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 ":" * " " *...