Cross--layer Formal Verification of Robotic Systems

David Doose; Fr\'ed\'eric Herbreteau; Julien Brunel; Sylvain Ra\"is

REVIEW 3 major objections 4 minor 13 references

Cross--layer Formal Verification of Robotic Systems

T0 review · 3 major / 4 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 The paper establishes that multi-layer robot properties such as "skill goto cannot be executed infinitely often" can be verified by refining either the functional-layer model or the LTL property under an assumption, and that combining the…

desk verdict A clear, honest workshop-scale proposal for cross-layer verification, held back by the missing abstraction correspondence between the verified models and the robot implementation. read the letter →

arxiv 2411.14373 v1 pith:JLK6J735 submitted 2024-11-21 cs.RO

Sylvain Raïs , Julien Brunel , David Doose , Frédéric Herbreteau This is my paper · ORCID

classification cs.RO MSC 68Q6068Q85

keywords cross-layerverificationRobotLanguageLTLmodelcheckingabstractionrefinementskill-basedroboticsfinitetransitionsystemsmulti-layerarchitecturesbatteryresourcemodeling

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

Robotic systems are designed in layers, yet some safety properties only make sense across layers. This paper argues that such cross-layer properties can be verified without flattening the whole system: one layer is checked against abstract models of the others, and either the abstract model or the property itself is refined. On a RobotLanguage example, the property "the goto skill cannot be executed infinitely often" is proved in two ways: by refining the functional-layer model with distance and battery variables, or by refining the LTL property to hold under the assumption that the battery eventually stays Critical. Both proofs succeed, and the property-refinement version keeps the model much smaller. The authors position the two approaches as complementary and leave the correspondence between abstract models and implementation for future work.

What carries the argument

The central machinery is a set of finite labeled transition systems that synchronize on common events, forming a global run. The executive-layer skill control-flow graph (Ready, Precondition, Validate, Start, Running, and so on) supplies the property's observed states; the functional-layer models $F$ (most abstract, allowing every event sequence) and $F'$ (refined with guards on $d$ and $blevel$) supply the environment; and the LTL formula is the interface. The paper's two operations, model refinement from $F$ to $F'$ and property refinement from formula (1) to formula (2), carry the verification because both transform an unprovable cross-layer requirement into one that holds on a synchronized product of modest size.

What would settle it

Construct a run of the synchronized model $\{S,F'\}$ in which $blevel$ never drops below $2.0$ and $validate\ success$ occurs infinitely often; the model checker would then return false for formula (1), contradicting the paper's claim for that model. Alternatively, instrument the real robot: if a recharge skill is added or battery consumption is less than $2.0$ per meter, the skill can be executed infinitely often while the paper's assumption no longer holds.

Watch

Extended reading notes

Core claim

The paper's central claim is that a multi-layer specification such as "skill goto cannot be executed infinitely often", written $FG\lnot Running$, can be established by either of two refinement strategies. In the first, the functional layer is modeled concretely enough (distance $d$ and battery level $blevel$, with each meter costing $2.0$ battery units) so that the battery eventually runs out and only failure transitions remain; the formula then holds on the synchronized model $\{S,F'\}$. In the second, the abstract functional layer $F$ is kept, and the specification is strengthened to $FG\ Critical \Rightarrow FG\lnot Running$; because the skill's precondition forbids starting while the battery is Critical, the implication holds on the smaller model $\{S,F\}$. The paper shows both formulas pass with a model checker and argues that combining the approaches, refining only the parts of the model that need precision, is the most promising way to keep models generic and avoid state-space explosion. It also states, as future work, that proving the abstract models correspond to the actual layer implementations remains open.

Load-bearing premise

Everything rests on the assumption that the abstract functional-layer models faithfully describe the real robot's low-level behavior, specifically that motion consumes battery at the modeled rate and that no recharge skill exists; the authors note this correspondence is not yet proved.

Editorial extensions

If this is right

After enough time, the battery level $blevel$ falls below $2.0$ on any run of the refined model, so the goto skill can only fail and $FG\lnot Running$ holds.
On the abstract model, the implication $FG\ Critical \Rightarrow FG\lnot Running$ holds because the skill's precondition blocks new runs once the battery is Critical.
Combining model refinement and property refinement lets the designer add implementation detail only where the property requires it, keeping models small.
The same synchronization-interface scheme applies to the decision layer, so cross-layer decision and executive properties can be handled analogously.
When a cross-layer property does not hold, the property-refinement formulation yields a simpler counterexample than a fully refined model.

