Pith. sign in

REVIEW 2 major objections 7 minor 67 references

RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics

T0 review · 2 major / 7 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read RTAMT compiles STL specifications into quantitative runtime monitors.

desk verdict A solid tool paper with a real public library; the dense-time monitoring needs an error bound or clearer sampling guidance, but the core STL monitoring claim holds. read the letter →

arxiv 2501.18608 v1 pith:WXMGLDBO submitted 2025-01-22 cs.LO cs.RO

Tomoya Yamaguchi , Bardh Hoxha , Dejan Nickovic This is my paper · ORCID
classification cs.LOcs.RO
keywords runtimeverificationSignalTemporalLogicrobustnessmonitoringonlinecyber-physicalsystemsroboticsROSSimulink
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper presents RTAMT, a library that turns Signal Temporal Logic (STL) specifications into quantitative monitors for real-valued signals. A monitor reports a real number at each step: positive when the requirement holds, negative when it is violated, with magnitude measuring how far the behavior is from the satisfaction boundary. The paper claims the library's architecture, centered on a Python API and a semantics layer that can be backed by C++ for speed, makes such monitors usable online in ROS and as Simulink blocks. If correct, a roboticist or control engineer can instrument a running system with formal specifications and get a live distance-to-failure measure without leaving the usual development environment.

What carries the argument

The carrying mechanism is the quantitative robustness semantics of STL, in which each operator is evaluated by min/max/inf/sup over the signal: a predicate contributes f(w(t)) − c, conjunction and disjunction become min and max, and timed operators become infima and suprema over time windows. The pastification operation rewrites any bounded-future STL formula into a past-only formula using an auxiliary precedes operator, which lets an online monitor postpone evaluation until the formula horizon and then update incrementally. Dense-time efficiency comes from sliding-window streaming algorithms for minima and maxima, adapted from offline to incremental online evaluation. IA-STL's output robustness and input vacuity are defined as a relative robustness that treats predicates over fixed variables as ±∞ and predicates over uncontrollable variables as zero.

What would settle it

Feed RTAMT's dense-time monitor the signal f(t)=t sampled only at t=0 and t=1, and evaluate the formula F[0,0.9](f > 0.5). Under the piecewise-constant interpretation the monitor reports negative robustness, because it sees f=0 throughout the window [0,0.9], while the true continuous-time signal satisfies the formula with positive robustness 0.1; observing this discrepancy would show the monitor does not reproduce continuous-time robustness for varying signals.

Watch

Extended reading notes

Core claim

The central claim is that one monitor-generation pipeline can serve discrete-time and dense-time interpretations of STL, online and offline modes, and an interface-aware variant (IA-STL), all behind a small API. The pipeline parses a specification, optionally pastifies bounded-future formulas into past-only form so that online evaluation waits only until the relevant horizon has arrived, then computes robustness by traversing the formula's syntax tree. Dense-time monitoring is event-driven and assumes signals are piecewise constant between samples; discrete-time monitoring is clock-driven with a fixed sampling period. The same evaluation routine is exposed as evaluate for offline use and update for online use, and the resulting robustness value can be published to a ROS topic or to a Simulink output port.

Load-bearing premise

The dense-time monitors assume every signal is constant between sample points, so a real signal that varies within a sampling interval can produce a robustness value different from the true continuous-time robustness, and the paper gives no error bound for that approximation.

Editorial extensions

If this is right

  • A ROS developer can attach a monitor node to the topics named in an STL annotation file and receive a live robustness signal, with bounded-future formulas automatically pastified for online use.
  • A Simulink engineer can insert a single S-function block that takes an array of signals and outputs a robustness trace, enabling sensitivity analysis and falsification during model-based development.
  • Because the monitor output is quantitative, it can serve as the objective for search-based test generation, not just as a yes/no verdict.
  • The separation of syntax and semantics means a new specification language or a new robustness notion can be added by extending only the parser rules or the predicate evaluation method, as demonstrated by the IA-STL extension.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A direction the paper leaves implicit is distributed monitoring: if every subsystem locally publishes its robustness, a system-level monitor could combine those values in an assume-guarantee fashion, which the paper names only as future work.
  • The piecewise-constant dense-time assumption means the reported robustness is an approximation for real continuous signals; a comparison against interpolation-based semantics or a formal error bound would tell practitioners how much they can trust the monitor on signals that change within a sampling interval.
  • The same engine could host other quantitative semantics, such as averaged or edit-distance variants, because only the operator evaluation methods would need to change; the author lists such variants as future plans rather than current claims.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 7 minor

