Pith. sign in

REVIEW 3 major objections 6 minor 65 references

Real-Time Model Checking for Closed-Loop Robot Reactive Planning

T0 review · 3 major / 6 minor · reviewed 2026-08-05 · deepseek-v4-flash

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

Pith's one-line read This paper claims that a purpose-built model checker can generate multi-step obstacle-avoidance plans on a low-powered robot in about 10 ms with no precomputed data, and that two safety properties—no corner trapping and collision-free navig

desk verdict Real, working on-board model-checking planner; the empirical claim holds, but the safety proof has a concrete definitional gap and the no-corner-trap theorem is true by construction. read the letter →

arxiv 2508.19186 v2 pith:TYCCRR24 submitted 2025-08-26 cs.RO cs.AIcs.FL

Christopher Chandler , Bernd Porr , Giulia Lafratta , Alice Miller This is my paper · ORCID
classification cs.ROcs.AIcs.FL
keywords modelcheckingreactiveplanningobstacleavoidanceclosed-loopcontrolLTLLiDARabstractionreal-timemobilerobots
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

Model checking is normally an offline verification tool; this paper turns it into an on-board planner. The authors claim that a small, purpose-built checker can run on a Raspberry Pi-class robot, take the current 2D LiDAR snapshot, reason three or four closed-loop actions ahead, and output an obstacle-avoidance plan in about 10 milliseconds—well inside the 100 ms real-time deadline. The central trick is to abstract each closed-loop "task" (turn left, turn right, drive straight) into a static spatial partition, so the future can be represented by a 15-state transition system and a plan is just a counterexample to an LTL property. If the claims hold, reactive robots can be both fast and explainable, avoiding the corner-trapping failure of one-step reactive controllers without needing precomputed maps.

What carries the argument

The load-bearing object is the disturbance-focused transition system (Definition 1), a 15-state egocentric model whose states are valued at runtime from sensor data. The abstraction renders closed-loop task outcomes as static geometry: LiDAR points are shifted by offsets Δ+ and Δ_L/R to simulate proximal detection and lateral displacement, then filtered into lateral partitions P_L/P_R and longitudinal partitions P_+/P_− (Algorithms 1–2). The planner checks the LTL property φ = ¬(safe U (safe ∧ horizon)) by forming the product of the transition system with a two-state NFA; an accepting path found by forward depth-first search is a safe task sequence, and the shortest such sequence without con

What would settle it

Measure actual lateral displacement over a 200 ms straight-driving step on the real platform; if it is large enough that a LiDAR point could cross the safe-zone boundary between observations, the safe-zone guarantee fails. Alternatively, instrument the executed task sequence in a corridor designed to provoke left-right alternation; any executed pair ⟨T_L, T_R⟩ or ⟨T_R, T_L⟩ would falsify the no-corner-trapping theorem.

Watch

Extended reading notes

Core claim

The central claim is that real-time multi-step planning can be achieved by running model checking inside the robot's control loop. The authors define a disturbance-focused transition system of 15 states whose valuations are computed at runtime from LiDAR observations: obstacles are translated by fixed offsets to predict what the robot will sense after each closed-loop task, and lateral and longitudinal partitions decide whether a straight task has a finite or infinite horizon. Planning is formulated as finding a counterexample to the LTL property ¬(safe U (safe ∧ horizon)), using a two-state NFA and forward depth-first search, so the counterexample path is the robot's plan. In a cul-de-sac s

Load-bearing premise

Everything rests on the assumption that the robot's immediate future can be predicted by rigidly shifting the current LiDAR cloud forward or sideways by fixed offsets, with lateral error effectively zero, in an environment that does not change.

Editorial extensions

If this is right

  • If the central claim is right, on-board model checking can meet hard real-time constraints on a low-powered device: mean latency around 10 ms in the cul-de-sac and at most 21.61 ms for four-step plans, both well below the 100 ms deadline.
  • The collision counts in both scenarios (0 for model checking versus 3 and 6 for the one-step baseline) imply that multi-step reasoning prevents a class of collisions that purely reactive control does not.
  • Because the transition system has no transitions producing alternating left/right pairs, the robot cannot exhibit the corner-trapping behaviour that motivates the paper, regardless of the static environment.
  • The shield-partition theorem implies that, absent lateral error, the robot will always act before a disturbance reaches its safe zone during straight driving—so the safety property is structural, not merely observed.
  • With estimated model-checking memory of about 2.9 KB, the planner leaves most of the Raspberry Pi's RAM free, so the approach is practical for energy-constrained platforms and needs no offline pre-computation.

Reading between the lines

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

  • I would extend the safety claim cautiously: because dsafe, dmax, dmin, and beta are never given numerical values, the informal proofs should be read as conditional on parameter choices; measuring the actual values on the platform would turn them into testable quantitative predictions.
  • The rigid-translation abstraction suggests an immediate stress test on surfaces with slip or camber; if lateral error over a 200 ms step is not negligible relative to dsafe, the safe-zone guarantee probably needs an explicit error bound rather than an assumption.
  • A natural generalisation is target-driven navigation: the paper deliberately omits localisation, but its own discussion notes SLAM can add hundreds of milliseconds, so adding goal-directed behaviour while preserving the latency budget is an open problem.
  • The architecture could be reused as a fast receding-horizon planner in dynamic environments by re-running the checker every control step, but the static-environment assumption in Section 4.2.2 must first be relaxed.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 6 minor

