Pith. sign in

REVIEW 4 major objections 5 minor 33 references

Symbolic Control for Autonomous Docking of Marine Surface Vessels

T0 review · 4 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Pith's one-line read A hierarchical symbolic controller docks a model vessel with formal safety guarantees.

desk verdict Real-time symbolic control is demonstrated on a physical vessel, and that is genuinely new; the formal guarantee, however, only covers the kinematic model, not the hardware. read the letter →

arxiv 2501.13199 v2 pith:VBUCZJNG submitted 2025-01-22 eess.SY cs.SY

classification eess.SYcs.SY
keywords autonomousdockingsymboliccontrolformalsafetyguaranteesfeedbackrefinementrelationreal-timecontrollersynthesisGPUaccelerationmarinesurfacevesseldynamicpositioning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper sets out to show that a hierarchical controller can give autonomous docking of a marine surface vessel genuinely formal safety guarantees, not just heuristic behavior. The key idea is to treat the vessel's desired surge, sway, and yaw velocities as control inputs, abstract the kinematic model into a finite symbolic system, and synthesize a controller on that abstraction that is then refined back to the real model. Because the abstraction over-approximates obstacles and under-approximates the target, any controller that solves the abstract problem guarantees that the real vessel avoids obstacles and reaches the docking target. The authors further claim that GPU-accelerated synthesis makes this feasible in real time, with re-synthesis taking about 0.5 seconds, and they support the claim with simulations and, for the first time, physical experiments on a scale-model vessel.

What carries the argument

The central object is the feedback refinement relation $Q$ between the plant $S_1$ (the kinematic model $\dot{\eta}=R(\eta_\psi)\nu$) and a finite-state abstraction $S_2$. The relation ensures that every behavior of the plant is mirrored by a behavior of the abstraction, so safety synthesized on $S_2$ transfers to $S_1$. The synthesis itself is a standard graph search over the abstract states, accelerated by a GPU-based parallel kernel to run in about 0.5 seconds; a cost function $J(\sigma_i)=\beta(\sigma_i)^\top W_i\beta(\sigma_i)$ then selects the most practical action from the list of safe ones, favoring forward motion and smooth heading changes.

What would settle it

Run a docking maneuver in the towing tank while logging commanded and realized velocities; if the measured tracking error ever exceeds the margin that the abstraction's obstacle over-approximation assumed, the vessel could be pushed outside the safe set, and the formal guarantee for the physical system would not follow.

Watch

Extended reading notes

Core claim

The central claim is that the feedback refinement relation between the 3-DOF kinematic vessel model and a finite abstraction transfers safety from the abstract to the real system. If an abstract controller solves the abstract docking problem—avoid the over-approximated obstacles and reach the under-approximated target—then the refined controller solves the actual problem and returns a list of all safe control actions at every step. The paper demonstrates that this synthesis can be performed and repeated in real time on a GPU, and that the resulting controller successfully docks a scale-model vessel in a towing tank while avoiding static obstacles. The authors state the formal guarantee explicitly: under the assumptions that the low-level loop realizes any commanded velocity and the kinematic model covers all real-world behavior, the synthesized velocity commands maintain vessel safety by construction.

Load-bearing premise

The load-bearing premise is that the vessel's low-level velocity controller can realize whatever surge, sway, and yaw velocity the symbolic controller commands, and that the kinematic model captures every behavior that matters for safety.

Editorial extensions

If this is right

  • Any control action on the synthesized list is safe with respect to the obstacles, so the choice among them can be optimized without re-verification.
  • Re-synthesis every 0.5 seconds lets the controller adapt to a changing environment, such as moving obstacles or a shifted target.
  • The finite abstraction means the same synthesis procedure applies to larger and more complex docking regions, with computational cost shifted to the abstraction size.
  • Successful physical experiments indicate that symbolic control can leave the simulation domain and run on real hardware with modest onboard computation.