Summary. The paper presents RTAMT, a Python library with a C++ backend for generating runtime robustness monitors from Signal Temporal Logic (STL) and Interface-Aware STL (IA-STL) specifications. It defines quantitative STL semantics over discrete-time and dense-time signals, describes a pastification procedure for bounded-future STL, and outlines the library architecture, API, and extension mechanism. The main practical contributions are integrations with ROS and MATLAB/Simulink, supported by scalability experiments and two case studies: an HSR robot simulator in ROS and an aircraft elevator control system in Simulink. The central claim is that a practitioner can write an STL/IA-STL formula, parse it in RTAMT, and obtain an online or offline robustness monitor in a CPS or robotics toolchain.

Significance. If the claims hold, RTAMT addresses a real integration gap between STL monitoring research and CPS/robotics development practice. The paper's strengths are its public repository, concrete code listings, reuse of independently published monitoring algorithms, explicit treatment of IA-STL, and the demonstrated ROS and Simulink integrations. The dense-time monitoring path, however, is built on a piecewise-constant signal assumption whose practical consequences are not quantified, so the advertised 'dense-time' monitoring of physical signals needs qualification. The theoretical content is largely standard; the novelty is architectural and experimental. The tool has clear value as a reusable artifact for runtime verification practitioners.

major comments (2)
  1. [Section 2.1, Section 3.2, Section 8] The dense-time monitoring path is defined only for piecewise-constant signals: Section 2.1 assumes 'for all t in [ti,ti+1) and x in X, w(x,t)=w(x,ti)', and Section 3.2 states that DenseTimeInterpreter uses piecewise-constant interpolation. The paper nevertheless presents RTAMT as measuring 'how far an observed signal is from satisfying or violating it' (Section 2) and targets CPS/robotics, where physical signals generally vary within a sampling interval. For such a signal, the computed value is the robustness of the piecewise-constant proxy, not of the observed continuous-time signal, and the two can differ by an amount comparable to the full signal amplitude. No error bound, no comparison with piecewise-linear interpolation, and no sampling-density guidance are provided; Section 8 restates the modeling premise but does not quantify its consequences. I recommend adding a quantitative error analysis under explicit signal-regularity assumptions, or a comparison of the piecewise-constant monitor with an alternative interpolation, or an explicit restriction of the dense-time claims to signals that are truly piecewise-constant.
  2. [Section 2.2, Definition 4] The pastification transformation is load-bearing for all online bfSTL monitors, including the ROS and Simulink integrations, but its key correctness statement is not fully supported. After Definition 4, the paper states 'Formally, we say that for an arbitrary bfSTL formula phi, signal w and time index t in N, rho(phi,w,t)=rho(Pi(phi),w,h(phi))'; the notation h(phi) is never defined (Definition 3 defines H(phi)), and no proof or precise theorem reference is given. The '↔' symbol in the until case of Definition 4 is also not the right relation for quantitative semantics. Please replace this with a precise statement of robustness preservation, add a proof sketch or point to the exact theorem in [9,10], and use '=' or '≡' rather than '↔'.