Summary. The paper presents a custom, on-board model-checking planner for a low-cost differential-drive robot with 2D LiDAR. It abstracts closed-loop obstacle-avoidance tasks into spatial partitions, constructs a 15-state disturbance-focused transition system, and uses an NFA for an LTL property to generate multi-step plans by counterexample search via forward depth-first search. Two scenarios (cul-de-sac, playground) compare planning against a one-step reactive baseline using trajectory length, collisions, latency, and memory. Reported processing latency is below 22 ms, with zero collisions for the model-checking method in the collected runs. Two informal theorems claim that the robot cannot get trapped in a corner and that no disturbance can enter the safe zone.

Significance. If the claims hold, the paper is a useful instructional case study showing that a small, purpose-built model checker can run on a low-powered robot in real time. Strengths include the deposited code (Zenodo link), the clear empirical setup, measured latency/memory data, zero collisions in the reported runs, and a transparent LTL/NFA formulation. The main safety theorem, however, is not correct as stated, and the unconditional "collision free navigation is guaranteed" phrasing in §5.5 and §7 overstates the support provided. The paper is also honest about its limitations (static environments, no target-driven behavior, specific hardware), which is welcome. The contribution is modest in scope but potentially publishable after the formal guarantee is repaired and the empirical claims are tempered.

major comments (3)
  1. [§5.4.2, Eq. (15) and Theorem 5.2] P_shield is defined with upper bound vΔt+ε, not d_safe+vΔt+ε. The proof then infers that a disturbance not in P_shield at t−1 satisfies D+_x > d_safe+vΔt+ε; this is not licensed. A stationary disturbance at x0 = vΔt+ε+δ with 0<δ<d_safe, y=0 lies outside P_shield as written, yet after one straight step its relative x-coordinate is δ, inside P_safe (Eq. 14). Thus the safe zone can be penetrated before the shield flags the disturbance. The fix is to define P_shield's longitudinal interval as (d_safe, d_safe+vΔt+ε] and to correct the proof's algebra to D+_x − (vΔt+ε) > d_safe. Since the unconditional safety claim in §5.5 and §7 rests on Theorem 5.2, this is load-bearing.
  2. [§5.4.2, Theorem 5.2 and §5.5] The proof assumes that lateral error is negligible, but no lateral tracking-error measurement is reported and the platform is acknowledged to have a strong right veer (§5.2.1). With differential-drive servos, a few centimeters of lateral drift can move a disturbance into P_shield's lateral band while its x-coordinate is outside the required interval; the proof has no margin for this. Please either provide empirical lateral-error data and set the shield's lateral tolerance accordingly, or state the theorem as conditional on zero lateral error and remove the unconditional "collision free navigation is guaranteed" in §5.5 and §7.
  3. [§5.4.1, Theorem 5.1] The statement uses "subsequence," but the proof only rules out the adjacent ordered pair ⟨T_L,T_R⟩ (and has a typo, repeating ⟨T_L,T_R⟩ twice). The distinction matters: Fig. 9 admits paths such as T_L, T_S, T_R, T0 (via s1→s3→s5), so if "subsequence" is read in the standard non-contiguous sense, the theorem is false as stated. If the intended claim is that avoid tasks never occur consecutively, state this explicitly and repair the proof. If the stronger non-contiguous claim is intended, a different argument is needed.
minor comments (6)
  1. [§4.2 and §5] The numeric values of parameters dsafe, dmax, dmin, β, L+tol, v, and ε are never reported. A parameter table would greatly improve reproducibility, even though code is available.
  2. [Algorithm 3, line 19] The condition "D_L_y ∈ P_L < d_min ∧ D_R_y ∈ P_R > −d_min" is malformed; it should express that the nearest lateral disturbance in each direction is within d_min. Also, Algorithm 2, line 4 uses Δ_y while the input is Δ_L/R.
  3. [Fig. 9 and Definition 1] The edge label "T / T0 S / T0 S" in Fig. 9 is garbled, and some edges have ambiguous labels. Please define all edge labels explicitly in the caption or text.
  4. [§5.1] The baseline method is not fully specified. In particular, it is unclear whether the baseline uses the same safe-zone and P_shield logic or only a single task feedback loop; this matters for interpreting the collision counts.
  5. [Eq. (15)] The use of min(o_x) in P_shield is inconsistent with the pointwise definitions in Eqs. (3)–(12); using o_x would be clearer.
  6. [§5.3.2] The playground scenario reports only two comparisons, apparently one run per method per comparison. The paper should state the number of runs explicitly and avoid generalizing "reliably avoids collisions" from this small sample.

Circularity Check

1 steps flagged · score 2.0 of 10

