Pith. sign in

REVIEW 3 major objections 5 minor 31 references

ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics

T0 review · 3 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

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

Pith's one-line read ROSMonitoring 2.0 verifies services and ordered message traces for ROS

desk verdict Useful tool extension with a correct reordering proof that silently depends on unstated clock-comparability and unique-timestamp assumptions; service monitoring is the solid part, the evaluation is thin. read the letter →

arxiv 2411.14367 v1 pith:KT7DWJWJ submitted 2024-11-21 cs.SE cs.AIcs.RO

Maryam Ghaffari Saadat (University of Manchester) , Angelo Ferrando (University of Modena , Reggio Emilia) , Louise A. Dennis (University of Manchester) , Michael Fisher (University of Manchester) This is my paper · ORCID
classification cs.SEcs.AIcs.RO
keywords runtimeverificationROSROSMonitoringservicemonitoringmessageorderingtemporallogicroboticsoftwareUAVcasestudy
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

ROSMonitoring 2.0 claims to close two gaps in the original ROSMonitoring framework: it can monitor ROS services as well as topics, and it can deliver monitored messages to the verification oracle in the order they were published rather than the order they happened to arrive. The service extension inserts the monitor as a proxy between client and server, checking each request with the oracle before forwarding it and each response before returning it. The ordering extension buffers messages per topic and releases the one with the earliest publication timestamp once every topic buffer is non-empty, with a proof that this yields true publication order under the assumption that each topic delivers messages in publish order. A battery-supervisor case study on a fire-fighting UAV shows that unordered monitoring produces frequent false-negative verdicts on properties linking battery status to percentage readings and to LED-set service calls, while ordered monitoring produces accurate verdicts at the cost of added latency. The paper argues the extensions preserve the framework's separation between message interception and formalism-agnostic oracles, so existing specifications carry over unchanged.

What carries the argument

The load-bearing mechanism is Algorithm 1, a timestamp-buffered release rule. Each monitored topic t has a buffer; addToBuffer(msg,t) appends the message's publication timestamp to buffers[t] and stores the message in a global dictionary keyed by that timestamp, all under a lock. A sendEarliestMessageToOracle step runs as soon as no topic buffer is empty, picks the smallest timestamp across buffers, sends that message to the oracle, publishes the verdict, and removes the entry. The proof of Theorem 1 rests on Assumption 1 (per-topic arrival order equals publication order) plus the observation that a larger-timestamp message from another topic cannot be selected while a smaller-timestamp message waits in a different buffer. The same buffering discipline applies to service requests and responses, and the paper warns that ordering mutually dependent topics and services together can deadlock, illustrating the workaround in the case study by keeping /status_change unordered and carrying a status_change flag inside the ordered /battery_status messages.

What would settle it

Run two publisher nodes with known clock offsets (for instance, one clock set 10 seconds ahead) and record the true send order with an independent logger; if the oracle receives the cross-topic trace in a different order under Algorithm 1, then publication-order delivery depends on synchronized clocks. On the case-study side, replay the same recorded message trace through the monitor once with ordering enabled and once disabled and count verdict mismatches: the paper's claim is that the mismatch rate goes to zero for the properties in Table 1 when ordering is on.

Watch

Extended reading notes

Core claim

The central claim is a framework extension: ROSMonitoring 2.0 makes service calls first-class citizens of runtime monitoring for ROS and gives the oracle a publication-ordered view across multiple topics and services. For services the monitor acts as an intermediary: it receives the client's request, sends it to the oracle for a verdict, invokes the real service only on a positive verdict, then sends the response back to the oracle before delivering it to the client; a negative verdict on either side triggers an error message and blocks the call. For ordering, Algorithm 1 keeps one FIFO buffer per monitored topic, tags each message with its publication timestamp, and only releases a message to the oracle when every topic buffer holds at least one message, always choosing the smallest timestamp. Theorem 1 states that this release rule propagates the complete event trace in publication order, relying on Assumption 1 that messages on a single topic arrive in publish order. The case study demonstrates the practical payoff: without ordering, messages on /battery_status can reach the monitor before the /battery_percentage or /input_accepted messages they depend on, producing false negatives; with ordering, the verdicts match the intended properties, and the measured overhead is concentrated in the time service requests wait while earlier messages drain from other buffers.

Load-bearing premise