minor comments (7)
  1. [Section 2.1] The sentence 'For x in X maps a variable x to a real value' is grammatically incomplete and should be rewritten.
  2. [Figure 2(b)] The interval in the definition of the historically operator is written as (t-a, t-b], which is reversed for a<b; it should be (t-b, t-a] to match the standard semantics of S and H.
  3. [Section 6.1] The scalability experiments report only average computation times over 50 repetitions, with no variance, standard deviation, or box plots; since Figures 9 and 10 are the main performance evidence, please add a measure of spread or show individual runs.
  4. [Section 6.2] The HSR fault-localization experiment is based on a single injected planner fault with one simulation run; because the planner uses RRT, which is randomized, please state the number of runs and whether the qualitative conclusion was stable across seeds.
  5. [Listing 5, lines 11-12] The topic annotation for the output variable 'rob' is set to 'rtamt/gnt' in the listing, which appears to be a typo for 'rtamt/rob'.
  6. [Section 8] The phrase 'we assumed dense-time as a perfect continuous clock' is imprecise; the implementation assumes piecewise-constant signals between sample points, which is a sampled-hold model rather than a perfect continuous-time model.
  7. [Section 5] It would be helpful to state explicitly whether IA-STL classes are shipped in the library or only provided as an extension template; the AECS case study suggests built-in support, but the text of Section 5 reads as a how-to guide for implementing IA-STL.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a tool/implementation report whose algorithms are cited to prior published work, and its dense-time assumption is an explicitly stated modeling premise rather than a circular reduction.

full rationale

This is a systems/tool paper with no predictive claim that is fitted to data. The STL robustness semantics (Definition 2) are standard and are implemented directly, while the monitoring algorithms are credited to prior publications ([10], [13], [14]). Several of those citations involve author overlap ([9], [10], [14]), but the cited results are prior, independently published theorems and algorithms; they are not constructed from RTAMT's own outputs, and the paper does not use them to forbid alternatives or to justify an otherwise unsupported choice. The pastification correctness statement in Section 2.2 is taken from [9,10] as an external, checkable result rather than derived circularly from RTAMT. The dense-time monitors explicitly assume piecewise-constant signals in Section 2.1 and Section 3.2 states that the dense-time implementation follows that piecewise-constant interpretation; this is a clearly disclosed modeling assumption, not a definitional equivalence that manufactures the claimed result. The HSR and AECS case studies use RTAMT as a monitor and no parameter is fitted and then renamed as a prediction. No self-definitional step, fitted-input-called-prediction step, uniqueness-imported-from-authors step, ansatz-smuggled-via-citation step, or renaming of a known result was found. Accordingly, the appropriate finding is that there is no significant circularity.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper does not fit any parameters or introduce new physical entities. It relies on standard STL semantics plus three domain assumptions: piecewise-constant dense-time signals, correctness of the cited pastification procedure, and the usefulness of discrete-time sampling. These assumptions are reasonable for the intended applications, but they are load-bearing for the dense-time and online monitoring claims.

assumptions (3)
  • domain assumption Dense-time signals are piecewise-constant between sample points.
    Section 2.1 assumes signals take constant values on each interval [ti,ti+1); physical signals that vary within a sample interval can yield an incorrect robustness value from the dense-time monitor.
  • domain assumption The pastification procedure preserves the robustness value exactly.
    Section 2.2 relies on the equivalence rho(phi,w,t)=rho(Pi(phi),w,t+H(phi)) cited from [9,10]; the paper sketches the transformation but does not prove it.
  • domain assumption Discrete-time periodic sampling is a sound approximation of dense-time semantics.
    Section 3.2 adopts discrete-time monitoring because of [12], which shows that weakening/strengthening real-time specifications preserves properties of dense-time interpretation; this background result is not proved in the paper.

how reviews work

0 comments
Cite this review

Pith. "Pith review of RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics." pith.science (2026). https://pith.science/paper/WXMGLDBO

@misc{pith2026250118608,
  author       = {Pith},
  title        = {Pith review of: RTAMT -- Runtime Robustness Monitors with Application to CPS and Robotics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/WXMGLDBO}},
  note         = {Machine review of arXiv:2501.18608}
}
read the original abstract

In this paper, we present Real-Time Analog Monitoring Tool (RTAMT), a tool for quantitative monitoring of Signal Temporal Logic (STL) specifications. The library implements a flexible architecture that supports: (1) various environments connected by an Application Programming Interface (API) in Python, (2) various flavors of temporal logic specification and robustness notion such as STL, including an interface-aware variant that distinguishes between input and output variables, and (3) discrete-time and dense-time interpretation of STL with generation of online and offline monitors. We specifically focus on robotics and Cyber-Physical Systems (CPSs) applications, showing how to integrate RTAMT with (1) the Robot Operating System (ROS) and (2) MATLAB/Simulink environments. We evaluate the tool by demonstrating several use scenarios involving service robotic and avionic applications.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