Reading between the lines

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

  • If the tracking-error bound were formally incorporated via a continuous abstraction, the same architecture could give guarantees for the closed-loop kinetic plant, not just the kinematic model.
  • The real-time synthesis rate could serve as a safety filter for other planning algorithms, checking their proposed velocity commands against the abstract safe set before execution.
  • Treating obstacle positions as additional state variables and re-synthesizing at the demonstrated rate would extend the approach to moving obstacles without changing the core machinery.
  • The performance of the scheme on full-scale vessels would depend on the accuracy of the kinematic model and on communication latency; the current experiments do not yet address those scales.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 5 minor

Summary. The paper proposes a hierarchical control architecture for autonomous docking of marine surface vessels. The upper-level controller uses symbolic control over a 3-DOF kinematic model (Eq. 1), synthesizing safe velocity commands in real time on a GPU; the lower level is a MIMO PID velocity controller with thrust allocation and an EKF. The authors claim formal, correct-by-construction safety guarantees via a feedback refinement relation from [18], and they validate the scheme in simulation and in ten physical trials with a scaled model vessel. The paper also presents a cost-based optimization over the synthesized safe action set and reports roughly 0.5-second re-synthesis times.

Significance. If the formal guarantee were fully established for the physical system, this would be a meaningful step toward practically deployable, verifiable autonomous docking: real-time symbolic synthesis on a physical vessel with static obstacles is genuinely novel in the marine control literature. The experimental demonstration, including ten successful docking runs, is a valuable contribution, and the use of GPU acceleration for re-synthesis addresses a well-known scalability bottleneck of symbolic control. The paper is also honest about several limitations, particularly the tracking-error issue in Section VI, which is commendable. However, the asserted safety guarantee currently holds rigorously only for the abstract kinematic model, not for the closed-loop physical vessel, and the abstraction parameters needed to check the refinement relation are not reported.

major comments (4)
  1. [Section V and Section VI] The formal guarantee for the physical vessel is not established as stated. Section V explicitly assumes that the low-level control system can realize any commanded velocity and that the kinematic model (Eq. 1) encompasses all real-world behavior, but Section VI reports nonzero tracking error (nu_MSE = [0.00768 m/s, 0.00431 m/s, 0.62108 deg/s]) and concedes that this error was not formally accounted for. Since the feedback refinement relation theorem from [18] applies to the kinematic plant (Eq. 1), not to the closed loop of the kinetic model (Eq. 2), PID controller, thrust allocation, and EKF, the abstraction-based safety guarantee does not transfer to the real vessel unless a verified bound on the tracking error is incorporated into the abstraction margins. The ten successful experiments are empirical evidence, not a formal proof. This is the load-bearing gap that must be addressed.
  2. [Section III-A] The paper does not provide the abstraction parameters needed to verify that the feedback refinement relation from [18] actually holds for the vessel model (Eq. 1). In particular, the quantizer (grid size and type), the discrete input set, the sampling/update period, and the transition relation of the abstract system S2 are not specified. Without these details, a reader cannot check the hypotheses of Theorem III.5 of [18], nor reproduce the synthesis results. Please report these parameters explicitly, including how the 2-second update period relates to the abstraction sampling time and to the low-level settling time.
  3. [Section III-A and Fig. 3] The obstacle over-approximation margins (O1_2, O2_2) and the target under-approximation margin (T2) are described qualitatively but never quantified. These margins are essential to the safety claim because they must absorb not only the vessel geometry but also any uncertainty in obstacle position and any unmodeled tracking error. Please provide the numerical values used in the experiments and state which physical effects each margin is intended to cover. If the margins were chosen only from preliminary observations, that should be stated explicitly and their effect on the guarantee assessed.
  4. [Section IV-A and Section VI] The statement in Section VI that the tracking error could be handled by a continuous abstraction as in [23] is a proposal for future work, not an established property of the current system. As written, the claim in Section V that the synthesized velocity commands are 'theoretically guaranteed to maintain vessel safety' under the stated assumptions is conditional on assumptions that are quantifiably false in the experiments. Please either weaken the safety claim to apply only to the kinematic model, or extend the abstraction to include a verified bound on the low-level tracking error.