The load-bearing premise is that every topic delivers its messages to the monitor in the order they were published, and that the timestamps used to compare messages across topics are mutually comparable; if either fails, the earliest-timestamp release rule may present the oracle with events that did not actually happen in that order.

Editorial extensions

If this is right

  • Temporal properties ranging over both topics and services become checkable at runtime, so requirements like 'every LED update follows a legitimate battery-status change' can be verified automatically.
  • Existing ROSMonitoring oracles and formal specifications remain usable because the extension changes only monitor synthesis, not the oracle interface or the formalism-agnostic design.
  • Enabling ordering removes the false-negative verdicts observed on cross-topic and topic-service properties, making ordered monitoring the appropriate choice for safety-critical robotic applications.
  • The publication-ordered trace and the original receive-ordered trace can be compared to localize which node reordered events, supporting fault attribution rather than only violation detection.
  • The service-proxy pattern and the buffered-release ordering are reusable outside ROSMonitoring, as the paper notes, for other publish-subscribe systems with per-channel ordering guarantees.

Reading between the lines

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

  • If the timestamps read by getTime(msg) come from unsynchronized clocks on different publishers, then comparing them across topics does not recover true publication order; Theorem 1's conclusion would need an explicit clock-synchronization or logical-clock assumption.
  • The deadlock workaround in the case study suggests a general design rule: order only channels whose dependency graph is acyclic, since ordered channels that wait on each other's messages must not feed each other; this could be turned into a static analysis.
  • In sparse or lossy topics, waiting until every buffer is non-empty may stall the trace indefinitely; a timeout-based variant that trades occasional mis-ordering for liveness would be a natural test, and the paper itself lists timeouts as future work.
  • The same buffering scheme could extend to ROS 2 actions or other asynchronous request-response patterns, where ordering goals and response matching would follow the same proxy-and-buffer structure.
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

3 major / 5 minor

Summary. The paper presents ROSMonitoring 2.0, an extension of the ROSMonitoring runtime verification framework that adds two features: monitoring of ROS services (in addition to topics) and reordering of messages across topics and services according to publication time before they are sent to the verification oracle. The reordering is implemented by Algorithm 1, which buffers messages per topic and releases the message with the smallest timestamp once every buffer is non-empty. The paper states Assumption 1 (messages on a single topic arrive in publication order) and proves Lemma 1 and Theorem 1 claiming that the algorithm propagates messages to the oracle in publication order. The authors also describe a case study on a battery-supervisor UAV system, with properties expressed in Past MTL, showing that ordered monitoring avoids the false negatives that unordered monitoring produces, at the cost of increased latency. The service monitoring feature is also ported to ROS2.

Significance. If the correctness claim of Algorithm 1 holds under clearly stated assumptions, the work addresses a genuine problem in runtime verification of distributed robotic systems: cross-topic message interleaving. The service monitoring extension is practically useful and the framework is open source, which supports reproducibility. The paper is clearly written and the case study, while small, illustrates the value of the ordering mechanism. However, the central correctness theorem currently relies on unstated global clock-comparability and liveness assumptions, and the algorithm has a concrete equal-timestamp bug. These issues must be resolved before the central claim is fully established. The empirical evaluation is also too thin to support the accuracy claim quantitatively, but that is secondary to the algorithm's correctness.

major comments (3)
  1. [Section 4.2, Theorem 1 and Algorithm 1] The proof of Theorem 1 tacitly assumes that the values returned by getTime(msg) are globally comparable as publication times across all topics. The paper does not specify whether these are publisher-inserted header stamps, ROS time, or monitor-side receive timestamps. In a distributed ROS1 system, nodes do not have synchronized clocks by default; if timestamps originate from different node clocks, the minimum-timestamp selection rule can emit messages in timestamp order rather than publication order, contradicting the conclusion of Theorem 1. Please state the clock-domain assumption explicitly and either restrict the theorem to systems with a global clock or justify that the chosen timestamp source preserves publication order.
  2. [Section 4.2, Algorithm 1 (lines 10-12 and 3-5)] The global messages dictionary is keyed by timestamp alone. If two messages on different topics carry the same timestamp, the assignment messages[time_stamp_of_msg] = msg overwrites the earlier entry, so one message is lost while its timestamp remains in buffer[t]. The algorithm therefore mishandles equal timestamps, and the proof of Theorem 1 does not address this case. Use a composite key (e.g., timestamp plus topic) or define a tie-breaking rule, and update the proof accordingly.
  3. [Section 4.2 (deadlock discussion) and Section 5 (page 47)] The paper acknowledges that the ordering mechanism can deadlock and works around it in the case study by keeping /status_change unordered and by interrupting the execution to release remaining messages. This means the delivered trace can be incomplete if a buffer remains empty; the correctness claim of Theorem 1 implicitly assumes that all relevant messages are eventually buffered. The theorem should state the liveness condition under which it applies, and the case study should be described as best-effort ordering rather than guaranteed complete ordering.