Reading between the lines

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

A tool could automate the choice by starting from the abstract model and using counterexamples to decide whether to refine the model or strengthen the assumption; the paper leaves this selection manual.
The same implication form should extend to other resource-exhaustion properties, such as memory, energy, or network budgets, where an eventual resource bound implies a liveness condition.
The unproved abstraction-to-implementation correspondence means today's certificates apply to the RobotLanguage model rather than the generated ROS2 code; a refinement proof for the generated hooks would close that gap.

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.

Desk Editor's Note

read the letter

Short version: this is a solid workshop paper that does what it says: it lays out two complementary ways to verify a cross-layer property on a skill-based robot model and checks both on a small battery example with Tatam. The novelty is modest—model refinement and property refinement are standard compositional ideas—but the application to RobotLanguage-style executive/functional layers is natural and the paper is honest about what is not done.

What I like: the example is small but actually executed. The authors translate both approaches into Tatam, report that the raw abstract model falsifies the property and the two refined variants prove it, and they put the models in a public repo. That is reproducible evidence, not just a proposal. The distinction between keeping the model abstract and refining the LTL formula under an assumption is worth having in this domain.

Where the soft spots are: the load-bearing assumption is that the functional-layer models F and F' correspond to the real implementation—the generated C++ hooks, the resource-update mechanism, and the real battery dynamics. The paper says this correspondence proof is future work, so technically both approaches prove properties of a model, not of a robot. That is not hidden; it is stated in Section 4, but it means the central claim is under-supported. Also, there is no formal definition of 'refinement' and no soundness theorem: F' is described informally as restricting sequences of events, and the property is checked on a small finite-state instance. For a workshop paper this is acceptable; for a journal it would need more. The second concern—that the model encodes the conclusion because the battery only drains and there is no recharge—is not really a flaw; the design deliberately lacks a recharge skill, so the property should hold on the model. The real question is whether the abstraction is faithful, which is exactly the unproven part.

Bottom line: this is a useful, honest position paper with a runnable example. It deserves peer review at workshop level, and it could grow into a real method if the authors add an abstraction/simulation relation between the models and the generated code. I would not cite it in my next paper, but I would point a student to it as a simple entry point into cross-layer verification for skill-based robotics. Send it to reviewers; expect them to ask for the correspondence proof.

Referee Report

3 major / 4 minor

Summary. The paper proposes a cross-layer formal verification method for skill-based robotic systems modeled in RobotLanguage. The method models the executive layer with a generic skill control-flow graph and the functional layer with either a most-abstract transition system (F) or a refined transition system (F') that tracks distance and battery level. Two verification approaches are presented: (1) refine the functional-layer model so that an LTL property such as "skill goto cannot be executed infinitely often" holds, and (2) refine the LTL property into an implication whose antecedent is a system assumption (e.g., the battery eventually becomes Critical forever). Both approaches are illustrated on a single example with the Tatam model checker, and the models are made available in a public repository.

Significance. If the method were fully formalized, it would address a real need: verifying properties that cross the executive/functional layer boundary while keeping models small. The two-approach decomposition (model refinement versus property refinement) is a sensible and potentially useful idea, and the paper provides a small, reproducible case study with machine-checked results. However, the current significance is limited because the paper does not state a formal notion of refinement or a soundness theorem, so the verified properties are not shown to transfer from the abstract model to the actual robotic system. The authors explicitly defer this correspondence proof to future work, which makes the paper a promising research note rather than a complete verification methodology.

major comments (3)

[Section 3.4, Figure 3] The paper never defines what "refinement" means formally. The claim that F' is a refinement of F because it "restricts the sequences of events" (Section 3.4) is informal, and no simulation, bisimulation, or abstraction relation is given. Consequently, no soundness theorem states that verifying property (1) on {S,F'} implies that the property holds on the concrete robot or even on {S,F}. Since Section 4 acknowledges that proving the correspondence between abstract models and implementations is future work, the headline claim that the method verifies "concrete robotic systems" is not supported.
[Section 3.5, Eq. (1) and Figure 3b] The refined model F' is designed with variable blevel and guards such that the battery eventually becomes insufficient (there is no recharge skill), so the property FG not Running holds by construction. This is not itself a flaw, but the missing piece is the connection between blevel and the RobotLanguage resource battery. The paper states that "the model for updating the battery resource according to the actual value of blevel is not shown for the sake of simplicity." Without that resource-update model, the verification result applies only to the transition system {S,F'}, not to the actual robot whose battery state is supposed to be represented. The inference that the battery eventually becomes Critical is assumed, not proved.
[Section 3.5, Eq. (2)] The second approach verifies the implication FG Critical => FG not Running. The antecedent is introduced as an assumption, and the argument that the design "lacks a skill to recharge the battery" and therefore "we can expect" Critical to eventually hold is not a formal proof. The abstract model F does not itself enforce the antecedent, and the resource model that would connect the battery to Critical is not shown. Thus the verification result is conditional: it only holds on runs that already satisfy the assumption. The paper should either prove that the antecedent follows from the multi-layer model (including the resource model) or clearly state that the contribution is the conditional property.