One 'no corner trap' theorem is built into the transition system by construction; the planning method itself is self-contained and not fitted.

  1. self definitional [Section 5.4.1, proof of Theorem 5.1]
    "By definition, no path in the disturbance-focused transition system𝐷𝑇𝑆 contains⟨𝑇𝐿,𝑇𝑅⟩ or⟨𝑇𝐿,𝑇𝑅⟩, so no subsequence of tasks generated as a plan can contain a subsequence which alternates between tasks𝑇𝐿 and𝑇𝑅."

    The 'cannot get trapped in a corner' guarantee is built into the transition system as a design constraint rather than derived. Getting trapped is defined as alternating TL/TR tasks, and the DTS transition relation is manually defined so that no path labels contain such consecutive pairs. The proof's only step is to point to this 'by definition' absence, so the theorem merely restates the model's construction. It does not derive the property from robot kinematics, sensor geometry, or the model-checking search; it is therefore equivalent to the input model by construction. The paper itself concedes that other trap loops are possible, which confirms the theorem only rules out the designed-out alternating-turn pattern.

full rationale

The planning core is not circular: the LTL property (Eq. 13) and the NFA are used to generate counterexample solution paths from runtime sensor valuations, and no numeric parameter is fitted to the experimental outcomes. The latency, collision, and trajectory-length results are genuine external comparisons against a baseline, so the central empirical claim is self-contained. Self-citations ([10], [34], [47], [48]) are historical/motivational and are not load-bearing: no uniqueness claim, ansatz, or fitted value is imported from them. The only definitional reduction is Theorem 5.1, which proves a property explicitly designed into the disturbance-focused transition system; this is a minor built-in guarantee rather than a fitted prediction. Separately, Theorem 5.2's proof contains a non-circular correctness gap: Eq. 15 defines P_shield with upper bound vΔt+ε, whereas the proof needs D+_x > d_safe+vΔt+ε; a disturbance just beyond one step of travel can enter P_safe before being flagged. That is an algebraic/definitional error in the safety argument, but it is not a circular reduction, so it does not raise the circularity score.

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

The central claim rests on hand-set spatial parameters (dsafe, dmax, dmin, beta, L+tol, v*dt+tol) and on domain assumptions of static environments and negligible lateral error. No new physical entities are introduced. The values of the parameters are not reported, which weakens reproducibility and the strength of the safety guarantees.

free parameters (6)
  • dsafe
    Radius of the egocentric safe zone and bound on longitudinal partitions. Value not reported; critical for safety claims (Equations 3-12, 14-15).
  • dmax
    Maximum lateral look-ahead distance in Equations 3-6. Value not reported; affects which disturbances are considered.
  • dmin
    Minimum lateral clearance used to decide whether the robot is boxed in (Equation 7). Value not reported.
  • beta
    Tunable coefficient in the longitudinal partition bounds (Equations 9-10). Value not reported.
  • L + tol
    Robot width plus tolerance used in lateral bounds of longitudinal partitions (Equations 9-10, 15). Value not reported.
  • v*dt + tol
    Length of the shield partition (Equation 15). Depends on robot velocity and a tolerance term; values not reported.
assumptions (4)
  • domain assumption Environment is static
    Section 4.2.2 states: 'As we restrict our attention to static environments, we can assume that returning to the default task T0 after turning around is safe.' This is load-bearing for the three-step plan logic and for the safety guarantees.
  • domain assumption Lateral error is negligible
    Theorem 5.2 proof: 'As Delta t is around 200 milliseconds, we assume any lateral error is negligible.' This assumption is required for the safe zone guarantee.
  • domain assumption Closed-loop task outcomes can be abstracted by rigid spatial translation of LiDAR data
    Section 4.2: 'we abstract away the timed aspects of closed-loop tasks and represent their continuous evolution with spatial constructions.' The plan predictions rely on translating point clouds by offsets, which may not match real kinematics.
  • standard math Standard LTL/NFA/DFS theory
    Section 3.3 introduces the LTL grammar, NFA acceptance, and product transition system; these are standard results used without proof.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Real-Time Model Checking for Closed-Loop Robot Reactive Planning." pith.science (2026). https://pith.science/paper/TYCCRR24

@misc{pith2026250819186,
  author       = {Pith},
  title        = {Pith review of: Real-Time Model Checking for Closed-Loop Robot Reactive Planning},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/TYCCRR24}},
  note         = {Machine review of arXiv:2508.19186}
}
read the original abstract