minor comments (5)
  1. [Figure 5 caption] The caption contains a typo: 'ans /battery_status' should be 'and /battery_status'.
  2. [Table 2] The description for /battery_status lists '0' as a possible status value, but Section 5 uses statuses 1, 2, and 3 only; clarify this inconsistency.
  3. [Section 5, Property 3b description] The textual description 'Every /SetLED service request is followed by a /SetLED service request within 100 time steps' appears to be a typo; the formalization in Table 1 suggests the intended property concerns responses, not requests.
  4. [Section 5, Experimental evaluation] The accuracy comparison is based on 10 runs with no raw data or statistical significance test; please report the number of false negatives per run or provide the trace data to substantiate the qualitative claim.
  5. [Section 6, Related work] The statement that ROSRV 'does not support the verification of services or the customisation of the order of topics' should be supported by a specific reference or a direct citation to [19] to avoid unsupported claims.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the ordering theorem is an internal scheduler-correctness statement, not a fitted prediction or self-cited derivation.

full rationale

The paper's central technical claim is Theorem 1 in Section 4.2, which states that Algorithm 1 propagates messages to the Oracle in publication order. The proof is an internal consistency argument: by Assumption 1, messages on a single topic arrive in publication order, and by construction the algorithm releases the buffered message with the smallest publication timestamp. This does not reduce to a fitted parameter or to a circular self-citation; it is a standard priority-queue correctness argument. The genuinely questionable point is an unstated external condition: Algorithm 1 calls getTime(msg) and compares timestamps across topics, but the paper never states the clock domain of those timestamps. If they are publisher-inserted header stamps from unsynchronized clocks, the smallest-timestamp rule does not recover true cross-topic publication order. That is a correctness risk in the face of distributed ROS nodes, not a circularity, because the conclusion is not identical to the input assumption; the argument merely omits a needed comparability hypothesis. The paper also honestly flags its own limitations: it notes deadlock risks in Section 4.2, describes a workaround in the case study, and lists deadlock-freeness verification and timeouts as future work in Section 7. Self-citations such as [15] and [5] are background descriptions of the predecessor framework and formalism, not load-bearing derivations of the new results. There are no fitted parameters being called predictions and no renaming of a known result as a novel derivation. The ordering mechanism's guarantee is built into the algorithm's design, but that is an implementation property, not circular reasoning.

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

The central algorithm makes no fitted parameters; it relies on ROS communication assumptions (per-topic order) and on unstated timestamp comparability and uniqueness. The liveness assumption is acknowledged as a deadlock risk.

assumptions (4)
  • domain assumption Messages on each single topic arrive at subscribers in the order of publication (Assumption 1).
    Stated in Section 4.2 before Algorithm 1; used in Lemma 1 and Theorem 1 to ensure per-topic order.
  • domain assumption Timestamps are globally comparable across topics, i.e., publisher clocks are synchronized or the timestamps are all drawn from one clock domain.
    Implicit in Algorithm 1's use of the minimum timestamp across all buffers; not stated or justified in the paper, and necessary for the ordering to reflect true publication order.
  • domain assumption Timestamps of different messages are unique.
    Algorithm 1's messages dictionary uses the timestamp as the key (messages[time_stamp_of_msg] = msg); duplicate timestamps would silently overwrite messages, which is not discussed.
  • domain assumption All monitored topics eventually deliver at least one message so the while loop in addToBuffer makes progress.
    The release condition 'while no topic has an empty buffer' blocks indefinitely if a monitored topic goes silent; the paper acknowledges this deadlock risk and works around it in the case study, but does not make it a first-class assumption.

how reviews work

0 comments
Cite this review

Pith. "Pith review of ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics." pith.science (2026). https://pith.science/paper/KT7DWJWJ