67 extracted references · 60 canonical work pages

  1. [1]

    Lee, E.A., Seshia, S.A.: Introduction to embedded systems: A cyber-physical systems approach (2016)

    work page 2016

  2. [2]

    Mitra, S.: Verifying cyber-physical systems: A path to safe autonomy (2021)

    work page 2021

  3. [3]

    Alur, R.: Principles of cyber-physical systems (2015)

    work page 2015

  4. [4]

    In: ICRA Workshop on Open Source Software, vol

    Quigley, M., Conley, K., Gerkey, B., Faust, J., Foote, T., Leibs, J., Wheeler, R., Ng, A.Y.: Ros: an open-source robot operating system. In: ICRA Workshop on Open Source Software, vol. 3, p. 5 (2009). Kobe, Japan

    work page 2009

  5. [5]

    IEEE Software (4), 20–28 (2001)

    Sha, L.: Using simplicity to control complex- ity. IEEE Software (4), 20–28 (2001)

    work page 2001

  6. [6]

    Maler, O., Nickovic, D.: Monitoring tem- poral properties of continuous signals. In: Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Mod- elling and Analysis of Timed Systems, FOR- MATS 2004 and Formal Techniques in Real- Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France...

    work page 2004

  7. [7]

    In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Mon- treal, QC, Canada, April 16-18, 2019, pp

    Ferr` ere, T., Nickovic, D., Donz´ e, A., Ito, H., RTAMT 23 Kapinski, J.: Interface-aware signal tempo- ral logic. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2019, Mon- treal, QC, Canada, April 16-18, 2019, pp. 57–66 (2019)

    work page 2019

  8. [8]

    In: Auto- mated Technology for Verification and Anal- ysis - 18th International Symposium, ATV A 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, pp

    Nickovic, D., Yamaguchi, T.: RTAMT: online robustness monitors from STL. In: Auto- mated Technology for Verification and Anal- ysis - 18th International Symposium, ATV A 2020, Hanoi, Vietnam, October 19-23, 2020, Proceedings, pp. 564–571 (2020). https://do i.org/10.1007/978-3-030-59152-6 34. https: //doi.org/10.1007/978-3-030-59152-6 34

    doi:10.1007/978-3-030-59152-6 2020

Show all 67 references
  1. [9]

    In: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp

    Maler, O., Nickovic, D., Pnueli, A.: On syn- thesizing controllers from bounded-response properties. In: Computer Aided Verification, 19th International Conference, CA V 2007, Berlin, Germany, July 3-7, 2007, Proceedings, pp. 95–107 (2007)

    2007

  2. [10]

    Jaksic, S., Bartocci, E., Grosu, R., Kloib- hofer, R., Nguyen, T., Nickovic, D.: From signal temporal logic to FPGA monitors. In: 13. ACM/IEEE International Conference on Formal Methods and Models for Code- sign, MEMOCODE 2015, Austin, TX, USA, September 21-23, 2015, pp. 218–2...

    2015

  3. [11]

    Parr, T.: The definitive antlr 4 reference (2013)

    2013

  4. [12]

    545–558 (1992)

    Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Interna- tional Colloquium on Automata, Languages, and Programming, pp. 545–558 (1992). Springer

    1992

  5. [13]

    In: Com- puter Aided Verification (CA V), pp

    Donz´ e, A., Ferr` ere, T., Maler, O.: Effi- cient robust monitoring for STL. In: Com- puter Aided Verification (CA V), pp. 264–279 (2013)

    2013

  6. [14]

    In: Formal Modeling and Analysis of Timed Systems, 5th International Conference, FOR- MATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, pp

    Nickovic, D., Maler, O.: AMT: A property- based monitoring tool for analog systems. In: Formal Modeling and Analysis of Timed Systems, 5th International Conference, FOR- MATS 2007, Salzburg, Austria, October 3-5, 2007, Proceedings, pp. 304–319 (2007)

    2007

  7. [15]

    In: 2020 18th ACM-IEEE Interna- tional Conference on Formal Methods and Models for System Design (MEMOCODE), pp

    Yamaguchi, T., Hoxha, B., Prokhorov, D., Deshmukh, J.V.: Specification-guided soft- ware fault localization for autonomous mobile systems. In: 2020 18th ACM-IEEE Interna- tional Conference on Formal Methods and Models for System Design (MEMOCODE), pp. 1–12 (2020). IEEE

    2020

  8. [16]

    ROBOMECH Journal 6(1), 4 (2019)

    Yamamoto, T., Terada, K., Ochiai, A., Saito, F., Asahara, Y., Murase, K.: Development of human support robot as the research platform of a domestic mobile manipulator. ROBOMECH Journal 6(1), 4 (2019)

    2019

  9. [17]

    In: IEEE/RSJ International Conference on Intelligent Robots and Sys- tems, Sendai, Japan, pp

    Koenig, N., Howard, A.: Design and use paradigms for gazebo, an open-source multi- robot simulator. In: IEEE/RSJ International Conference on Intelligent Robots and Sys- tems, Sendai, Japan, pp. 2149–2154 (2004)

    2004

  10. [18]

    : Autonomous driving in urban environments: Boss and the urban challenge

    Urmson, C., Anhalt, J., Bagnell, D., Baker, C., Bittner, R., Clark, M., Dolan, J., Dug- gins, D., Galatali, T., Geyer, C., et al. : Autonomous driving in urban environments: Boss and the urban challenge. Journal of Field Robotics 25(8), 425–466 (2008)

    2008

  11. [19]

    Thrun, S., Burgard, W., Fox, D.: Probabilis- tic robotics (2005)

    2005

  12. [20]

    In: International Confer- ence on Robotics and Automation (2010)

    Marder-Eppstein, E., Berger, E., Foote, T., Gerkey, B., Konolige, K.: The office marathon: Robust navigation in an indoor office environment. In: International Confer- ence on Robotics and Automation (2010)

    2010

  13. [21]

    In: Proceedings 2000 ICRA

    Kuffner, J.J., LaValle, S.M.: Rrt-connect: An efficient approach to single-query path plan- ning. In: Proceedings 2000 ICRA. Millennium Conference. IEEE International Conference on Robotics and Automation. Symposia Pro- ceedings (Cat. No. 00CH37065), vol. 2, pp. 995–1001 (2000). IEEE

    2000

  14. [22]

    In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp

    Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp. 46–57 (1977). ieee

    1977

  15. [23]

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications. In: Formal Approaches to Software Testing and Runtime 24 RTAMT Verification, First Combined International Workshops, F ATES 2006 and R V 2006, Seat- tle, W A, USA, August 15-16, 2006, Revised Selected P...

    2006

  16. [24]

    Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous- time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009). https://doi.org/10.1016/j. tcs.2009.06.021

    2009 doi

  17. [25]

    In: Formal Modeling and Analysis of Timed Systems (FORMATS), pp

    Donz´ e, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 92–106 (2010)

    2010

  18. [26]

    In: 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), pp

    Abbas, H., Mittelmann, H., Fainekos, G.: Formal property verification in a confor- mance testing framework. In: 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 155–164 (2014). IEEE

    2014

  19. [27]

    In: Computer Aided Verification, 27th International Conference, CA V 2015, San Francisco, CA, USA, July 18-24, 2011, Proceedings (2015 (to appear))

    Akazaki, T., Tasuo, I.: Time robustness in MTL and expressivity in hybrid system fal- sification. In: Computer Aided Verification, 27th International Conference, CA V 2015, San Francisco, CA, USA, July 18-24, 2011, Proceedings (2015 (to appear))

    2015

  20. [28]

    Annpureddy, Y., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: A tool for temporal logic falsification for hybrid sys- tems. In: Tools and Algorithms for the Con- struction and Analysis of Systems - 17th International Conference, TACAS 2011, Held as Part of the Joint...

    2011

  21. [29]

    In: Computer Aided Verification, 22nd Inter- national Conference, CA V 2010, Edinburgh, UK, July 15-19, 2010

    Donz´ e, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Computer Aided Verification, 22nd Inter- national Conference, CA V 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pp. 167– 170 (2010)

    2010

  22. [30]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp

    Havelund, K., Ro¸ su, G.: Synthesizing mon- itors for safety properties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 342–356 (2002). Springer

    2002

  23. [31]

    In: Proc

    Reinbacher, T., F¨ ugger, M., Brauer, J.: Real- time runtime verification on chip. In: Proc. of R V 2012. LNCS, vol. 7687, pp. 110–125 (2013). https://doi.org/10.1007/978-3-642-3 5632-2-13

    2013 doi

  24. [32]

    Formal Methods in System Design 44(3), 230–239 (2014)

    Reinbacher, T., F¨ ugger, M., Brauer, J.: Run- time verification of embedded real-time sys- tems. Formal Methods in System Design 44(3), 230–239 (2014)

    2014

  25. [33]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp

    Reinbacher, T., Rozier, K.Y., Schumann, J.: Temporal-logic based runtime observer pairs for system health management of real- time systems. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 357–372 (2014). Springer

    2014

  26. [34]

    In: Runtime Verification - 16th International Conference, R V 2016, Madrid, Spain, September 23-30, 2016, Proceedings, pp

    Schumann, J., Moosbrugger, P., Rozier, K.Y.: Runtime analysis with R2U2: A tool exhibi- tion report. In: Runtime Verification - 16th International Conference, R V 2016, Madrid, Spain, September 23-30, 2016, Proceedings, pp. 504–509 (2016)

    2016

  27. [35]

    In: R V-CuBES 2017

    Rozier, K.Y., Schumann, J.: R2U2: tool overview. In: R V-CuBES 2017. An Interna- tional Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisa- tion for Runtime Verification Tools, Septem- ber 15, 2017, Seattle, W A, USA, pp. 138–156 (2017)

    2017

  28. [36]

    Hariharan, G., Kempa, B., Wongpiromsarn, T., Jones, P.H., Rozier, K.Y.: MLTL multi- type (MLTLM): A logic for reasoning about signals of different types. In: Software Verifi- cation and Formal Methods for ML-Enabled Autonomous Systems - 5th International Workshop, FoMLAS 2022,...

    2022

  29. [37]

    In: Runtime Verification 2002, R V 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002, pp

    Finkbeiner, B., Sankaranarayanan, S., Sipma, H.: Collecting statistics over runtime exe- cutions. In: Runtime Verification 2002, R V 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002, pp. 36–54 (2002). RTAMT 25 https://doi.org/10.1016/S1571-0661(04)805 76-0. https...

    2002 doi

  30. [38]

    In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pp

    D’Angelo, B., Sankaranarayanan, S., S´ anchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burli...

    2005

  31. [39]

    In: Runtime Verification: 16th International Conference, R V 2016, Madrid, Spain, September 23– 30, 2016, Proceedings, pp

    Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification lan- guage for network monitoring. In: Runtime Verification: 16th International Conference, R V 2016, Madrid, Spain, September 23– 30, 2016, Proceedings, pp. 152–168 (2016). Springer

    2016

  32. [40]

    arXiv preprint arXiv:1711.03829 (2017)

    Faymonville, P., Finkbeiner, B., Schwenger, M., Torfah, H.: Real-time stream-based monitoring. arXiv preprint arXiv:1711.03829 (2017)

    2017 arXiv

  33. [41]

    In: Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26– 30, 2018, Proceedings 21, pp

    Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: Tessla: temporal stream-based specification language. In: Formal Methods: Foundations and Applications: 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26– 30, 2018, Proceedings 21...

    2018

  34. [42]

    In: Runtime Verification: 18th Inter- national Conference, R V 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings 18, pp

    Gorostiaga, F., S´ anchez, C.: Striver: Stream runtime verification for real-time event- streams. In: Runtime Verification: 18th Inter- national Conference, R V 2018, Limassol, Cyprus, November 10–13, 2018, Proceedings 18, pp. 282–298 (2018). Springer

    2018

  35. [43]

    In: International Conference on Runtime Ver- ification, pp

    Dokhanchi, A., Hoxha, B., Fainekos, G.: On- line monitoring for temporal logic robustness. In: International Conference on Runtime Ver- ification, pp. 231–246 (2014). Springer

    2014

  36. [44]

    For- mal Methods in System Design 51(1), 5–30 (2017)

    Deshmukh, J.V., Donz´ e, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. For- mal Methods in System Design 51(1), 5–30 (2017)

    2017

  37. [45]

    IEEE Trans

    Mamouras, K., Wang, Z.: Online signal mon- itoring with bounded lag. IEEE Trans. Com- put. Aided Des. Integr. Circuits Syst. 39(11), 3868–3880 (2020). https://doi.org/10.1109/ TCAD.2020.3013053

    2020

  38. [46]

    IEEE Trans

    Jaksic, S., Bartocci, E., Grosu, R., Nick- ovic, D.: An algebraic framework for runtime verification. IEEE Trans. on CAD of Inte- grated Circuits and Systems 37(11), 2233– 2243 (2018). https://doi.org/10.1109/TCAD .2018.2858460

    2018

  39. [47]

    Mamouras, K., Chattopadhyay, A., Wang, Z.: Algebraic quantitative semantics for effi- cient online temporal monitoring. In: Tools and Algorithms for the Construction and Analysis of Systems - 27th International Con- ference, TACAS 2021, Held as Part of the European Joint Confe...

    2021

  40. [48]

    Journal of ACM 49(2), 172–206 (2002)

    Asarin, E., Caspi, P., Maler, O.: Timed reg- ular expressions. Journal of ACM 49(2), 172–206 (2002)

    2002

  41. [49]

    In: Logic in Computer Science (LICS), pp

    Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Logic in Computer Science (LICS), pp. 160–171 (1997)

    1997

  42. [50]

    In: Formal Model- ing and Analysis of Timed Systems (FOR- MATS), pp

    Ulus, D., Ferr` ere, T., Asarin, E., Maler, O.: Timed pattern matching. In: Formal Model- ing and Analysis of Timed Systems (FOR- MATS), pp. 222–236 (2014)

    2014

  43. [51]

    Ulus, D., Ferr` ere, T., Asarin, E., Maler, O.: Online timed pattern matching using deriva- tives. In: Tools and Algorithms for the Con- struction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and ...

    2016

  44. [52]

    In: Computer Aided Ver- ification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 26 RTAMT 2017, Proceedings, Part I, pp

    Ulus, D.: Montre: A tool for monitoring timed regular expressions. In: Computer Aided Ver- ification - 29th International Conference, CA V 2017, Heidelberg, Germany, July 24-28, 26 RTAMT 2017, Proceedings, Part I, pp. 329–335 (2017)

    2017

  45. [53]

    IEEE Trans

    Waga, M., Hasuo, I.: Moore-machine filter- ing for timed and untimed pattern matching. IEEE Trans. on CAD of Integrated Circuits and Systems 37(11), 2649–2660 (2018)

    2018

  46. [54]

    In: Formal Modeling and Analysis of Timed Systems - 15th Interna- tional Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pp

    Waga, M., Hasuo, I., Suenaga, K.: Efficient online timed pattern matching by automata- based skipping. In: Formal Modeling and Analysis of Timed Systems - 15th Interna- tional Conference, FORMATS 2017, Berlin, Germany, September 5-7, 2017, Proceedings, pp. 224–243 (2017)

    2017

  47. [55]

    In: 3rd Work- shop on Monitoring and Testing of Cyber- Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pp

    Waga, M., Hasuo, I., Suenaga, K.: MONAA: A tool for timed pattern matching with automata-based acceleration. In: 3rd Work- shop on Monitoring and Testing of Cyber- Physical Systems, MT@CPSWeek 2018, Porto, Portugal, April 10, 2018, pp. 14–15 (2018)

    2018

  48. [56]

    Technical report, SAE Technical Paper (2016)

    Kapinski, J., Jin, X., Deshmukh, J., Donze, A., Yamaguchi, T., Ito, H., Kaga, T., Kobuna, S., Seshia, S.: St-lib: A library for specifying and classifying model behav- iors. Technical report, SAE Technical Paper (2016)

    2016

  49. [57]

    Technical report, United States

    Najm, W.G., Smith, J.D., Yanagisawa, M., et al.: Pre-crash scenario typology for crash avoidance research. Technical report, United States. National Highway Traffic Safety Administration (2007)

    2007

  50. [58]

    In: International Conference on Computer Safety, Reliability, and Security, pp

    Koopman, P., Osyk, B., Weast, J.: Autonomous vehicles meet the physical world: Rss, variability, uncertainty, and prov- ing safety. In: International Conference on Computer Safety, Reliability, and Security, pp. 245–253 (2019). Springer

    2019

  51. [59]

    In: Proceedings of the 17th ACM-IEEE Inter- national Conference on Formal Methods and Models for System Design, pp

    Hekmatnejad, M., Yaghoubi, S., Dokhanchi, A., Amor, H.B., Shrivastava, A., Karam, L., Fainekos, G.: Encoding and monitoring responsibility sensitive safety rules for auto- mated vehicles in signal temporal logic. In: Proceedings of the 17th ACM-IEEE Inter- national Conference ...

    2019

  52. [60]

    arXiv preprint arXiv:1902.04245 (2019)

    Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez-Chanlatte, M., Seshia, S.A.: Verifai: A toolkit for the design and analysis of artificial intelligence-based systems. arXiv preprint arXiv:1902.04245 (2019)

    2019 arXiv

  53. [61]

    : Lgsvl simula- tor: A high fidelity simulator for autonomous driving

    Rong, G., Shin, B.H., Tabatabaee, H., Lu, Q., Lemke, S., Moˇ zeiko, M., Boise, E., Uhm, G., Gerow, M., Mehta, S., et al. : Lgsvl simula- tor: A high fidelity simulator for autonomous driving. In: 2020 IEEE 23rd International Conference on Intelligent Transportation Sys- tems (...

    2020

  54. [62]

    arXiv preprint arXiv:2109.13602 (2021)

    Vitelli, M., Chang, Y., Ye, Y., Wo lczyk, M., Osi´ nski, B., Niendorf, M., Grimmett, H., Huang, Q., Jain, A., Ondruska, P.: Safetynet: Safe planning for real-world self-driving vehi- cles using machine-learned policies. arXiv preprint arXiv:2109.13602 (2021)

    2021 arXiv

  55. [63]

    arXiv preprint arXiv:1903.06758 (2019)

    Liu, C., Arnon, T., Lazarus, C., Barrett, C., Kochenderfer, M.J.: Algorithms for ver- ifying deep neural networks. arXiv preprint arXiv:1903.06758 (2019)

    2019 arXiv

  56. [64]

    In: 2018 IEEE Intel- ligent Vehicles Symposium (IV), pp

    Tuncali, C.E., Fainekos, G., Ito, H., Kapinski, J.: Simulation-based adversarial test genera- tion for autonomous vehicles with machine learning components. In: 2018 IEEE Intel- ligent Vehicles Symposium (IV), pp. 1555– 1562 (2018). IEEE

    2018

  57. [65]

    In: 2020 International Conference on Embedded Software (EMSOFT), pp

    Date, Y., Baba, T., Hoxha, B., Yamaguchi, T., Prokhorov, D.: Application of simulation- based methods on autonomous vehicle con- trol with deep neural network: Work-in- progress. In: 2020 International Conference on Embedded Software (EMSOFT), pp. 1–3 (2020). IEEE

    2020

  58. [66]

    In: 2021 American Control Conference (ACC), pp

    Ghosh, S., Pant, Y.V., Ravanbakhsh, H., Seshia, S.A.: Counterexample-guided synthe- sis of perception models and control. In: 2021 American Control Conference (ACC), pp. 3447–3454 (2021). IEEE

    2021

  59. [67]

    arXiv preprint arXiv:1903.10033 (2019)

    Dreossi, T., Ghosh, S., Sangiovanni- Vincentelli, A., Seshia, S.A.: A formalization of robustness for deep neural networks. arXiv preprint arXiv:1903.10033 (2019)

    2019 arXiv

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.