minor comments (5)
  1. [Abstract and Section I] The phrase 'for the first time' in the abstract and contributions is used for physical experiments of symbolic control on a scale model vessel; please clarify whether this refers to symbolic control for docking specifically, since the current wording is open to a broader interpretation.
  2. [Section IV-E] Equation (7) defines W_i conditionally on the sign of the forward velocity component, but the text says 'W is chosen conditionally based on the forward velocity component of the proposed control action, sigma_i_nu_x' without noting that the two branches of W_i are both used in the same experiment; please make this explicit.
  3. [Section V] There is a typo in 'minium' (should be 'minimum') and in 're-sythesizes' (should be 're-synthesizes'). Also, 'apx.' is informal; consider writing 'approximately'.
  4. [Fig. 3 and Fig. 7] The figure labels O1_1, O2_1, O1_2, O2_2, T1, T2 are hard to read in the printed version; please increase font sizes or use a legend that is legible after typesetting.
  5. [Section III-B] Please define the notation nu_ref and nu_MSE at first use, and ensure that the units for yaw error are consistently stated (rad/s vs deg/s). Currently Section VI reports yaw MSE in deg/s while Section II defines angular velocities in rad/s.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: the docking-safety claim rests on an external abstraction theorem [18] and is conditional on stated assumptions, not on fitted parameters or self-citations.

full rationale

The derivation chain is not circular. The correctness of the symbolic controller over the kinematic model is imported from the external feedback-refinement-relation theorem of Reissig, Weber, and Rungger [18], which is not a self-citation and does not depend on the present paper's fitted quantities. The physical-system safety claim is explicitly conditional: Section V states the assumptions that the low-level loop realizes any commanded velocity and that the kinematic model encompasses all real-world vessel behaviors. A conditional guarantee is not circular even if the antecedent is idealized. Section VI honestly discloses that the tracking error was not formally accounted for and proposes a continuous abstraction as future work; this is a limitation in transferring the guarantee to hardware, not a reduction of the conclusion to the inputs. The cost weights W in Eq. (7) are hand-tuned based on design iterations and preliminary observations, but they only select among actions that are already certified safe by the abstraction; they do not define or determine the safety property, so they are not fitted parameters renamed as predictions. Self-citations to pFaces [21] and earlier docking work [23] are implementation/context citations and are not load-bearing; the load-bearing correctness argument is external [18]. No equation or construction in the paper makes the stated output equal to the input by definition. Therefore, no significant circularity is present.

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

The central claim rests on the abstraction theorem from [18], the kinematic-model idealization, and the untested assumption that the low-level loop tracks any velocity command. The only hand-fitted quantity entering the control policy is the cost matrix W (Eq. 7); the abstraction grid and obstacle margins are not disclosed, so the formal guarantee cannot be checked from the paper alone. No new physical entities are introduced.

free parameters (5)
  • Cost matrix W (Eq. 7) = diag(7.5,3,1,1,1,2.5) or diag(1,6,1,1,1,2.5)
    Chosen conditionally on the sign of forward velocity through domain specific knowledge and design iterations (Section IV-E); tunes which safe action is selected, affecting trajectory shape and experiment outcomes, but not the formal safety property.
  • Abstraction quantization parameters
    The finite state and input sets S2 are created by grids; the paper never reports cell sizes, sampling time, or input discretization, so the abstraction used for the formal guarantee cannot be reconstructed.
  • Obstacle over-approximation and target under-approximation margins
    Fig. 3 and Section III-A introduce margins O2 and T2 to account for the geometrical shape of the vessel; without numerical values, the conservativeness of the safety guarantee is unspecified.
  • Control update period = 2 s
    Selected to account for the settling time of the low-level velocity controller (Section III-A); determines how often re-synthesis occurs and thus the dynamic responsiveness.
  • Input and state bounds U1, X1 = U1 = [-0.1,0.2] x [-0.1,0.1] x [-0.2,0.2], X1 = [-3.5,4.5] x [-3.0,3.0] x [-pi,pi)
    Chosen from the testing arena and vessel capabilities (Section IV-A); these bounds define the operating envelope of the controller.