@misc{pith2026241114367,
  author       = {Pith},
  title        = {Pith review of: ROSMonitoring 2.0: Extending ROS Runtime Verification to Services and Ordered Topics},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/KT7DWJWJ}},
  note         = {Machine review of arXiv:2411.14367}
}
read the original abstract

Formal verification of robotic applications presents challenges due to their hybrid nature and distributed architecture. This paper introduces ROSMonitoring 2.0, an extension of ROSMonitoring designed to facilitate the monitoring of both topics and services while considering the order in which messages are published and received. The framework has been enhanced to support these novel features for ROS1 -- and partially ROS2 environments -- offering improved real-time support, security, scalability, and interoperability. We discuss the modifications made to accommodate these advancements and present results obtained from a case study involving the runtime monitoring of specific components of a fire-fighting Uncrewed Aerial Vehicle (UAV).

Figures

Figures reproduced from arXiv: 2411.14367 by the authors.

Figure 1
Figure 1. High-level overview of ROSMonitoring [15]. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Motivating example with three components: Battery, Battery Supervisor, and LED Panel. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Service verification in ROSMonitoring 2.0 when filtering is enabled. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: Case study with ROS Monitor and additional topics [PITH_FULL_IMAGE:figures/full_fig_p010_4.png]
Figure 6
Figure 6. Figure 6: Mean and standard deviation of time (nanoseconds) taken for [PITH_FULL_IMAGE:figures/full_fig_p012_6.png]
Figure 5
Figure 5. Figure 5: Mean and standard deviation of time (nanoseconds) taken for monitor with ordering to buffer [PITH_FULL_IMAGE:figures/full_fig_p013_5.png]
Figure 7
Figure 7. Figure 7: Mean and standard deviation of time (nanoseconds) taken for monitor with ordering to buffer [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 19 canonical work pages

  1. [1]

    https://rsl.ethz.ch/ research/challenges-competitions/mbzirc2020.html

    MBZIRC 2020: The Mohamed Bin Zayed International Robotics Challenge . https://rsl.ethz.ch/ research/challenges-competitions/mbzirc2020.html. Accessed on April 8th, 2024

    work page 2020

  2. [2]

    https://www.ros.org/

    ROS: Robot Operating System. https://www.ros.org/. Accessed on April 8th, 2024

    work page 2024

  3. [3]

    Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza & Anna Ingólfsdóttir (2024): A Monitoring Tool for Linear-Time µHML. Sci. Comput. Program. 232, p. 103031. Available at https://doi.org/10.1016/j.scico.2023.103031

    arXiv 2024

  4. [4]

    In Davide Brugali, Jan F

    Sorin Adam, Morten Larsen, Kjeld Jensen & Ulrik Pagh Schultz (2014): Towards Rule-Based Dynamic Safety Monitoring for Mobile Robots . In Davide Brugali, Jan F. Broenink, Torsten Kroeger & Bruce A. MacDonald, editors: Proc. 4th International Conference on Simulation, Modeling, and Programming for Autonomous Robots (SIMPAR), Lecture Notes in Computer Scienc...

    work page doi:10.1007/978-3-319-11900-7_18 2014

  5. [5]

    Davide Ancona, Luca Franceschini, Angelo Ferrando & Viviana Mascardi (2021): RML: Theory and practice of a domain specific language for runtime verification . Sci. Comput. Program. 205, p. 102610, doi:10.1016/J.SCICO.2021.102610

    arXiv 2021

  6. [6]

    In Michael J

    Howard Barringer & Klaus Havelund (2011): TraceContract: A Scala DSL for Trace Analysis. In Michael J. Butler & Wolfram Schulte, editors: Proc. 17th International Symposium on Formal Methods (FM) , Lec- ture Notes in Computer Science 6664, Springer, pp. 57–72. Available at https://doi.org/10.1007/ 978-3-642-21437-0_7

    work page 2011

  7. [7]

    In Erika Ábrahám, Clemens Dubslaff & Silvia Lizeth Tapia Tarifa, editors: Proc

    Marian Johannes Begemann, Hannes Kallwies, Martin Leucker & Malte Schmitz (2023): TeSSLa-ROS- Bridge - Runtime Verification of Robotic Systems. In Erika Ábrahám, Clemens Dubslaff & Silvia Lizeth Tapia Tarifa, editors: Proc. 20th International Colloquium on Theoretical Aspects of Computing (ICTAC) , Lec- ture Notes in Computer Science 14446, Springer, pp. ...

    work page 2023

  8. [8]

    In: Proc

    Guido Breitenhuber (2020): Towards Application Level Testing of ROS Networks . In: Proc. Fourth IEEE International Conference on Robotic Computing (IRC) , IEEE, pp. 436–442. Available at https://doi. org/10.1109/IRC.2020.00081

    work page arXiv 2020

Show all 31 references
  1. [9]

    Maria A. S. Brito, Simone R. S. Souza & Paulo S. L. Souza (2022): Integration testing for robotic systems. Softw. Qual. J. 30(1), pp. 3–35. Available at https://doi.org/10.1007/s11219-020-09535-w

    2022 doi

  2. [10]

    In Nicolas Halbwachs & Lenore D

    Feng Chen & Grigore Rosu (2005): Java-MOP: A Monitoring Oriented Programming Environment for Java. In Nicolas Halbwachs & Lenore D. Zuck, editors: Proc. 11th International Conference on Tools and Algo- rithms for the Construction and Analysis of Systems (TACAS), held as Part o...

    2005 doi

  3. [11]

    Clarke, Orna Grumberg & Doron A

    Edmund M. Clarke, Orna Grumberg & Doron A. Peled (2001): Model checking . MIT Press, doi:10.1016/B978-044450813-3/50026-6. Available at http://books.google.de/books?id= Nmc4wEaLXFEC

    2001 doi

  4. [12]

    Sipma, Sandeep Mehrotra & Zohar Manna (2005): LOLA: Runtime Monitoring of Synchronous Systems

    Ben D’Angelo, Sriram Sankaranarayanan, César Sánchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra & Zohar Manna (2005): LOLA: Runtime Monitoring of Synchronous Systems. In: Proc. 12th International Symposium on Temporal Representation and Reasoning (TIME)...

    2005 doi

  5. [13]

    In Fumiya Iida, Perla Maiolino, Arsen Abdulali & Mingfeng Wang, editors: Proc

    Elif Degirmenci, Yunus Sabri Kirca, Özlem Örnek, Mert Bulut, Serhat Kahraman, Metin Ozkan & Ahmet Yazici (2023): Developing an Integrated Runtime Verification for Safety and Security of Industrial Robot Inspection System. In Fumiya Iida, Perla Maiolino, Arsen Abdulali & Mingfe...

    2023 doi

  6. [14]

    Seshia (2017): Combining Model Checking and Runtime Veri- fication for Safe Robotics

    Ankush Desai, Tommaso Dreossi & Sanjit A. Seshia (2017): Combining Model Checking and Runtime Veri- fication for Safe Robotics. In Shuvendu K. Lahiri & Giles Reger, editors:Proc. 17th International Conference on Runtime Verification (RV), Lecture Notes in Computer Science 1054...

    2017 doi

  7. [15]

    Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mas- cardi (2020): ROSMonitoring: A Runtime Verification Framework for ROS

    Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mas- cardi (2020): ROSMonitoring: A Runtime Verification Framework for ROS . In Abdelkhalick Mohammad, Xin Dong & Matteo Russo, editors: Proc. 21st Annual Conference on Towards Auton...

    2020 doi

  8. [16]

    Mohammed Foughali, Bernard Berthomieu, Silvano Dal-Zilio, Félix Ingrand & Anthony Mallet (2016): Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots . In Kazuhiro Ogata, Mark Lawford & Shaoying Liu, editors: Formal Methods and Software Engineering ...

    2016

  9. [17]

    Dimitra Giannakopoulou, Thomas Pressburger, Anastasia Mavridou, Julian Rhein, Johann Schumann & Nija Shi (2020): Formal Requirements Elicitation with FRET. In Mehrdad Sabetzadeh, Andreas V ogelsang, Sal- lam Abualhaija, Markus Borg, Fabiano Dalpiaz, Maya Daneva, Nelly Condori-...

    2020

  10. [18]

    In: Proc

    Klaus Havelund, Doron Peled & Dogan Ulus (2018): DejaVu: A Monitoring Tool for First-Order Temporal Logic. In: Proc. 3rd Workshop on Monitoring and Testing of Cyber-Physical Systems, MT@CPSWeek 2018, IEEE, pp. 12–13. Available at https://doi.org/10.1109/MT-CPS.2018.00013

    2018

  11. [19]

    Moore, Qingzhou Luo, Aravind Sundaresan & Grigore Rosu (2014): ROSRV: Runtime Verification for Robots

    Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon M. Moore, Qingzhou Luo, Aravind Sundaresan & Grigore Rosu (2014): ROSRV: Runtime Verification for Robots. In Borzoo Bonakdarpour & Scott A. Smolka, editors: Proc. 5th International Conference on Runtime Verification (RV), Lecture No...

    2014 doi

  12. [20]

    www.isp.uni-luebeck.de/lamaconv

    Institute for Software Engineering and Programming Languages: LamaConv - Logics and Automata Con- verter Library. www.isp.uni-luebeck.de/lamaconv

  13. [21]

    Gert Kanter & Jüri Vain (2020): Model-based testing of autonomous robots using TestIt . J. Reliab. Intell. Environ. 6(1), pp. 15–30. Available at https://doi.org/10.1007/s40860-019-00095-w

    2020 doi

  14. [22]

    Real Time Syst

    Ron Koymans (1990): Specifying Real-Time Properties with Metric Temporal Logic. Real Time Syst. 2(4), pp. 255–299, doi:10.1007/BF01995674. M. G. Saadat, A. Ferrando, L. A. Dennis, & M. Fisher 55

    1990 doi

  15. [23]

    Martin Leucker & Christian Schallhart (2009): A Brief Account of Runtime Verification . J. Log. Algebraic Methods Program. 78(5), pp. 293–303. Available at https://doi.org/10.1016/j.jlap.2008.08.004

    2009 doi

  16. [24]

    Oded Maler & Dejan Nickovic (2004): Monitoring Temporal Properties of Continuous Signals. In Yassine Lakhnech & Sergio Yovine, editors:Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint International Conferences on Formal Modelling and Analysi...

    2004

  17. [25]

    In Dang Van Hung & Oleg Sokolsky, editors: Proc

    Dejan Nickovic & Tomoya Yamaguchi (2020): RTAMT: Online Robustness Monitors from STL. In Dang Van Hung & Oleg Sokolsky, editors: Proc. 18th International Symposium on Automated Technology for Verifi- cation and Analysis (ATV A), Lecture Notes in Computer Science 12302, Springe...

    2020 doi

  18. [26]

    Technical Report, doi:10.13140/RG.2.2.35163.80163

    Ivan Perez & Alwyn Goodloe (2020): Copilot 3. Technical Report, doi:10.13140/RG.2.2.35163.80163

    2020

  19. [27]

    Martin (2022): Mon- itoring ROS2: from Requirements to Autonomous Robots

    Ivan Perez, Anastasia Mavridou, Thomas Pressburger, Alexander Will & Patrick J. Martin (2022): Mon- itoring ROS2: from Requirements to Autonomous Robots . In Matt Luckcuck & Marie Farrell, editors: Proceedings Fourth International Workshop on Formal Methods for Autonomous Syst...

    2022 doi

  20. [28]

    In: Proc

    Amir Pnueli (1977): The Temporal Logic of Programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, pp. 46–57. Available at https://doi.org/10.1109/SFCS. 1977.32

    1977 doi

  21. [29]

    Basin & Dmitriy Traytel (2020): Multi-head Monitoring of Metric Dynamic Logic

    Martin Raszyk, David A. Basin & Dmitriy Traytel (2020): Multi-head Monitoring of Metric Dynamic Logic. In Dang Van Hung & Oleg Sokolsky, editors:Proc. 18th International Symposium on Automated Technology for Verification and Analysis (ATV A), Lecture Notes in Computer Science ...

    2020 doi

  22. [30]

    In: Proc

    André Santos, Alcino Cunha, Nuno Macedo & Cláudio Lourenço (2016):A framework for quality assessment of ROS repositories. In: Proc. IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), IEEE, pp. 4491–4496. Available at https://doi.org/10.1109/IROS.2016.7759661

    2016

  23. [31]

    Prasad Sistla & Edmund M

    A. Prasad Sistla & Edmund M. Clarke (1985): The Complexity of Propositional Linear Temporal Logics. J. ACM 32(3), pp. 733–749. Available at https://doi.org/10.1145/3828.3837

    1985

Pith tools

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