minor comments (4)

[Section 3.4, first paragraph] "For now on" should be "From now on."
[Section 3.5, Eq. (1)] The formula is typeset as "F Gnot Running"; it should be "FG not Running" (or with a space) to avoid confusion with a formula named "Gnot."
[Section 3.5, last paragraph] The paper states that the Tatam models are available in a public repository, but it does not specify the exact tool version or the encoding used. Adding this information would improve reproducibility.
[Throughout] The meaning of the unlabeled transitions in Figure 2 (plain, zigzag, dashed, dotted) is described in the text, but the legend in the figure is incomplete (e.g., the "precond success" and "validate success" labels are absent). A more complete legend would be helpful.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the verification results are model-checking theorems on explicitly constructed models, and the acknowledged gap between those models and the implementation is a validation limitation, not a circular step.

full rationale

The paper's claimed results are (1) that FG not Running holds on the synchronized model {S,F'} built from Figure 2 and Figure 3b, and (2) that the implication FG Critical => FG not Running holds on {S,F} built from Figure 2 and Figure 3a. Both statements are established by model checking the explicitly given transition systems, and the models are defined independently of the LTL formulae. The property follows from the chosen guards and updates (battery level decreases by 2.0 per move, no recharge skill exists), but that is a modeling choice for an illustrative example, not a case where a fitted parameter is renamed as a prediction or where the target formula defines the model. The paper is honest about the main weakness: Section 4 states that proving that the abstract models correspond to the implementations is future work, and Section 3.4 notes that the model updating the battery resource from blevel is 'not shown for the sake of simplicity'. These are soundness and validation gaps in transferring the model-level guarantee to the concrete robot, and they should be weighed as correctness risk rather than as circularity. The self-citations to RobotLanguage are contextual descriptions of the framework and are not load-bearing in the reduction of the property to an input. Consequently, there is no significant circularity in the derivation chain.

Assumptions & free parameters 2 free parameters · 5 assumptions · 0 invented entities

The central example is not fitted to data; instead, the distance and battery variables are modeling choices that make the verification conclusion follow. The battery consumption rate (2.0) and threshold (2.0) are chosen by hand and directly enforce eventual exhaustion. The main formal dependency is the unproven abstraction correspondence between the model and the functional-layer implementation.

free parameters (2)

Initial distance d = unspecified finite value
The refined functional layer model F' has variable d; property (1) holds because d decreases by 1 on each move and eventually reaches 0 or the battery fails. The paper does not specify domains or initial values.
Battery consumption rate and critical threshold = consume 2.0 per move, critical below 2.0
These constants are chosen in Figure 3b to ensure the battery eventually becomes insufficient; they determine that the refined model satisfies the property, so the verification result is sensitive to them.

assumptions (5)

domain assumption A three-layer architecture (decision, executive, functional) is a valid decomposition for the robotic systems under consideration.
Section 1 introduces the architecture as a 'promising and widely used approach'; the method is built on it, but no formal justification is given for why every relevant system fits it.
standard math Labeled transition systems with synchronization on common events faithfully model the composition of robotic layers.
Section 3.2 defines the global behavior as parallel composition via shared labels; this is a standard semantics but its adequacy for RobotLanguage code is not proven.
ad hoc to paper The transition system F' in Figure 3b is a faithful refinement of the concrete functional layer, including battery consumption of 2.0 per move and absence of recharge.
Section 3.5 uses F' to conclude the property holds; the paper defers the correspondence proof to future work in Section 4, making this the load-bearing assumption.
domain assumption The RobotLanguage design has no battery recharge skill, so the battery eventually becomes Critical.
Listing 1 shows only the goto skill, and Section 3.5 relies on the absence of a recharge skill to make the property hold; this is an assumption about the system under design, not a proven fact.
domain assumption The Tatam model checker correctly checks the LTL formulas on the generated transition systems.
Section 3.5 relies on Tatam runs to establish both the counterexample and the two proofs; the paper does not independently verify the tool's results.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Cross--layer Formal Verification of Robotic Systems." pith.science (2026). https://pith.science/paper/JLK6J735