assumptions (4)
  • standard math Theorem III.5 of [18]: if the abstract controller solves the abstract control problem, the refined controller solves the actual problem under a feedback refinement relation.
    Invoked in Section III-A without proof; provides the correctness transfer from S2 to S1.
  • domain assumption The 3-DOF kinematic model (1) with desired velocities as control inputs captures all vessel behavior relevant to docking safety.
    Assumed in Section V; ignores kinetic dynamics, actuator limits, and environmental loads.
  • domain assumption The low-level velocity controller realizes any commanded surge, sway, and yaw velocity exactly.
    Stated assumption in Section V; contradicted by the nonzero tracking error reported in Section VI, so the formal guarantee applies only under this idealization.
  • domain assumption Obstacles are static, perfectly known, and no environmental disturbances act on the vessel.
    The specification (3) and experiments use fixed obstacle sets; waves and wind are deferred to future work.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Symbolic Control for Autonomous Docking of Marine Surface Vessels." pith.science (2026). https://pith.science/paper/VBUCZJNG

@misc{pith2026250113199,
  author       = {Pith},
  title        = {Pith review of: Symbolic Control for Autonomous Docking of Marine Surface Vessels},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VBUCZJNG}},
  note         = {Machine review of arXiv:2501.13199}
}
read the original abstract

We develop a hierarchical control architecture for autonomous docking maneuvers of a dynamic positioning vessel and provide formal safety guarantees. At the upper-level, we treat the vessel's desired surge, sway, and yaw velocities as control inputs and synthesize a symbolic controller in real-time. The desired velocities are then executed by the vessel's low-level velocity feedback control loop. We next investigate methods to optimize the performance of the proposed control scheme. The results are evaluated on a simulation model of a marine surface vessel in the presence of static obstacles and, for the first time, through physical experiments on a scale model vessel.

Figures

Figures reproduced from arXiv: 2501.13199 by the authors.