Reactive obstacle avoidance methods often cause agents to become trapped in local minima, because they can often only reason one step ahead (i.e., the next action based on the current state). In this paper, we use model checking to achieve reactive multi-step planning and obstacle avoidance on an autonomous robot. Our small, purpose-built model checking algorithm generates plans in situ (within the robot's code) based on ``core'' knowledge and attention as found in biological agents. This is achieved in real-time using no pre-computed data on a low-powered device. Our approach is based on chaining temporary control systems that are spawned to counteract disturbances in the local environment which disrupt an autonomous agent from its preferred action (or resting state). We mitigate state-space explosion by relying on temporary snapshots of the immediate environment, restricting the number of states. Multi-step planning using counter-examples generated by depth-first search and a negated LTL path property is applied to scenarios involving a cul-de-sac and a free-standing obstacle. Empirical results and informal proofs of two fundamental properties demonstrate the effectiveness of our approach for the creation of efficient multi-step plans for local obstacle avoidance. We significantly improve performance compared to a purely reactive agent that can only plan one step ahead. Our approach is an instructional case study for the development of safe and reliable navigation in the context of autonomous vehicles. We believe it also has general application in navigation for mission-critical mobile robots.

Figures

Figures reproduced from arXiv: 2508.19186 by the authors.

Figure 1
Figure 1. A: robot encountering an obstacle in its environment, represented as the disturbance [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Uncertainty in corner situation from the perspective of a closed task feedback loop. A and B: valid [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. A: our robotic platform. B: schematic showing robot dimensions. [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (15 more)
Figure 4
Figure 4. Figure 4: Agent architecture. Red indicates reasoning based on current task outcomes. Blue indicates planning [PITH_FULL_IMAGE:figures/full_fig_p006_4.png]
Figure 5
Figure 5. Figure 5: A: closed-loop execution of the two step sequence [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: A: closed-loop execution of the two step sequence [PITH_FULL_IMAGE:figures/full_fig_p010_6.png]
Figure 7
Figure 7. Figure 7: States for two step sequences. A: lateral partitions with no distal disturbances detected. B: lateral [PITH_FULL_IMAGE:figures/full_fig_p014_7.png]
Figure 8
Figure 8. Figure 8: States for three and four step sequences. A: states for three step sequence. B: states for the final [PITH_FULL_IMAGE:figures/full_fig_p014_8.png]
Figure 9
Figure 9. Figure 9: Disturbance-focused transition system [PITH_FULL_IMAGE:figures/full_fig_p015_9.png]
Figure 10
Figure 10. Figure 10: NFA for the property 𝑠𝑎 𝑓 𝑒 U (𝑠𝑎 𝑓 𝑒 ∧ ℎ𝑜𝑟𝑖𝑧𝑜𝑛). A¬𝜑 = (𝑄, Σ, 𝛿, 𝑄0, 𝐹 ) where 𝑄 = {𝑞0, 𝑞1} is the set of states, Σ = 2 𝐴𝑃 is a finite alphabet, 𝛿 : 𝑄 × Σ → 2 𝑄 is a transition relation, 𝑄0 = {𝑞0} is the initial state, and 𝐹 = {𝑞1} is the accepting state [PITH_FULL_…
Figure 11
Figure 11. Figure 11: A: instance of our transition system showing a valuation of the elements of [PITH_FULL_IMAGE:figures/full_fig_p017_11.png]
Figure 12
Figure 12. Figure 12: A: idealised schematic of cul-de-sac scenario. B: actual cul-de-sac scenario. [PITH_FULL_IMAGE:figures/full_fig_p020_12.png]
Figure 13
Figure 13. Figure 13: The experimental setup. A: the three starting positions (left, centre, right) and placement of the [PITH_FULL_IMAGE:figures/full_fig_p021_13.png]
Figure 14
Figure 14. Figure 14: Trajectory length grouped by method. Next a comparison was made between starting positions. It was reasoned that this could have an influence on the generated trajectory lengths due to differences in starting pose, specifically angle of entry into the cul-de-sac. We p…
Figure 15
Figure 15. Figure 15: Trajectory length grouped by starting position. A: baseline, B: model checking. [PITH_FULL_IMAGE:figures/full_fig_p022_15.png]
Figure 16
Figure 16. Figure 16: A: idealised schematic of playground scenario. B: actual playground. [PITH_FULL_IMAGE:figures/full_fig_p023_16.png]
Figure 17
Figure 17. Figure 17: Comparison 1. A: baseline method. B: planning using model checking. [PITH_FULL_IMAGE:figures/full_fig_p024_17.png]
Figure 18
Figure 18. Figure 18: Comparison 2. A: baseline method. B: planning using model checking (yellow box indicates evasion [PITH_FULL_IMAGE:figures/full_fig_p025_18.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

65 extracted references · 48 canonical work pages

  1. [1]

    Rajeev Alur, Costas Courcoubetis, and David Dill. 1990. Model-checking for real-time systems. In [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science . IEEE, 414–425. doi:10.1109/LICS.1990.113766 Real-Time Model Checking for Closed-Loop Robot Reactive Planning 31

    work page arXiv 1990

  2. [2]

    Christel Baier and Joost-Pieter Katoen. 2008. Principles Of Model Checking . Vol. 950. The MIT Press, Cambridge, Mass. doi:10.1093/comjnl/bxp025 Publication Title: MIT Press ISSN: 00155713

    doi:10.1093/comjnl/bxp025 2008

  3. [3]

    Davide Basile, Alessandro Fantechi, and Irene Rosadi. 2021. Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer. In Formal Methods for Industrial Critical Systems , Alberto Lluch Lafuente and Anastasia Mavridou (Eds.). Springer International Publishing, Cham, 174–190

    work page 2021

  4. [4]

    Battaglia, Jessica B

    Peter W. Battaglia, Jessica B. Hamrick, and Joshua B. Tenenbaum. 2013. Simulation as an engine of physical scene understanding. Proceedings of the National Academy of Sciences 110, 45 (2013), 18327–18332. doi:10.1073/pnas. 1306572110 arXiv:https://www.pnas.org/doi/pdf/10.1073/pnas.1306572110

    doi:10.1073/pnas 2013

  5. [5]

    Myreen, and André Platzer

    Rose Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen, and André Platzer. 2018. VeriPhy: verified controller executables from verified cyber-physical system models. SIGPLAN Not. 53, 4 (June 2018), 617–630. doi:10.1145/3296979. 3192406

    work page doi:10.1145/3296979 2018

  6. [6]

    Sara Bouraine, Abdelhak Bougouffa, and Ouahiba Azouaoui. 2022. Particle swarm optimization for solving a scan- matching problem based on the normal distributions transform. Evolutionary Intelligence 15, 1 (3 2022), 683–694. doi:10.1007/S12065-020-00545-Y/FIGURES/8

    work page doi:10.1007/s12065-020-00545-y/figures/8 2022

  7. [7]

    Sara Bouraine, Thierry Fraichard, and Hassen Salhi. 2012. Provably safe navigation for mobile robots with limited field- of-views in dynamic environments. Autonomous Robots 32, 3 (01 Apr 2012), 267–283. doi:10.1007/s10514-011-9258-8

    work page doi:10.1007/s10514-011-9258-8 2012

  8. [8]

    Braitenberg

    V. Braitenberg. 1986. Vehicles: Experiments in Synthetic Psychology . MIT Press, Cambridge, Massachussets

    work page 1986

Show all 65 references
  1. [9]

    R. C. Cardoso, G. Kourtis, L. A. Dennis, C. Dixon, M. Farrell, M. Fisher, and M. Webster. 2021. A Review of Verification and Validation for Space Autonomous Systems. Current Robotics Reports 2, 3 (2021), 273—-283. doi:10.1007/s43154-021- 00058-1

    2021 doi

  2. [10]

    Christopher Chandler, Bernd Porr, Alice Miller, and Giulia Lafratta. 2023. Model Checking for Closed-Loop Robot Reactive Planning. Electronic Proceedings in Theoretical Computer Science 395 (Nov. 2023), 77–94. doi:10.4204/eptcs.395.6

    2023 doi

  3. [11]

    Li Chen, Penghao Wu, Kashyap Chitta, Bernhard Jaeger, Andreas Geiger, and Hongyang Li. 2024. End-to-End Autonomous Driving: Challenges and Frontiers. IEEE Transactions on Pattern Analysis and Machine Intelligence 46, 12 (2024), 10164–10183. doi:10.1109/TPAMI.2024.3435937

    2024

  4. [12]

    François Chollet. 2019. On the Measure of Intelligence. doi:10.48550/arXiv.1911.01547 arXiv:1911.01547 [cs]

    2019 doi arXiv

  5. [13]

    Silvano Dal Zilio, Pierre-Emmanuel Hladik, Félix Ingrand, and Anthony Mallet. 2023. A formal toolchain for offline and run-time verification of robotic systems. Robotics and Autonomous Systems 159 (2023), 104301. doi:10.1016/j.robot. 2022.104301

    2023

  6. [14]

    Werner Damm, Eike Möhlmann, Thomas Peikenkamp, and Astrid Rakow. 2018. A Formal Semantics for Traffic Sequence Charts. In Principles of Modeling, Marten Lohstroh, Patricia Derler, and Marjan Sirjani (Eds.). Vol. 10760. Springer International Publishing, 182–205. doi:10.1007/97...

    2018 doi

  7. [15]

    Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikučionis, and Jakob Haahr Taankvist. 2015. Uppaal Stratego. In Tools and Algorithms for the Construction and Analysis of Systems , Christel Baier and Cesare Tinelli (Eds.). Vol. 9035. Springer Berlin Heidelber...

    2015 doi

  8. [16]

    Dennis, Michael Fisher, Matthew P

    Louise A. Dennis, Michael Fisher, Matthew P. Webster, and Rafael H. Bordini. 2012. Model checking agent programming languages. Automated Software Engineering 19, 1 (March 2012), 5–63. doi:10.1007/s10515-011-0088-x

    2012 doi

  9. [17]

    Ankush Desai, Tommaso Dreossi, and Sanjit A. Seshia. 2017. Combining Model Checking and Runtime Verification for Safe Robotics. In Runtime Verification, Shuvendu Lahiri and Giles Reger (Eds.). Springer International Publishing, Cham, 172–189

    2017

  10. [18]

    Joint Research Centre

    European Commission. Joint Research Centre. 2021. Trustworthy autonomous vehicles: assessment criteria for trustworthy AI in the autonomous driving domain. https://data.europa.eu/doi/10.2760/120385

    2021 doi

  11. [19]

    Marie Farrell and Matt Luckcuck (Eds.). 2021. Proceedings of the Third Workshop on Formal Methods for Autonomous Systems. Vol. 348. Open Publishing Association. doi:10.4204/eptcs.348

    2021 doi

  12. [20]

    L. E. R. Fernandes, V. Custodio, G. V. Alves, and M. Fisher. 2017. A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification. Electronic Proceedings in Theoretical Computer Science 257 (2017), 35–42. doi:10.1007/978-94-015-9204-8

    2017 doi

  13. [21]

    Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini, and Viviana Mascardi

    Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini, and Viviana Mascardi

  14. [22]

    Dennis, Davide Ancona, Michael Fisher, and Viviana Mascardi

    Angelo Ferrando, Louise A. Dennis, Davide Ancona, Michael Fisher, and Viviana Mascardi. 2018. Verifying and Validating Autonomous Systems: Towards an Integrated Approach. InRuntime Verification, Christian Colombo and Martin Leucker (Eds.). Springer International Publishing, Ch...

    2018

  15. [23]

    Mohammed Foughali, Saddek Bensalem, Jacques Combaz, and Félix Ingrand. 2020. Runtime Verification of Timed Properties in Autonomous Robots. In 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE). 1–12. doi:10.1109/MEMOCODE51338...

    2020

  16. [24]

    Fraser, R

    D. Fraser, R. Giaquinta, Hoffmann, M. Ireland, A. Miller, and G. Norman. 2020. Collaborative models for autonomous systems controller synthesis. Form Aspects of Computing 32 (2020), 157—-186. doi:10.1109/TCST.2006.872519

    2020

  17. [25]

    Rong Gu, Cristina Seceleanu, Eduard Enoiu, and Kristina Lundqvist. 2021. Model Checking Collision Avoidance of Nonlinear Autonomous Vehicles. In Formal Methods, Marieke Huisman, Corina Păsăreanu, and Naijun Zhan (Eds.). Springer International Publishing, Cham, 676–694

    2021

  18. [26]

    Hamilton, I

    J. Hamilton, I. Stefanakos, R. Calinescu, and J. Cámara. 2022. Towards Adaptive Planning of Assistive-care Robot Tasks. In Electronic Proceedings in Theoretical Computer Science , Matt Luckcuck and Marie Farrell (Eds.), Vol. 371. Open Publishing Association, 175–183. doi:10.42...

    2022 doi

  19. [27]

    Havelund, M

    K. Havelund, M. Lowry, and J. Penix. 2001. Formal Analysis of a Space-Craft Controller Using SPIN. Software Engineering, IEEE Transactions on 27 (09 2001), 749–765. doi:10.1109/32.940728

    2001 doi

  20. [28]

    Hendriks, P

    M. Hendriks, P. Petterson, J. Hakansson, K.G. Larsen, A. David, G. Behrmann, Wang Yi, P. Petterson, J. Hakansson, K.G. Larsen, A. David, G. Behrmann, M. Hendriks, and Wang Yi. 2006. UPPAAL 4.0. In Third International Conference on the Quantitative Evaluation of Systems - (QEST...

    2006 doi

  21. [29]

    Henzinger, Pei-Hsin Ho, and Howard Wong-Toi

    Thomas A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. 1997. HyTech: A model checker for hybrid systems. In Computer Aided Verification, Orna Grumberg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 460–463

    1997

  22. [30]

    Holzmann

    G. Holzmann. 2011. The SPIN Model Checker: Primer and Reference Manual (1st ed.). Addison-Wesley Professional

    2011

  23. [31]

    Xuemin Hu, Shen Li, Tingyu Huang, Bo Tang, Rouxing Huai, and Long Chen. 2023. How Simulation Helps Autonomous Driving:A Survey of Sim2real, Digital Twins, and Parallel Intelligence. doi:10.48550/arXiv.2305.01263 arXiv:2305.01263 [cs]

    2023 doi arXiv

  24. [32]

    Jeff Huang, Cansu Erdogan, Yi Zhang, Brandon Moore, Qingzhou Luo, Aravind Sundaresan, and Grigore Rosu. 2014. ROSRV: Runtime Verification for Robots. In Runtime Verification, Borzoo Bonakdarpour and Scott A. Smolka (Eds.). Springer International Publishing, 247–254

    2014

  25. [33]

    Dennis, Owen McAree, Michael Fisher, and Sandor M

    Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher, and Sandor M. Veres. 2017. Formal verification of autonomous vehicle platooning. Science of Computer Programming 148 (2017), 88–106. doi:10.1016/j.scico.2017.05.006 Special issue on Automated Verification of Critica...

    2017 doi

  26. [34]

    Giulia Lafratta, Bernd Porr, Christopher Chandler, and Alice Miller. 2025. Closed-loop multi-step planning. Neural Computation (forthcoming) (2025)

    2025

  27. [35]

    Lake, Tomer D

    Brenden M. Lake, Tomer D. Ullman, Joshua B. Tenenbaum, and Samuel J. Gershman. 2017. Building machines that learn and think like people. Behavioral and Brain Sciences 40 (2017), e253. doi:10.1017/S0140525X16001837

    2017 doi

  28. [36]

    Yann LeCun. 2022. A Path Towards Autonomous Machine Intelligence | OpenReview. https://openreview.net/forum? id=BZ5a1r-kVsf

    2022

  29. [37]

    Lehmann, A

    S. Lehmann, A. Rogalla, M. Neidhardt, A. Schlaefer, and S. Schupp. 2021. Online Strategy Synthesis for Safe and Optimized Control of Steerable Needles, See [19], 128–135. doi:10.4204/EPTCS.348.9

    2021 doi

  30. [38]

    Leonard and H.F

    J.J. Leonard and H.F. Durrant-Whyte. 1991. Simultaneous map building and localization for an autonomous mobile robot. In Proceedings IROS ’91:IEEE/RSJ International Workshop on Intelligent Robots and Systems ’91 . 1442–1447 vol.3. doi:10.1109/IROS.1991.174711

    1991

  31. [39]

    Bo Li, Yingqiang Wang, Yu Zhang, Wenjie Zhao, Jianyuan Ruan, and Ping Li. 2020. GP-SLAM: laser-based SLAM approach based on regionalized Gaussian process map reconstruction. Autonomous Robots 44, 6 (7 2020), 947–967. doi:10.1007/S10514-020-09906-Z/FIGURES/26

    2020 doi

  32. [40]

    Xiaohui Li, Zhenping Sun, Dongpu Cao, Zhen He, and Qi Zhu. 2016. Real-Time Trajectory Planning for Autonomous Urban Driving: Framework, Algorithms, and Verifications. IEEE/ASME Transactions on Mechatronics 21, 2 (April 2016), 740–753. doi:10.1109/TMECH.2015.2493980

    2016

  33. [41]

    Qin Lin, Stefan Mitsch, André Platzer, and John M. Dolan. 2022. Safe and Resilient Practical Waypoint-Following for Autonomous Vehicles. IEEE Control Systems Letters 6 (2022), 1574–1579. doi:10.1109/LCSYS.2021.3125717

    2022

  34. [42]

    Haque, Lingjia Tang, and Jason Mars

    Shih-Chieh Lin, Yunqi Zhang, Chang-Hong Hsu, Matt Skach, Md E. Haque, Lingjia Tang, and Jason Mars. 2018. The Architectural Implications of Autonomous Driving: Constraints and Acceleration. In Proceedings of the Twenty-Third International Conference on Architectural Support fo...

    2018

  35. [43]

    Liu, Hendrik Roehm, Christian Heinzemann, Ingo Lütkebohle, Jens Oehlerking, and Matthias Althoff

    Stefan B. Liu, Hendrik Roehm, Christian Heinzemann, Ingo Lütkebohle, Jens Oehlerking, and Matthias Althoff. 2017. Provably safe motion of mobile robots in human environments. In 2017 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) . 1351–1357. doi:10...

    2017

  36. [44]

    Dennis Louise, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa, and Sandor Veres. 2016. Practical verification of decision- making in agent-based autonomous systems.Automated Software Engineering 23, 3 (2016), 305–359. doi:10.1007/s10515- 014-0168-9 Real-Time Model Checking f...

    2016 doi

  37. [45]

    Y. Lu, A. Miller, C. Johnson, Z. Peng, and T. Zhao. 2014. Availability analysis of satellite positioning systems for avaiation using the Prism model checker. In Proceedings of the 17th International Conference on Computational Science and Engineering (CSE 2014) . 704–713. doi:...

    2014 doi

  38. [46]

    Dennis, Clare Dixon, and Michael Fisher

    Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, and Michael Fisher. 2019. A Summary of Formal Specification and Verification of Autonomous Robotic Systems. In Integrated Formal Methods, Wolfgang Ahrendt and Silvia Lizeth Tapia Tarifa (Eds.). Springer International...

    2019

  39. [47]

    Alice Miller, Bernd Porr, Ivaylo Valkov, Douglas Fraser, and Daumantas Pagojus. 2025. Model checking with memoisa- tion for fast overtaking planning. Science of Computer Programming 244 (2025), 103300. doi:10.1016/j.scico.2025.103300

    2025

  40. [48]

    Daumantas Pagojus, Alice Miller, Bernd Porr, and Ivaylo Valkov. 2021. Simulation and Model Checking for Close to Realtime Overtaking Planning, See [19], 20–37. doi:10.4204/EPTCS.348.2

    2021 doi

  41. [49]

    Christian Pek, Stefanie Manzinger, Markus Koschi, and Matthias Althoff. 2020. Using online verification to prevent autonomous vehicles from causing accidents. Nature Machine Intelligence 2, 9 (01 Sep 2020), 518–528. doi:10.1038/ s42256-020-0225-y

    2020

  42. [50]

    Gang Peng, Yicheng Zhou, Lu Hu, Li Xiao, Zhigang Sun, Zhangang Wu, and Xukang Zhu. 2023. VILO SLAM: Tightly Coupled Binocular Vision–Inertia SLAM Combined with LiDAR. Sensors 2023, Vol. 23, Page 4588 23, 10 (5 2023), 4588. doi:10.3390/S23104588

    2023 doi

  43. [51]

    Bernd Porr and Florentin Wörgötter. 2005. Inside embodiment – what means embodiment to radical constructivists? Kybernetes 34, 1 (2005), 105–117. doi:10.1108/03684920510575762

    2005 doi

  44. [52]

    P. J. Ramadge and W. M. Wonham. 1987. Supervisory Control of a Class of Discrete Event Processes. SIAM Journal on Control and Optimization 25, 1 (1987), 206–230. doi:10.1137/0325013 arXiv:https://doi.org/10.1137/0325013

    1987 doi

  45. [53]

    Yingying Ran, Xiaobin Xu, Zhiying Tan, and Minzhou Luo. 2025. A Review of 2D Lidar SLAM Research. Remote Sensing 2025, Vol. 17, Page 1214 17, 7 (3 2025), 1214. doi:10.3390/RS17071214

    2025 doi

  46. [54]

    Smith and Peter Cheeseman

    Randall C. Smith and Peter Cheeseman. 1986. On the Representation and Estimation of Spatial Uncer- tainty. The International Journal of Robotics Research 5, 4 (1986), 56–68. doi:10.1177/027836498600500404 arXiv:https://doi.org/10.1177/027836498600500404

    1986 doi

  47. [55]

    Spelke and Katherine D

    Elizabeth S. Spelke and Katherine D. Kinzler. 2007. Core knowledge. Developmental Science 10, 1 (1 2007), 89–96. doi:10.1111/J.1467-7687.2007.00569.X

    2007

  48. [56]

    Huihui Sun, Weijie Zhang, Runxiang Yu, and Yujie Zhang. 2021. Motion Planning for Mobile Robots—Focusing on Deep Reinforcement Learning: A Systematic Review. IEEE Access 9 (2021), 69061–69081. doi:10.1109/ACCESS.2021.3076530

    2021

  49. [57]

    Güliz Tuncay, Soteris Demetriou, Karan Ganju, and Carl A. Gunter. 2018. Resolving the Predicament of Android Custom Permissions. In Network and Distributed System Security Symposium . 1–15. doi:10.14722/ndss.2018.23221

    2018

  50. [58]

    Moshe Y. Vardi. 1988. An automata-theoretic approach to protocol verification. In CONCURRENCY 88, Frederich H. Vogt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 73–73

    1988

  51. [59]

    Wang and F

    L. Wang and F. Cai. 2017. Reliability analysis for flight control systems using probabilistic model checking.Proceedings of the IEEE International Conference on Software Engineering and Service Sciences, ICSESS 2017-Novem (2017), 161–164. doi:10.1109/RAM.2017.7889773

    2017

  52. [60]

    Ammar, and Tianyao Shen

    Weichen Wei, Bijan Shirinzadeh, Rohan Nowell, Mohammadali Ghafarian, Mohamed M.A. Ammar, and Tianyao Shen

  53. [61]

    Weißmann, S

    M. Weißmann, S. Bedenk, C. Buckl, and A. Knoll. 2011. Model Checking Industrial Robot Systems. In Model checking software (SPIN 2011), Vol. 6823. Springer Berlin Heidelberg, 161–176

    2011

  54. [62]

    Kelvin Wong, Yanlei Gu, and Shunsuke Kamijo. 2021. Mapping for Autonomous Driving: Opportunities and Challenges. IEEE Intelligent Transportation Systems Magazine 13, 1 (2021), 91–106. doi:10.1109/MITS.2020.3014152

    2021

  55. [63]

    Bin Zhang, Zexin Peng, Bi Zeng, and Junjie Lu. 2024. 2DLIW-SLAM:2D LiDAR-inertial-wheel odometry with real-time loop closure. Measurement Science and Technology 35, 7 (4 2024), 075205. doi:10.1088/1361-6501/AD3EA3

    2024 doi

  56. [2020]

    In Towards Autonomous Robotic Systems: 21st Annual Conference, TAROS 2020, Nottingham, UK, September 16, 2020, Proceedings (Nottingham, United Kingdom)

    ROSMonitoring: A Runtime Verification Framework for ROS. In Towards Autonomous Robotic Systems: 21st Annual Conference, TAROS 2020, Nottingham, UK, September 16, 2020, Proceedings (Nottingham, United Kingdom). Springer-Verlag, Berlin, Heidelberg, 387–399. doi:10.1007/978-3-030...

    2020 doi

  57. [2021]

    Sensors 2021, Vol

    Enhancing Solid State LiDAR Mapping with a 2D Spinning LiDAR in Urban Scenario SLAM on Ground Vehicles. Sensors 2021, Vol. 21, Page 1773 21, 5 (3 2021), 1773. doi:10.3390/S21051773

    2021 doi

Pith tools

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