@misc{pith2026241114373,
  author       = {Pith},
  title        = {Pith review of: Cross--layer Formal Verification of Robotic Systems},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JLK6J735}},
  note         = {Machine review of arXiv:2411.14373}
}

read the original abstract

Robotic systems are widely used to interact with humans or to perform critical tasks. As a result, it is imperative to provide guarantees about their behavior. Due to the modularity and complexity of robotic systems, their design and verification are often divided into several layers. However, some system properties can only be investigated by considering multiple layers simultaneously. We propose a cross-layer verification method to verify the expected properties of concrete robotic systems. Our method verifies one layer using abstractions of other layers. We propose two approaches: refining the models of the abstract layers and refining the property under verification. A combination of these two approaches seems to be the most promising to ensure model genericity and to avoid the state-space explosion problem.

Figures

Figures reproduced from arXiv: 2411.14373 by the authors.

**Figure 2.** Control flow graph of a skill with the functional layer (dashed/dotted transitions). The execution begins in the state Ready, and spans into three phases. First, on reception of request from the decision layer, the state of the system is checked at the executive layer (precond) and the functional layer (validate). If these conditions are satisfied, start_hook triggers the execution of the functional layer, switching… view at source ↗

**Figure 3.** Transition systems modeling the skill goto at the functional layer that the variables used at the functional layer partly model the robot’s state, while the RobotLanguage resources used in the executive layer (Listing 1) are abstract knowledge of the robot’s state, updated by monitoring the robot. The model for updating the battery resource according to the actual value of blevel is not shown for the sake of simplic… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

13 extracted references · 7 canonical work pages

[1]

Alexandre Albore, David Doose, Christophe Grand, Jérémie Guiochet, Charles Lesire & Au- gustin Manecy (2023): Skill-based design of dependable robotic architectures 160, p. 104318. doi:10.1016/J.ROBOT.2022.104318

arXiv 2023
[2]

Alexandre Albore, David Doose, Christophe Grand, Charles Lesire & Augustin Manecy (2021): Skill- Based Architecture Development for Online Mission Reconfiguration and Failure Management , pp. 47–54. doi:10.1109/ROSE52553.2021.00015

arXiv 2021
[3]

Alcácer & V

V . Alcácer & V . Cruz-Machado (2019):Scanning the Industry 4.0: A Literature Review on Technologies for Manufacturing Systems. Engineering Science and Technology, an International Journal 22(3), pp. 899–919, doi:10.1016/j.jestch.2019.01.006. Available at https://www.sciencedirect.com/science/article/ pii/S2215098618317750

work page doi:10.1016/j.jestch.2019.01.006 2019
[5]

7227–7232

Christophe Grand Charles Lesire, David Doose (2020): Formalization of Robot Skills with Descriptive and Operational Models, pp. 7227–7232. doi:10.1109/IROS45743.2020.9340698

arXiv 2020
[6]

Lukas Johannes Dust, Rong Gu, Cristina Seceleanu, Mikael Ekström & Saad Mubeen (2023): Pattern-Based Verification of ROS 2 Nodes Using UPPAAL. In Alessandro Cimatti & Laura Titolo, editors:Formal Methods for Industrial Critical Systems - 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023, Proceedings, 14290, Springer, pp. 5...

work page doi:10.1007/978-3-031-43681-9_4 2023
[7]

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: Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, 8734, Springer, pp. 247–254, doi:10....

doi:10.1007/978-3-319-11164-3_20 2014
[8]

PROSKILL: A formal skill language for acting in robotics

Félix Ingrand (2024): PROSKILL: A formal skill language for acting in robotics . CoRR abs/2403.07770, doi:10.48550/ARXIV .2403.07770

work page Pith review arXiv doi:10.48550/arxiv.2403.07770 2024
[9]

Robotics 7(3), p

André Leite, Andry Maykol Pinto & Aníbal Matos (2018): A Safety Monitoring Model for a Faulty Mobile Robot. Robotics 7(3), p. 32, doi:10.3390/ROBOTICS7030032

work page doi:10.3390/robotics7030032 2018

Show all 13 references

[10]

Robotics and Computer-Integrated Manufacturing 37, pp