Figure 1
Figure 1. Symbolic control architecture for Dynamic Positioning (DP) vessels. [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Closed loop: abstraction, refinement, and optimization. [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 4
Figure 4. Possible transitions from vessel state (solid circle) to locations [PITH_FULL_IMAGE:figures/full_fig_p003_4.png] view at source ↗
Figures from the paper (4 more)
Figure 3
Figure 3. Figure 3: Discretized system with boundary B = 8m × 6m and states of S1 and S2. S1 has obstacles O1 1 and O2 1 (dark orange) and target docking position, T1 (dark green). S2 has obstacles O1 2 and O2 2 (light orange) and target docking position, T2 (light green). S2 is connected…
Figure 5
Figure 5. Figure 5: The low-level velocity control loop of the DP control system. [PITH_FULL_IMAGE:figures/full_fig_p004_5.png]
Figure 6
Figure 6. Figure 6: (a) Marine Cybernetics Laboratory (MCLab) where experiments [PITH_FULL_IMAGE:figures/full_fig_p004_6.png]
Figure 7
Figure 7. Figure 7: The yellow rectangles portray 3 meter obstacles, and the green box [PITH_FULL_IMAGE:figures/full_fig_p005_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

33 extracted references · 31 canonical work pages

  1. [18]

    Feedback refinement relations for the synthesis of symbolic controllers,

    G. Reissig, A. Weber, and M. Rungger, “Feedback refinement relations for the synthesis of symbolic controllers,” IEEE Transactions on Automatic Control, vol. 62, no. 4, pp. 1781–1796, 2016

  2. [23]

    Continuous and discrete abstractions for planning, applied to ship docking,

    P.-J. Meyer, H. Yin, A. H. Brodtkorb, M. Arcak, and A. J. Sørensen, “Continuous and discrete abstractions for planning, applied to ship docking,” IFAC-PapersOnLine, vol. 53, no. 2, pp. 1831–1836, 2020

  3. [1]

    Towards the assessment of potential impact of unmanned vessels on maritime transportation safety,

    K. Wróbel, J. Montewka, and P. Kujala, “Towards the assessment of potential impact of unmanned vessels on maritime transportation safety,” Reliability Engineering & System Safety , vol. 165, pp. 155– 169, 2017

  4. [2]

    A survey of dynamic positioning control systems,

    A. J. Sørensen, “A survey of dynamic positioning control systems,” Annual reviews in control , vol. 35, no. 1, pp. 123–136, 2011

  5. [3]

    Annual overview of marine casualties and incidents 2024,

    European Maritime Safety Agency, “Annual overview of marine casualties and incidents 2024,” EMSA, Technical report, 2024

  6. [4]

    Automated docking for marine surface vessels—a survey,

    S. J. N. Lexau, M. Breivik, and A. M. Lekkas, “Automated docking for marine surface vessels—a survey,” IEEE Access, vol. 11, 2023

  7. [5]

    Long-range UWB positioning based automatic docking trajectory design for unmanned surface vehicle,

    W. Cai, M. Zhang, Q. Yang, C. Wang, and J. Shi, “Long-range UWB positioning based automatic docking trajectory design for unmanned surface vehicle,” IEEE Transactions on Instrumentation and Measure- ment, 2023

  8. [6]

    An event-triggered trajectory planning and tracking scheme for automatic berthing of unmanned surface vessel,

    S. Yuan, Z. Liu, Y . Sun, Z. Wang, and L. Zheng, “An event-triggered trajectory planning and tracking scheme for automatic berthing of unmanned surface vessel,” Ocean Engineering, vol. 273, 2023

Show all 33 references
  1. [7]

    An optimization-based motion planner for autonomous maneuvering of marine vessels in complex environments,

    K. Bergman, O. Ljungqvist, J. Linder, and D. Axehill, “An optimization-based motion planner for autonomous maneuvering of marine vessels in complex environments,” in IEEE Conference on Decision and Control (CDC) , 2020, pp. 5283–5290

  2. [8]

    An anytime visibility– voronoi graph-search algorithm for generating robust and feasible unmanned surface vehicle paths,

    M. Schoener, E. Coyle, and D. Thompson, “An anytime visibility– voronoi graph-search algorithm for generating robust and feasible unmanned surface vehicle paths,” Autonomous Robots, vol. 46, no. 8, pp. 911–927, 2022

  3. [9]

    An hierarchical architecture for docking autonomous surface vehicles,

    P. Leite, R. Silva, A. Matos, and A. M. Pinto, “An hierarchical architecture for docking autonomous surface vehicles,” in 2019 IEEE International Conference on Autonomous Robot Systems and Compe- titions (ICARSC), 2019, pp. 1–6

  4. [10]

    Model reference adaptive control-based au- tonomous berthing of an unmanned surface vehicle under environ- mental disturbance,

    S. Baek and J. Woo, “Model reference adaptive control-based au- tonomous berthing of an unmanned surface vehicle under environ- mental disturbance,” Machines, vol. 10, 2022

  5. [11]

    A ship berthing system design by cooperating with tugboats and dampers,

    A.-M. D. Tran, S. Ji, and Y .-B. Kim, “A ship berthing system design by cooperating with tugboats and dampers,” 2014

  6. [12]

    Autonomous docking of an unmanned surface vehicle using model predictive control,

    S. Kockum, “Autonomous docking of an unmanned surface vehicle using model predictive control,” Master’s thesis, Lund University, 2022

  7. [13]

    Towards using reinforcement learning for autonomous docking of unmanned surface vehicles,

    M. Holen, E.-L. M. Ruud, N. D. Warakagoda, M. Goodwin, P. Engel- stad, and K. M. Knausgård, “Towards using reinforcement learning for autonomous docking of unmanned surface vehicles,” in Engineering Applications of Neural Networks , 2022, pp. 461–474

  8. [14]

    Baier and J.-P

    C. Baier and J.-P. Katoen, Principles of model checking . MIT press, 2008

  9. [15]

    Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,

    X. Yin, B. Gao, and X. Yu, “Formal synthesis of controllers for safety- critical autonomous systems: Developments and challenges,” Annual Reviews in Control, vol. 57, 2024

  10. [16]

    (2018) Class guidelines for autonomuos and remotely operated ships

    DNV GL. (2018) Class guidelines for autonomuos and remotely operated ships. DNVGL-CG-0264, Edition September 2018

  11. [17]

    Tabuada, Verification and control of hybrid systems: a symbolic approach

    P. Tabuada, Verification and control of hybrid systems: a symbolic approach. Springer Science & Business Media, 2009

  12. [19]

    Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations,

    B. Zhong, A. Lavaei, M. Zamani, and M. Caccamo, “Automata-based controller synthesis for stochastic systems: A game framework via approximate probabilistic relations,” Automatica, 2023

  13. [20]

    SCOTS: A tool for the synthesis of symbolic controllers,

    M. Rungger and M. Zamani, “SCOTS: A tool for the synthesis of symbolic controllers,” in Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control , 2016

  14. [21]

    pFaces: An acceleration ecosystem for symbolic control,

    M. Khaled and M. Zamani, “pFaces: An acceleration ecosystem for symbolic control,” in Proceedings of the 22nd International Confer- ence on Hybrid Systems: Computation and Control , 2019

  15. [22]

    Digital-physical testbed for ship autonomy studies in the marine cybernetics laboratory basin,

    E. C. Gezer, M. K. I. Moreau, A. S. Høgden, D. T. Nguyen, R. Skjetne, and A. Sørensen, “Digital-physical testbed for ship autonomy studies in the marine cybernetics laboratory basin,” ArXiv. 2025

  16. [24]

    Towards safe AI: Sandboxing dnns-based controllers in stochastic games,

    B. Zhong, H. Cao, M. Zamani, and M. Caccamo, “Towards safe AI: Sandboxing dnns-based controllers in stochastic games,” in Proceed- ings of the AAAI Conference on Artificial Intelligence , vol. 37, no. 12, 2023, pp. 15 340–15 349

  17. [25]

    Efficient implementation of symbolic controllers for cyber-physical systems,

    M. K. M. Mahmoud, “Efficient implementation of symbolic controllers for cyber-physical systems,” Ph.D. dissertation, Technichal University of Munich, 2021

  18. [26]

    T. I. Fossen, Handbook of marine craft hydrodynamics and motion control. John Wiley & Sons, 2011

  19. [27]

    Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach, 1st ed

    P. Tabuada, Verification and Control of Hybrid Systems: A Symbolic Approach, 1st ed. Springer Publishing Company, Incorporated, 2009

  20. [28]

    Provably safe trajectory optimization in the presence of uncertain convex obstacles,

    C. Dawson, A. Jasour, A. Hofmann, and B. Williams, “Provably safe trajectory optimization in the presence of uncertain convex obstacles,” in 2020 IEEE International Conference on Intelligent Robots and Systems (IROS), 2020, pp. 6237–6244

  21. [29]

    Provably safe robot navigation with obstacle uncertainty,

    B. Axelrod, L. P. Kaelbling, and T. Lozano-Pérez, “Provably safe robot navigation with obstacle uncertainty,” The International Journal of Robotics Research, vol. 37, no. 13-14, pp. 1760–1774, 2018

  22. [30]

    Maneuvering-based dynamic thrust allocation for fully-actuated vessels,

    E. C. Gezer and R. Skjetne, “Maneuvering-based dynamic thrust allocation for fully-actuated vessels,” IFAC-PapersOnLine, vol. 58, no. 20, pp. 374–379, 2024

  23. [31]

    A generalized extended kalman filter implementation for the robot operating system,

    T. Moore and D. Stouch, “A generalized extended kalman filter implementation for the robot operating system,” in Proceedings of the 13th International Conference on Intelligent Autonomous Systems (IAS-13), 2014

  24. [32]

    Development of a DP system for CS Enterprise I with V oith Schneider thrusters,

    H. N. Skåtun, “Development of a DP system for CS Enterprise I with V oith Schneider thrusters,” Master’s thesis, Norwegian University of Science and Technology, 2011. [Online]. Available: https://ntnuopen.ntnu.no/ntnu-xmlui/handle/11250/237980

  25. [33]

    Distributed automated synthesis of correct-by-construction controllers,

    UNIV MUENCHEN TECH, “Distributed automated synthesis of correct-by-construction controllers,” Patent EP3 633 468A1, 2020

Pith tools

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