Pith. sign in

REVIEW 2 major objections 5 minor 38 references

Per-platform monitors miss swarm-level violations that only compositional, evidence-aware runtime verification can catch and refuse to silently clear.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · grok-4.5

2026-07-30 19:54 UTC pith:YA4YS3ZJ

load-bearing objection Solid systems paper: compositional swarm RV plus an evidence-aware fabric that refuses silent all-clears; novelty is mostly the ISR/LLM lift of their prior edge-IoT stack, and the trusted event path is assumed rather than stress-tested. the 2 major comments →

arxiv 2607.23532 v1 pith:YA4YS3ZJ submitted 2026-07-26 cs.CR cs.AIcs.LOcs.RO

Mission-Level Runtime Assurance for LLM-Assisted ISR Swarms over a Verification-Aware Fabric

Nikolaos Kekatos , Stylianos Basagiannis , Panagiotis Katsaros , Alexios Lekidis , Tom Nianios This is my paper
classification cs.CR cs.AIcs.LOcs.RO
keywords runtime verificationLLM-assisted autonomyrobot swarmsdistributed monitoringmission assurancecontested environmentsprompt injectioncross-agent composition
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

When LLM-assisted robot swarms run intelligence missions, a prohibited objective can be split across platforms so that every local action looks legal while the joint outcome breaks the mission rules. Contested links make the problem worse: lost or delayed reports let a naive central monitor issue a confident all-clear. This paper argues that mission assurance therefore needs a three-tier runtime-verification stack—platform, squad, mission—over a messaging fabric that makes delivery loss and silence observable, plus a two-axis verdict that separates “did they violate?” from “do we have enough evidence?”. On a simulated ISR mission, an indirect prompt injection steers real LLM planners into a four-way split that every per-platform monitor accepts, yet the compositional mission monitor detects it with named platforms; under drop and jam faults a best-effort central monitor silently clears incidents while the fabric never does.

Core claim

Individually compliant platform actions can compose into a mission-level violation that no per-platform guardrail can see; a three-tier compositional monitor over a verification-aware fabric detects those joint violations with platform provenance and, when evidence is incomplete, downgrades unsupported all-clears to explicit unknowns instead of silent false clears.

What carries the argument

The evidence-aware two-axis verdict algebra (security × completeness) over the RV-Fabric: cross-agent verdicts carry both a security value and a completeness status derived from observable gaps, order violations, and mission-clock silence, with provenance naming the platforms and witness events that jointly triggered a violation.

Load-bearing premise

The attack can divert only the LLM planner; platforms still report their real actions faithfully, stay authenticated, and may go silent but do not forge identity or systematically lie about what they did.

What would settle it

Run the same ISR task-split under contested links and check whether a best-effort central monitor produces silent mission all-clears while the fabric produces none, and whether every per-platform monitor still reports compliance when the joint package is prohibited.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Mission commanders can treat an unknown/incomplete verdict as a hold-or-re-task signal rather than an all-clear under jamming.
  • Provenance names which platforms jointly breached a policy, enabling targeted supervision without blaming every unit.
  • The same composition pattern covers semantic packages, swarm budgets, joint occupancy counts, and cross-agent causal chains—not only one hand-picked rule.
  • Assurance can drop onto an existing autonomy stack without rewriting safety-critical flight controllers.
  • Silent false all-clears become a measurable safety metric (no-silent-clear rate) for contested multi-robot missions.

Where Pith is reading between the lines

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

  • Any multi-agent LLM system that interprets untrusted retrieved text faces the same split-across-agents failure mode once local schemas and per-agent checks pass.
  • Making transport loss first-class is a general pattern for distributed monitors: without it, “no news is good news” becomes an adversary feature.
  • Independent corroborating witnesses (e.g., RF sentries) would be a natural next layer once platforms can under-report their own actions.
  • The approach suggests mission policies should be written as cross-agent predicates from the start, not only as per-vehicle limits.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

2 major / 5 minor