Mikkel Rath Pedersen, Lazaros Nalpantidis, Rasmus Skovgaard Andersen, Casper Schou, Simon Bøgh, V olker Krüger & Ole Madsen (2016):Robot skills for manufacturing: From concept to industrial deployment. Robotics and Computer-Integrated Manufacturing 37, pp. 282–291, doi:10.1016...

2016 doi
[11]

Baptiste Pelletier, Charles Lesire, David Doose, Karen Godary-Dejean & Charles Dramé-Maigné (2022): SkiNet, A Petri Net Generation Tool for the Verification of Skillset-based Autonomous Systems . In Matt Luckcuck & Marie Farrell, editors: Proceedings Fourth International Works...

2022
[12]

In: IEEE International Conference on Robotics and Automation, ICRA 2023, London, UK, May 29 - June 2, 2023 , IEEE, pp

Baptiste Pelletier, Charles Lesire, Christophe Grand, David Doose & Mathieu Rognant (2023): Predictive Runtime Verification of Skill-based Robotic Systems using Petri Nets . In: IEEE International Conference on Robotics and Automation, ICRA 2023, London, UK, May 29 - June 2, 2...

2023
[13]

Francesco Rovida, Matthew Crosby, Dirk Holz, Athanasios Polydoros, Bjarne Großmann, Ronald Petrick & V olker Krueger (2017): SkiROS—A skill-based robot control platform on top of ROS , pp. 121–160. doi:10.1007/978-3-319-54927-9_4. 150 Cross-layer Formal Verification of Robotic Systems

2017 doi
[14]

Robotics and Computer-Integrated Man- ufacturing 53, pp

Casper Schou, Rasmus Skovgaard Andersen, Dimitrios Chrysostomou, Simon Bøgh & Ole Madsen (2018): Skill-based instruction of collaborative robots in industrial settings. Robotics and Computer-Integrated Man- ufacturing 53, pp. 72–80, doi:10.1016/j.rcim.2018.03.008. Available at...

2018 doi

Pith tools

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

[1] [1]

Alexandre Albore, David Doose, Christophe Grand, Jérémie Guiochet, Charles Lesire & Au- gustin Manecy (2023): Skill-based design of dependable robotic architectures 160, p. 104318. doi:10.1016/J.ROBOT.2022.104318

arXiv 2023

[2] [2]

Alexandre Albore, David Doose, Christophe Grand, Charles Lesire & Augustin Manecy (2021): Skill- Based Architecture Development for Online Mission Reconfiguration and Failure Management , pp. 47–54. doi:10.1109/ROSE52553.2021.00015

arXiv 2021

[3] [3]

Alcácer & V

V . Alcácer & V . Cruz-Machado (2019):Scanning the Industry 4.0: A Literature Review on Technologies for Manufacturing Systems. Engineering Science and Technology, an International Journal 22(3), pp. 899–919, doi:10.1016/j.jestch.2019.01.006. Available at https://www.sciencedirect.com/science/article/ pii/S2215098618317750

work page doi:10.1016/j.jestch.2019.01.006 2019

[4] [5]

7227–7232

Christophe Grand Charles Lesire, David Doose (2020): Formalization of Robot Skills with Descriptive and Operational Models, pp. 7227–7232. doi:10.1109/IROS45743.2020.9340698

arXiv 2020

[5] [6]

Lukas Johannes Dust, Rong Gu, Cristina Seceleanu, Mikael Ekström & Saad Mubeen (2023): Pattern-Based Verification of ROS 2 Nodes Using UPPAAL. In Alessandro Cimatti & Laura Titolo, editors:Formal Methods for Industrial Critical Systems - 28th International Conference, FMICS 2023, Antwerp, Belgium, September 20-22, 2023, Proceedings, 14290, Springer, pp. 5...

work page doi:10.1007/978-3-031-43681-9_4 2023

[6] [7]

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: Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, 8734, Springer, pp. 247–254, doi:10....

doi:10.1007/978-3-319-11164-3_20 2014

[7] [8]

PROSKILL: A formal skill language for acting in robotics

Félix Ingrand (2024): PROSKILL: A formal skill language for acting in robotics . CoRR abs/2403.07770, doi:10.48550/ARXIV .2403.07770

work page Pith review arXiv doi:10.48550/arxiv.2403.07770 2024

[8] [9]

Robotics 7(3), p

André Leite, Andry Maykol Pinto & Aníbal Matos (2018): A Safety Monitoring Model for a Faulty Mobile Robot. Robotics 7(3), p. 32, doi:10.3390/ROBOTICS7030032

work page doi:10.3390/robotics7030032 2018