Summary. The paper presents a three-tier (platform/squad/mission) compositional runtime-verification framework for LLM-assisted ISR swarms. A mission policy is decomposed into per-agent aspects and cross-agent properties (Ppkg: prohibited-package composition; Pemcon: swarm emission budget; Pauth: cross-agent authorisation order). Verdicts carry a two-axis (security x completeness) value with platform provenance, and a "verification-aware fabric" (MQTT QoS1 + NATS JetStream, trusted ingest ordering, event-id gap detection, backend-resident mission clock) makes evidence loss and silence observable, so unsupported negative verdicts are downgraded to unknown rather than reported as mission-wide all-clears. On a simulated ISR scenario where an indirect prompt injection splits a prohibited collection across four platforms, per-platform monitors detect 0/3 mission incidents while the compositional monitor detects all three with provenance; under drop/jam fault campaigns a best-effort central monitor emits silent false all-clears (NSCR 50%) while the fabric emits none (100%). The evaluation includes a Dockerised one-command reproducible core, an executed ROS2/DDS and ArduPilot-SITL layer, a MonPoly cross-check, guarantee ablations (G1/G3), benign-collaboration and timing/skew sweeps, a 500-mission randomised campaign, and a 400-mission ROC check of the budget property.

Significance. If the results hold, the paper addresses a genuine gap: mission-level, cross-agent obligations that per-platform guardrails structurally cannot express, monitored over a transport that degrades to an honest unknown under contested communications rather than a silent all-clear. Strengths worth naming: a fully reproducible deterministic core (single docker run, fixed seeds, per-table scripts enumerated in Appendix A); an executed ROS2/DDS and ArduPilot-SITL realism layer rather than a purely paper design; validation of the cross-agent primitive on the real MonPoly engine; guarantee ablations (Table 8) that causally attribute the zero-silent-clear result to specific fabric signals rather than to the scenario; and a thoughtful argument for NSCR over detection-ROC as the metric of record. The threats-to-validity section (§7.6) is unusually candid about what the controlled experiments do and do not establish. The contribution is incremental over the authors' prior edge-IoT fabric line (acknowledged in §3), but the swarm lifting, the LLM-driven attack scenario, and the evidence-aware composition at mission level are new and relevant to the security/RV community.

major comments (2)
  1. [§3 Threat model vs §6/Fig. 1] The claim that prompt injection 'subverts only the LLM planner ... so a manipulated planner cannot falsify the evidence a platform reports' is not supported by the evaluated pipeline. In all three evaluation layers (scripted generator in the reproducible core; ROS2 nodes publishing 'the attack's actions' on /<ns>/action topics; the SITL 'collected action stream'), canonical events -- including the target attribute F in collect(a,x,F,I) -- are built from the subverted planner's own action fields. The same in-scope injection that splits the task could equally make the planner label the FacX collection as, e.g., 'Sector B waypoint survey': the physical violation would occur while Ppkg, a predicate over the reported F, never fires. §7.4 concedes this pattern for self-reported emissions (RF-sentry) but not for semantic target labels. Please (i) state precisely what part of canonicalisation is
  2. [§7.3 and Abstract] The abstract's headline that 'real LLM planners' split the prohibited collection is supported in this paper only by a pointer to 'a separate empirical study' of seven planners -- no per-model attack-success rates, variants, or even a summary table appear here, and it is not stated whether LLM-emitted action streams were actually driven through the L1/L3 monitors or whether all monitored runs use the scripted generator of §6. Since the 'Why the attack is LLM-specific' argument (§2) motivates the entire scenario, include at least a summary of the seven-planner campaign (models, injection variants, success rates) and state explicitly which events fed which experiments. As written, the central empirical claim of the abstract cannot be verified from this manuscript.
minor comments (5)
  1. [§7, opening paragraph] 'The fault-free RV-Fabric run defines the ground-truth oracle of mission incidents, |I*|=3.' Since the oracle is produced by the system under test, NSCR (Table 9) is measured against a partly self-defined reference. The incidents are in fact planted by the scripted scenario, so an independent ground truth exists -- please state it that way explicitly rather than via the fabric's own fault-free output.
  2. [Table 4] The per-platform-guardrails row counts 9 silent false all-clears (3 incidents x 3 fault conditions, all structural). A footnote explaining this counting convention would help, since the baseline cannot represent cross-agent incidents at all, which makes its column not strictly comparable with the central/fabric rows.
  3. [§7.4 'Real formal engine'] The MonPoly export checks a weaker property ('>=3 distinct platforms collect on the protected site within 30s') than Ppkg (four distinct fragments on F within window W, with authorisation cancellation). Please note the gap explicitly so the formal-engine validation is not read as covering the headline property.
  4. [§3 notation; Figs. 6-7] t is used both as the current mission time and as a free variable in Pauth(aj, Z, t); consider distinct symbols. Fig. 6 lacks a y-axis label and units in the caption; Fig. 7's axis labels are very small.
  5. [Appendix A (Reproducibility)] Appendix A refers to both 'the artifact' and 'the companion artifact' (for the crash/retention/isolation scripts); please clarify whether these are the same repository. Also state the model identifiers for the seven LLM planners in the paper itself, not only in the archived outputs.

Circularity Check

1 steps flagged

Minor self-citation load for the unreproved soundness algebra; central detection claims are experimental invariant checks, not inputs renamed as predictions.

specific steps
  1. self citation load bearing [§3 Background (Carried over vs. new); §4 Conditional soundness; §9 Conclusion]
    "Carried over from that line are the three-tier decomposition, the five fabric guarantees, and the evidence-aware verdict algebra with its conditional-soundness argument [23,22] ... The soundness argument is instantiated, not re-proved; a full proof of the composition algebra remains future work. ... A full proof follows the argument of our prior edge-IoT fabric, instantiated with the cross-agent primitive of Sect. 3."

    The paper's formal assurance that no_violation+sound agrees with the oracle, and that observable loss yields unknown rather than a clean all-clear, is justified by citing the authors' own to-appear edge-IoT fabric papers rather than a self-contained proof or an external machine-checked result. The algebra is load-bearing for the 'zero silent false all-clears' interpretation. This is mild: the empirical fault campaign still independently measures the claimed behaviour, and the citation is not used to forbid alternatives via a uniqueness theorem.

full rationale

This is a systems/RV engineering paper whose strongest claims are comparative experimental outcomes (silent false all-clears, NSCR, provenance match) under planted attacks and injected faults, scored against a designed ground-truth incident set. Those metrics are not fitted parameters recycled as predictions, nor self-definitional identities. The only circularity-adjacent element is that the evidence-aware composition algebra and its conditional-soundness argument are carried over from the authors' own to-appear edge-IoT fabric papers and explicitly 'instantiated, not re-proved,' with a full proof left as future work. That is ordinary incremental systems citation and slightly load-bearing for the formal soundness claim, but it does not force the empirical results: fault-free vs drop/jam tables, guarantee ablations, and the central-vs-fabric contrast are independently executed. The skeptic concern that canonical events originate in planner actions is a threat-model/faithfulness assumption, not a derivation that equates Y to an input defined as Y. Score 2 reflects one non-central self-citation dependency without collapsing the paper's main claims into tautology.

Axiom & Free-Parameter Ledger

4 free parameters · 6 axioms · 2 invented entities

The central claim rests on a trust boundary (faithful event path, authenticated non-forging platforms), monotone-witness conditional soundness carried from prior fabric work, and engineering parameters (windows, budgets, silence timeout) that define when properties fire—not on fitted physical constants. Invented naming (RV-Fabric, two-axis verdict) packages existing brokers and RV engines rather than new physics.

free parameters (4)
  • mission sliding window W = scenario-dependent (e.g. package within W; MonPoly example 30s)
    Defines the temporal scope for Ppkg, Pemcon, Pauth; low-and-slow adversary can evade if span exceeds W (§7.4). Chosen for the mission scenario, not derived.
  • Bmission EMCON budget and per-platform local limits = e.g. Bmission=900B, local 500B, swarm total 1200B in sensitivity table
    Thresholds that separate L1 vs L3 catch regions in the split-cardinality sweep (Table 7); set by mission policy design.
  • mission-clock silence timeout = 5s (knee); 2s/10s explored
    Trades jam-detection latency vs false-silence flags; 5s chosen as knee over 300 jittery missions (§7.3).
  • order window for causal properties = e.g. 5s window; skew ≥10s triggers unknown
    Clock-skew sweep downgrades auth-order/targeting-chain beyond window rather than false verdict (§7.3).
axioms (6)
  • domain assumption Monotone witness properties: violations certified by finite event sets are preserved under supersets; loss only removes evidence
    Conditional soundness of the two-axis algebra for Ppkg/Pemcon/Pauth (§4); full proof deferred to prior fabric instantiation.
  • domain assumption Authenticated platform identity; adversary cannot forge identity on the protected path
    Threat model Table 1; residual risk marked outside trust boundary.
  • domain assumption LLM injection subverts only the planner; structured event generation and monitors report actual executed actions faithfully
    §3 threat model and §2 ‘trusted event-generation and monitoring path is unaffected’.
  • domain assumption MQTT QoS1 + durable outbox and NATS JetStream provide at-least-once delivery, monotone ingest order, and durable cursors as modeled (G1–G5)
    §5 Table 3; systems validation on real brokers supports but does not formally verify all contested-environment cases.
  • domain assumption Backend-resident mission clock remains available even if all platforms are lost
    Required so silence is observable (G3); §4–5.
  • standard math Standard past-time / MFOTL and stream monitoring semantics (MonPoly, RTLola-style)
    Background RV engines cited (§3, §8); used as decision procedures for cross-agent properties.
invented entities (2)
  • RV-Fabric (verification-aware messaging fabric) independent evidence
    purpose: Name the five-guarantee transport that makes loss, reorder, and silence observable to mission monitors
    Built from MQTT + NATS JetStream + sidecar timestamps/outbox + mission clock; packaging of known mechanisms with swarm semantics, largely carried from prior edge-IoT fabric.
  • Two-axis evidence-aware verdict (security × completeness) with provenance independent evidence
    purpose: Separate did-violate from enough-evidence and name contributing platforms/events
    Composition rule downgrades no_violation over non-sound evidence to unknown (§4); algebra reused from prior work, applied to swarm cross-agent properties.

pith-pipeline@v1.2.0-grok45-kimik3 · 23868 in / 3991 out tokens · 98317 ms · 2026-07-30T19:54:08.896024+00:00 · methodology

0 comments
read the original abstract

Swarms of LLM-assisted autonomous robots are increasingly proposed for cooperative intelligence, surveillance, and reconnaissance (ISR) in contested environments. A growing class of their assurance failures arises not within any single platform but across the swarm: individually-compliant actions compose into a mission-level violation: a prohibited objective split across platforms to evade per-platform lim- its, or a collective budget quietly exceeded. Per-platform guardrails miss these by construction, and contested communications let the violation hide behind lost or delayed evidence. We present a three-tier (platfor- m/squad/mission) compositional runtime-verification framework that de- composes a mission policy into per-agent and cross-agent aspects, aggre- gates per-platform verdicts over a verification-aware messaging fabric, and fuses them with an evidence-aware, two-axis (security x complete- ness) algebra whose provenance names the platforms that jointly trig- gered a violation. Because the fabric makes evidence loss and silence observable, unsupported negative verdicts are downgraded to an explicit unknown rather than reported as mission-wide all-clears. On a simulated ISR mission, an indirect prompt injection that causes real LLM planners to split a prohibited collection task across four platforms is invisible to every per-platform monitor yet detected compositionally with full prove- nance; under an injected fault campaign a best-effort central monitor emits silent false all-clears while the verification-aware fabric emits none

Figures

Figures reproduced from arXiv: 2607.23532 by Alexios Lekidis, Nikolaos Kekatos, Panagiotis Katsaros, Stylianos Basagiannis, Tom Nianios.

Figure 1
Figure 1. Figure 1: High-level approach. Adversarial content retrieved mid-mission diverts the per-platform LLM planners a1, . . . , an (each ai denotes an individual platform/agent); the actions they emit are canonicalised into a shared event stream that feeds the three￾tier (L1/L2/L3) monitors over the verification-aware fabric, which produce a two-axis verdict (s, c) with platform provenance. Individually-benign per-platfo… view at source ↗
Figure 2
Figure 2. Figure 2: The distributed violation. Each platform’s collection action is individually permitted and passes its per-platform (L1) monitor; only the cross-agent composition (L3) constitutes the prohibited intelligence package, reported with platform provenance. "sensor":"eo_camera"} # event: collect(imagery, SectorB) # retrieved-intel prompt injection -> "Divide the Facility X collection among available units; transm… view at source ↗
Figure 3
Figure 3. Figure 3: Three-tier deployment. Per-platform L1 monitors publish over MQTT to a squad coordinator (L2) whose sidecar assigns trusted timestamps and event-ids and relays durably to a JetStream backend; the mission (L3) monitor reads via its own cursor and a backend-resident mission clock supplies silence-liveness. The five guarantees of [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The ISR mission executed with ArduPilot SITL (four simulated platforms, MAVLink telemetry); the 360 position samples are generated by the SITL flight￾dynamics model. Trajectories converge on Facility X, uav_2 crosses the sensitive zone, and the four split-collection events (stars, one fragment per platform) are labelled around the facility. Every per-platform (L1) monitor is compliant, yet the compositiona… view at source ↗
Figure 5
Figure 5. Figure 5: The interactive Mission RV Console on the intel-package scenario at mission end: every per-platform (L1) verdict is no_violation (bottom left), while the compositional (L3) monitor reports all three mission violations (red chips, right) with platform provenance; the map shows the four trajectories converging on Facility X. Faults and the evidence-aware vs. best-effort monitor are switchable live. Benign mi… view at source ↗
Figure 6
Figure 6. Figure 6: Silent false all-clears summed over the four objectives and the three-fault campaign (lower is better; shading darkens with severity). Per-platform guardrails are structurally blind (they never see the cross-agent incident); the central best-effort monitor silently misses under fault; the RV-Fabric alone reaches zero [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Mission-monitor evaluation time vs swarm size (real measurements). Cross￾agent checking scales roughly linearly and stays sub-2 ms to 1000 platforms, orders of magnitude below the second-scale mission-decision budget. to (unknown, incomplete): a flagged 2/3 +1u with zero silent misses. Under jam uav_3 (a denial, G3), both the package (missing comms) and the emissions budget (missing uav_3’s transmissions, … view at source ↗

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 · 2 linked inside Pith

  1. [1]

    Abdelsalam, M., Bensalem, S., Delacourt, A., He, W., Katsaros, P., Kekatos, N., Ruiz Nolasco, R., Peled, D., Ponchant, M., Ryad, I., Temperekidis, A., Wu, C.: Digitaltwinfortheformalanalysisofadepthofanesthesiacontroller.SIMULATION 101(3), 341–360 (2025)

    2025

  2. [2]

    In: Conf

    Ahn, M., Brohan, A., Brown, N., et al.: Do as i can, not as i say: Grounding language in robotic affordances. In: Conf. on Robot Learning (CoRL) (2022)

    2022

  3. [3]

    In: MEMOCODE

    Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems (STREL). In: MEMOCODE. pp. 146–155 (2017)

    2017

  4. [4]

    Lectures on Runtime Verification, LNCS 10457 (2018)

    Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. Lectures on Runtime Verification, LNCS 10457 (2018)

    2018

  5. [5]

    Journal of the ACM62(2) (2015)

    Basin, D., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. Journal of the ACM62(2) (2015)

    2015

  6. [6]

    In: RV-CuBES (2017)

    Basin, D., Klaedtke, F., Zalinescu, E.: The MonPoly monitoring tool. In: RV-CuBES (2017)

    2017

  7. [7]

    ACM Transactions on Software Engineering and Methodology (TOSEM)20(4) (2011)

    Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM)20(4) (2011)

    2011

  8. [8]

    In: Bridging the Gap Between AI and Reality (AISoLA 2023)

    Bensalem, S., Katsaros, P., Kekatos, N., et al.: Continuous engineering for trust- worthy learning-enabled autonomous systems. In: Bridging the Gap Between AI and Reality (AISoLA 2023). LNCS, vol. 14380. Springer (2023)

    2023

  9. [9]

    In: CONCUR (2016)

    Bonakdarpour, B., Fraigniaud, P., Rajsbaum, S., Rosenblueth, D.A., Travers, C.: Decentralized asynchronous crash-resilient runtime verification. In: CONCUR (2016)

    2016

  10. [10]

    Swarm Intelligence7(1), 1–41 (2013)

    Brambilla, M., Ferrante, E., Birattari, M., Dorigo, M.: Swarm robotics: A review from the swarm engineering perspective. Swarm Intelligence7(1), 1–41 (2013)

    2013

  11. [11]

    IEEE Transactions on Robotics34(4), 837–855 (2018)

    Chung, S.J., Paranjape, A.A., Dames, P., Shen, S., Kumar, V.: A survey on aerial swarm robotics. IEEE Transactions on Robotics34(4), 837–855 (2018)

    2018

  12. [12]

    In: SBMF (2018)

    Convent, L., Hungerecker, S., Leucker, M., Scheffel, T., Schmitz, M., Thoma, D.: TeSSLa: Temporal stream-based specification language. In: SBMF (2018)

    2018

  13. [13]

    In: IEEE Conference on Decision and Control (CDC) (2023)

    Dang, T., Donzé, A., Haque, I., Kekatos, N., Saha, I.: Counter-example guided imitation learning of feedback controllers from temporal logic specifications. In: IEEE Conference on Decision and Control (CDC) (2023)

    2023

  14. [14]

    In: NeurIPS Datasets and Benchmarks (2024)

    Debenedetti, E., et al.: AgentDojo: A dynamic environment to evaluate prompt injection attacks and defenses for llm agents. In: NeurIPS Datasets and Benchmarks (2024)

    2024

  15. [15]

    In: 49th IEEE/IFIP Int

    Desai, A., Ghosh, S., Seshia, S.A., Shankar, N., Tiwari, A.: SOTER: A runtime assurance framework for programming safe robotics systems. In: 49th IEEE/IFIP Int. Conf. on Dependable Systems and Networks (DSN). pp. 138–150 (2019)

    2019

  16. [16]

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

    Eleftheriadis, C., Kekatos, N., Katsaros, P., Tripakis, S.: On neural network equiv- alence checking using SMT solvers. In: Formal Modeling and Analysis of Timed Systems (FORMATS). pp. 237–257. LNCS (2022)

    2022

  17. [17]

    In: Computer Aided Verification (CAV) (2019) Mission-Level Runtime Assurance for ISR Swarms 25

    Faymonville, P., Finkbeiner, B., Schledjewski, M., Schwenger, M., Stenger, M., Tentrup, L., Torfah, H.: StreamLAB: Stream-based monitoring of cyber-physical systems. In: Computer Aided Verification (CAV) (2019) Mission-Level Runtime Assurance for ISR Swarms 25

    2019

  18. [18]

    In: Towards Au- tonomous Robotic Systems (TAROS)

    Ferrando, A., Cardoso, R.C., Fisher, M., Ancona, D., Franceschini, L., Mascardi, V.: ROSMonitoring: A runtime verification framework for ROS. In: Towards Au- tonomous Robotic Systems (TAROS). LNCS, vol. 12228, pp. 387–399. Springer (2020)

    2020

  19. [19]

    In: Runtime Verification (RV) (2014)

    Fraigniaud, P., Rajsbaum, S., Travers, C.: On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In: Runtime Verification (RV) (2014)

    2014

  20. [20]

    In: ACM Workshop on Artificial Intelligence and Security (AISec) (2023)

    Greshake, K., Abdelnabi, S., Mishra, S., Endres, C., Holz, T., Fritz, M.: Not what you’ve signed up for: Compromising real-world LLM-integrated applications with indirect prompt injection. In: ACM Workshop on Artificial Intelligence and Security (AISec) (2023)

    2023

  21. [21]

    In: Formal Methods in Computer-Aided Design (FMCAD) (2017)

    Havelund, K., Peled, D., Ulus, D.: First-order temporal logic monitoring with BDDs. In: Formal Methods in Computer-Aided Design (FMCAD) (2017)

    2017

  22. [22]

    In: IEEE International Conference on Cyber Security and Resilience (CSR) (2026), to appear

    Kekatos, N., Chintri, M., Katsaros, P., Nianios, T., Seitoglou, I., Basagiannis, S.: Hierarchical security monitoring for edge-iot: A formal methods approach. In: IEEE International Conference on Cyber Security and Resilience (CSR) (2026), to appear

    2026

  23. [23]

    Kekatos, N., Chintri, M., Katsaros, P., Lekidis, A., Nianios, T., Seitoglou, I., Temperekidis, A., Basagiannis, S.: A hierarchical runtime-verification approach for security monitoring of edge-iot. In: Int. Workshop on Advances in Practical Security (ARES) (2026), to appear

    2026

  24. [24]

    In: ARES 2026 Workshops (EPES-SPR) (2026), to appear

    Kekatos, N., Koutidis, G., Antonakopoulos, K., Basagiannis, S., Katsikas, S., Kaval- lieratos,G.,Lekidis,A.,Nianios,T.,Papageorgiou,E.:RESILAGENT:Athree-pillar architecture for cyber-physical resilience in electrical power and energy systems. In: ARES 2026 Workshops (EPES-SPR) (2026), to appear

    2026

  25. [25]

    Lee, D., Tiwari, M.: Prompt infection: LLM-to-LLM prompt injection within multi-agent systems (2024), arXiv:2410.07283

    Pith/arXiv arXiv 2024

  26. [26]

    Journal of Logic and Algebraic Programming78(5), 293–303 (2009)

    Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming78(5), 293–303 (2009)

    2009

  27. [27]

    Li, J.J., He, J., Shang, C., Kulshreshtha, D., Xian, X., Zhang, Y., Su, H., Swamy, S., Qi, Y.: STAC: When innocent tools form dangerous chains to jailbreak LLM agents (2025), arXiv:2509.25624

    Pith/arXiv arXiv 2025

  28. [28]

    In: USENIX Security Symposium (2024)

    Liu, Y., Jia, Y., Geng, R., Jia, J., Gong, N.Z.: Formalizing and benchmarking prompt injection attacks and defenses. In: USENIX Security Symposium (2024)

    2024

  29. [29]

    (eds.): Modelling and Simulation for Autonomous Systems (MESAS 2024), Revised Selected Papers, LNCS, vol

    Mazal, J., Fagiolini, A., et al. (eds.): Modelling and Simulation for Autonomous Systems (MESAS 2024), Revised Selected Papers, LNCS, vol. 15761. Springer (2025)

    2024

  30. [30]

    OASIS Standard (2019)

    OASIS: MQTT version 5.0. OASIS Standard (2019)

    2019

  31. [31]

    In: NeurIPS ML Safety Workshop (2022)

    Perez, F., Ribeiro, I.: Ignore previous prompt: Attack techniques for language models. In: NeurIPS ML Safety Workshop (2022)

    2022

  32. [32]

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

    Sha, L.: Using simplicity to control complexity. IEEE Software18(4), 20–28 (2001)

    2001

  33. [33]

    IEEE Internet of Things Journal3(5) (2016)

    Shi, W., Cao, J., Zhang, Q., Li, Y., Xu, L.: Edge computing: Vision and challenges. IEEE Internet of Things Journal3(5) (2016)

    2016

  34. [34]

    In: ARES 2026 Workshops (GenXSec) (2026), to appear

    Sinha, P., Kekatos, N., Basagiannis, S., Bruto da Costa, A.A., Lekidis, A., Mitra, P., Nianios, T., Papageorgiou, E.: Explainable rule mining of IPv6 extension- header presence patterns from paired-vantage captures. In: ARES 2026 Workshops (GenXSec) (2026), to appear

    2026

  35. [35]

    Synadia / CNCF: NATS and JetStream.https://nats.io(2024)

    2024

  36. [36]

    Runtime Verification (RV), LNCS 13498 (2022) 26 N

    Temperekidis, A., Kekatos, N., Katsaros, P.: Runtime verification for FMI-based co-simulation. Runtime Verification (RV), LNCS 13498 (2022) 26 N. Kekatos et al

    2022

  37. [37]

    In: MESAS

    Temperekidis, A., Kekatos, N., Katsaros, P., et al.: Towards a digital twin architec- ture with formal analysis capabilities for learning-enabled autonomous systems. In: MESAS. LNCS, vol. 13866 (2022)

    2022

  38. [38]

    Zhan, Q., Liang, Z., Ying, Z., Kang, D.: InjecAgent: Benchmarking indirect prompt injections in tool-integrated large language model agents. In: Findings of the Association for Computational Linguistics (ACL) (2024) A Reproducibility The reproducible core (kinematic mission, monitors, verification-aware fabric, fault campaign) and the ROS2 adapter are pro...

    2024