Pith. sign in

REVIEW 3 major objections 4 minor 29 references

Efficient Dynamic Shielding for Parametric Safety Specifications

T0 review · 3 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

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

Pith's one-line read For parametric safety specifications, this paper claims a dynamic shield can be assembled at runtime by composing precomputed atomic shields, and does so up to five times faster than recomputing from scratch.

desk verdict A genuinely new problem and a correct composition theorem, but the abstraction-based implementation is not conservative for arbitrary safe sets, so the paper needs a major revision before its generality claims hold. read the letter →

arxiv 2505.22104 v1 pith:RVGOSDJQ submitted 2025-05-28 cs.AI cs.LGcs.LOcs.ROcs.SYeess.SY

Davide Corsi , Kaushik Mallik , Andoni Rodriguez , Cesar Sanchez This is my paper
classification cs.AIcs.LGcs.LOcs.ROcs.SYeess.SY
keywords dynamicshieldingparametricsafetyspecificationsabstraction-basedcontrolcontrollersmaximalpermissivenessrobotnavigationruntimeverificationbinarydecisiondiagrams
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

Safety shields are runtime monitors that override an AI controller's actions when they would violate a safety specification. Traditionally, if the specification changes—say, a robot discovers a new obstacle—the shield must be recomputed from scratch. This paper introduces dynamic shields for parametric safety specifications, where the possible specifications are a finite family of atomic safe sets, and the online adaptation is just a composition of the precomputed atomic shields. The central result is that the shield for a conjunction of atomic specifications is the largest nonblocking sub-controller—a controller that never lets a path get stuck—of the product of the atomic shields, obtained by intersecting allowed actions and then pruning deadlock-prone states. On a Dubins-vehicle navigation benchmark where obstacles appear as they come into sensor range, the dynamic shields adapted in a fraction of a second to a few seconds per step, up to five times faster than the brute-force online recomputation baseline.

What carries the argument

The load-bearing object is the nonblocking, maximally permissive (n.m.p.) safety controller: for a safe set $G$, the unique controller that keeps every path inside $G$ forever, never lets a finite path get stuck, and allows every input that some safe controller could allow. The composition step is the controller product $C^*_G \sqcap C^*_H$, defined state-wise as $C^*_G(x) \cap C^*_H(x)$ on the intersection of the atomic domains, followed by computing the largest nonblocking sub-controller of that product. The pruning is implemented by adding a sink state, sending every disallowed transition into it, and applying the standard controllable-predecessor operator, which deletes states that have no input keeping the system inside the surviving set. This product-plus-prune recipe is what lets the shield adapt online from precomputed atomic shields; in the implementation the surviving system has far fewer live transitions than the full abstraction, which is the source of the speedup.

What would settle it

Construct a navigation scenario in which a previously unknown obstacle first appears exactly at the border of the visible region, and observe whether the robot can reach a state inside the visible region at which the dynamically composed shield returns the empty set of actions while the state is actually safe; a single such stuck state would falsify the safe-handover guarantee.

Watch

Extended reading notes

Core claim

At the theory level, the discovery is Theorem 2: for safe sets $G$ and $H$, a nonblocking controller is a safety controller for $\mathrm{Safety}(G \cap H)$ if and only if it is a nonblocking sub-controller of the product $C^*_G \sqcap C^*_H$, where $C^*_G$ and $C^*_H$ are the unique nonblocking, maximally permissive safety controllers for the individual specifications. Because $\mathrm{Safety}(G \cap H)$ equals $\mathrm{Safety}(G) \cap \mathrm{Safety}(H)$, any safe controller must at every state choose an input allowed by both atomic controllers, and the only leftover work is to remove states from which no infinite safe play exists. The paper turns this into an algorithm: compute atomic shields offline, then at runtime compute their product and prune it to the largest nonblocking sub-controller. In the abstraction-based implementation the pruning is done by redirecting disallowed transitions to a sink state and running the standard controllable-predecessor iteration, all symbolically with BDDs, so the concrete shield is sound for the continuous system though maximal permissiveness is only guaranteed for the abstraction.

Load-bearing premise

The navigation guarantees rely on an unproven safe-handover claim: treating the entire unobservable region as unsafe through artificial fences of thickness epsilon is asserted to keep every future robot state inside the domain of the next adapted shield, and if that fails a newly composed shield may have no defined action at the current state.

Editorial extensions

If this is right

  • A runtime change in the safety specification is handled by composing the relevant atomic shields, so the online cost scales with the number of active atomic safe sets rather than with the $2^{|R|}$ possible conjunctions.
  • The concrete shield is sound by construction: because the abstraction over-approximates the continuous dynamics, any input the shield allows keeps the real system inside the current safe set despite disturbances.
  • The online step is dominated by deadlock removal on the product controller, whose effective transition count is small, giving the observed speedup of up to five times over recomputing a shield from scratch.
  • The same composition works for any subset of the parameter set revealed at runtime, not just for a fixed sequence of specifications.
  • The resulting shields are minimally intervening: they override a learned controller only when the proposed input could leave the domain of the n.m.p. controller, so the controller keeps as much freedom as safety allows (within abstraction granularity).

Reading between the lines

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

  • If new atomic safe sets can be added at runtime, the composition recipe suggests an incremental extension: synthesize one new atomic shield and splice it into the product, rather than re-solving the whole family.
  • The product-and-prune construction might transfer to other settings where unique maximally permissive controllers exist, such as some quantitative or cost-bounded shields, but liveness objectives generally lack the uniqueness that makes the intersection argument exact.
  • The artificial-fence handover is a deliberately worst-case solution; a less conservative handover based on forward reachability or context-triggered re-abstraction could shrink the permissiveness lost to the fence, at the cost of a heavier online step.
  • The benchmark speedup is relative to a software baseline; whether the sub-second-to-few-second adaptation suffices for real vehicles depends on the system's dynamics time step, which would need hardware validation.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

Summary. The paper proposes dynamic shields for parametric safety specifications. Given a finite set R of atomic safe sets, the shield is designed offline as a collection of nonblocking maximally permissive (n.m.p.) safety controllers, one per atomic set. At runtime, when the active specification is an intersection of atomic sets, the corresponding controllers are combined by first intersecting their allowed actions and then computing the largest nonblocking sub-controller. Theorem 2 states that this two-step composition yields exactly the n.m.p. safety controller for the intersection, assuming such controllers exist. The paper then instantiates this scheme in the abstraction-based control (ABC) framework using feedback refinement relations and symbolic BDD operations, and evaluates it on a Dubins vehicle navigation task in unknown territory with a limited visible region, reporting offline synthesis times of minutes and online adaptation times of fractions of a second to a few seconds, up to 5x faster than recomputing a shield online. A 'safe handover' strategy based on artificial fences is proposed for the navigation setting.

Significance. If the technical gaps are repaired, this is a valuable contribution. The core theoretical result—Theorem 2 and Corollary 1—is clean and the proofs are correct for finite-state systems; the idea of composing atomic n.m.p. shields offline and only removing blocking states online is elegant and likely to be useful beyond the specific robot-navigation example. The paper is also honest about the incompleteness of ABC (Remark 2) and provides a concrete experimental infrastructure built on the authors' Mascot-SDS tool with BDDs; the reported online times are concrete and the up-to-5x speedup is a useful data point. There are no fitted parameters in the central derivation; the free parameters (grid size, fence thickness, sampling time) are standard for ABC. However, the general soundness claim for the ABC implementation is not established, and the safe handover guarantee is asserted without proof, so the general claims currently exceed what is proved.

major comments (3)
  1. [Section 4.1] The abstraction cG = Q(G) = {bx in bX | bx ∩ G ≠ ∅} together with bPhi = Safety_bSigma(Q(G)) is not a conservative abstraction of the safety specification Safety_Sigma(G). For the FRR refinement step to be sound, every concrete path whose abstract image is accepted by bPhi must itself be safe, i.e., Q^{-1}(bPhi) ⊆ Safety_Sigma(G). This fails already in a one-dimensional example: take X=[0,1], G=(0.4,0.6), and cells [0,0.5], [0.5,1]. Then Q(G) contains the cell [0,0.5], so the constant abstract path [0,0.5]^ω is in bPhi, but the concrete path 0.1,0.1,... maps to it and leaves G. Consequently, the controller refined as C_Phi(x)=bC(Q(x)) is not guaranteed to be a sound safety controller for arbitrary atomic safe sets. This invalidates the claimed 'sound but incomplete' ABC algorithm for the general setting of Problem 3, where R is an arbitrary finite subset of 2^X. The standard fix is to abstract G by the inner approximation {bx | bx ⊆ G}, or to restrict the scope to safe sets that are unions of grid cells (which is the case in the Section 5 benchmark).
  2. [Section 5] The safe handover guarantee is asserted without proof. The paragraph beginning 'We need to ensure a safe handover...' claims that artificial fences of thickness epsilon model the unobservable region as unsafe and that 'it is guaranteed that the future states of the robot will be within the domain of future shield adaptations.' This does not follow: the fence makes the current unobservable region unsafe, but the next shield is synthesized over a re-centered visible region and may contain newly revealed obstacle cells. A move allowed by the current shield can lead to a state that is winning in the current local frame but, after re-centering, is losing for the new obstacle configuration (for example, if the newly revealed obstacles surround the origin so that no action keeps the system inside the new safe set). The paper needs a proof of the handover property, or a formal restriction to states that are winning for all admissible parameter values, or an explicit additional handover constraint in the synthesis. This is load-bearing for the navigation application and for the 100% safety claim in Section 6.
  3. [Section 6] The experimental claim that 'All synthesized shields are by-construction safe and minimally permissive' contradicts Remark 2, which states that using ABC sacrifices maximal permissiveness with respect to the concrete system. The composition theorem (Theorem 2) yields an n.m.p. controller only at the abstract level; after refinement, the concrete shield is safe only if the abstraction is correct, and it is not known to be minimally intervening in the sense of Problem 1. The experimental section should be reworded, and the effect of abstraction on permissiveness should be discussed or measured rather than asserted away.
minor comments (4)
  1. [Section 4.2, Step A] The sentence 'Suppose Gi ⊆ X be an atomic unsafe set of states' should read 'atomic safe set' or 'atomic safety specification', since Section 3.2 defines R as a set of atomic safe sets.
  2. [Section 5] The statement 'The state space ... in which the robot's initial state is always the origin' is ambiguous; please state explicitly whether the reference frame is re-centered at every adaptation step and how the new visible region and fence are computed from the previous action.
  3. [Figure 2] The caption says 'The corners (−1,−1) and (1,1) of the visible region', but the extended state space X includes the fence of thickness epsilon; the labels should refer to the boundary of the extended state space, or the text should define d explicitly.
  4. [Section 5] The paper should state more prominently that in the experiments the RL controller knows the entire map while the shield has only local visibility; this asymmetry is important for interpreting the setup and the reported safety rates.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: Theorem 2 follows from the definitions of n.m.p. safety controllers and the product operation; the implementation caveats are soundness gaps, not self-referential reductions.

full rationale

The central derivation (Theorem 2, Corollary 1, and the online composition algorithm in Section 3.3) is not circular. It uses Safety(G ∩ H) = Safety(G) ∩ Safety(H), so any nonblocking safety controller for the intersection is a safety controller for each conjunct; by maximal permissiveness it is a sub-controller of each atomic n.m.p. controller and hence of their product. The largest nonblocking sub-controller is then characterized by the three clauses of Corollary 1, which are exactly the definition of the n.m.p. controller for the intersection. No fitted parameter is renamed as a prediction, and no result is imported from the authors' own prior work as a load-bearing uniqueness theorem; the uniqueness/maximal-permissiveness fact is cited to the external reference [28]. The self-citation to Mascot-SDS [15] appears only as the implementation substrate for the prototype and does not support the composition theorem. Two non-circular caveats are worth recording: Section 4.1 asserts without proof that bPhi = Safety_bSigma(Q(G)) is a conservative abstraction (bPhi ⊆ Q(Phi)), which can fail when a grid cell straddles the boundary of G; and Section 5 asserts a safe-handover guarantee for artificial fences without a proof. These are correctness/soundness gaps in the general abstraction and navigation application, not reductions of the conclusion to the premises, so they do not raise the circularity score.

Assumptions & free parameters 3 free parameters · 5 assumptions · 1 invented entities

The theoretical core rests on standard safety-game results (existence of n.m.p. controllers, FRR soundness) and on the problem assumption that specifications are conjunctions of atomic safe sets. The navigation experiments add hand-chosen parameters (epsilon, grid sizes, tau) and an unproved fence-based safe-handover assumption. There are no fitted constants.

free parameters (3)
  • Fence thickness epsilon = 0.3
    Hand-chosen in the navigation experiments; it is the width of the artificial unsafe boundary and is load-bearing for the safe handover claim, but no sensitivity analysis is given.
  • Abstraction grid sizes = state [0.10, 0.10, 0.30], [0.08, 0.08, 0.25], [0.06, 0.06, 0.20]; input [0.2, 0.5]
    Chosen by hand to define three abstraction coarseness levels; these choices affect offline synthesis time and the reported online speedups.
  • Sampling time tau = 0.1 s
    Fixed discretization step of the Dubins model; affects the reachable dynamics and the fence requirement, chosen without sensitivity analysis.
assumptions (5)
  • standard math For safety specifications, unique nonblocking maximally permissive state-feedback controllers exist.
    Invoked in Section 2, following [28], and used to build atomic shields; unproved in this paper but standard in safety-game literature.
  • domain assumption The runtime safety specification is always the conjunction of an arbitrary subset of a finite, statically provided set R of atomic safe sets.
    This defines the parametric safety specification in Section 3.2 and bounds the problem; if the actual specification cannot be expressed this way, the dynamic shield construction does not apply.
  • domain assumption A feedback refinement relation from concrete system to finite abstraction can be constructed, giving sound but incomplete controller synthesis.
    Section 4.1 relies on the FRR framework [24]; soundness of the abstract shield transfers to the concrete system, but completeness and maximal permissiveness are lost.
  • standard math Largest nonblocking sub-controllers can be computed by the greatest-fixed-point iteration in Algorithms 1 and 2.
    Used in Step B2; guaranteed on finite abstractions but not in general for infinite-state systems, as acknowledged in Section 4.
  • ad hoc to paper Unobservable states can be safely over-approximated by artificial fences, ensuring safe handover.
    Asserted in Section 5 without proof; this is the paper-specific mechanism for the navigation scenario.
invented entities (1)
  • Artificial fences
    purpose: Model the worst-case uncertainty at the boundary of the visible region and ensure safe handover between dynamic shields at consecutive steps.
    The fence is an added unsafe set X \ [-d,d]^2 that is not part of the physical environment; no falsifiable prediction is attached to it outside the navigation scenario.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Efficient Dynamic Shielding for Parametric Safety Specifications." pith.science (2026). https://pith.science/paper/RVGOSDJQ

@misc{pith2026250522104,
  author       = {Pith},
  title        = {Pith review of: Efficient Dynamic Shielding for Parametric Safety Specifications},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RVGOSDJQ}},
  note         = {Machine review of arXiv:2505.22104}
}
read the original abstract

Shielding has emerged as a promising approach for ensuring safety of AI-controlled autonomous systems. The algorithmic goal is to compute a shield, which is a runtime safety enforcement tool that needs to monitor and intervene the AI controller's actions if safety could be compromised otherwise. Traditional shields are designed statically for a specific safety requirement. Therefore, if the safety requirement changes at runtime due to changing operating conditions, the shield needs to be recomputed from scratch, causing delays that could be fatal. We introduce dynamic shields for parametric safety specifications, which are succinctly represented sets of all possible safety specifications that may be encountered at runtime. Our dynamic shields are statically designed for a given safety parameter set, and are able to dynamically adapt as the true safety specification (permissible by the parameters) is revealed at runtime. The main algorithmic novelty lies in the dynamic adaptation procedure, which is a simple and fast algorithm that utilizes known features of standard safety shields, like maximal permissiveness. We report experimental results for a robot navigation problem in unknown territories, where the safety specification evolves as new obstacles are discovered at runtime. In our experiments, the dynamic shields took a few minutes for their offline design, and took between a fraction of a second and a few seconds for online adaptation at each step, whereas the brute-force online recomputation approach was up to 5 times slower.

Figures

Figures reproduced from arXiv: 2505.22104 by the authors.

Figure 1
Figure 1. Illustration of the two steps involved in the online composition of atomic [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗
Figure 2
Figure 2. Illustration of dy￾namic shielding of the robot (blue dot) in an unknown environment. Dynamic shields are com￾puted using ABC, but not over the entire state space, rather over the the tiny visible region of the robot. The corners “(−1, −1)” and “(1, 1)” of the visible region are in the robot’s own reference coordinates. We need to ensure a safe handover of two dynamically adapted shields at consecutive steps, i.e., … view at source ↗
Figure 3
Figure 3. Average online computation times of the pure online algorithm (the base [PITH_FULL_IMAGE:figures/full_fig_p018_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

29 extracted references · 24 canonical work pages

  1. [1]

    In: Proceedings of the AAAI conference on artificial intelligence

    Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Proceedings of the AAAI conference on artificial intelligence. vol. 32 (2018)

    2018

  2. [2]

    In: International Conference on Computer Aided Verification

    Anand, A., Nayak, S.P., Schmuck, A.K.: Synthesizing permissive winning strat- egy templates for parity games. In: International Conference on Computer Aided Verification. pp. 436–458. Springer (2023)

    2023

  3. [3]

    In: 2019 American Control Confer- ence (ACC)

    Bharadwaj, S., Bloem, R., Dimitrova, R., Konighofer, B., Topcu, U.: Synthesis of minimum-cost shields for multi-agent systems. In: 2019 American Control Confer- ence (ACC). pp. 1048–1055. IEEE (2019)

    work page 2019

  4. [4]

    In: International conference on tools and algo- rithms for the construction and analysis of systems

    Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: Runtime enforcement for reactive systems. In: International conference on tools and algo- rithms for the construction and analysis of systems. pp. 533–548. Springer (2015)

    2015

  5. [5]

    arXiv preprint arXiv:2101.11196 (2021)

    ElSayed-Aly, I., Bharadwaj, S., Amato, C., Ehlers, R., Topcu, U., Feng, L.: Safe multi-agent reinforcement learning via shielding. arXiv preprint arXiv:2101.11196 (2021)

    arXiv 2021

  6. [6]

    Proceedings of the ACM on Programming Languages9(OOPSLA1), 816– 843 (2025)

    Feng, Y., Zhu, J., Platzer, A., Laurent, J.: Adaptive shielding via parametric safety proofs. Proceedings of the ACM on Programming Languages9(OOPSLA1), 816– 843 (2025)

    work page 2025

  7. [7]

    In: 2018 IEEE International Conference on Robotics and Automation (ICRA)

    Fridovich-Keil, D., Herbert, S.L., Fisac, J.F., Deglurkar, S., Tomlin, C.J.: Planning, fast and slow: A framework for adaptive real-time safe trajectory planning. In: 2018 IEEE International Conference on Robotics and Automation (ICRA). pp. 387–394. IEEE (2018)

    work page 2018

  8. [8]

    In: International Workshop on Hybrid Systems: Computation and Control

    Henzinger, T.A., Raskin, J.F.: Robust undecidability of timed and hybrid systems. In: International Workshop on Hybrid Systems: Computation and Control. pp. 145–159. Springer (2000)

    work page 2000

Show all 29 references
  1. [9]

    IEEE Robotics and Automation Letters 7(2), 5591–5598 (2022)

    Hu, H., Nakamura, K., Fisac, J.F.: Sharp: Shielding-aware robust planning for safe and efficient human-robot interaction. IEEE Robotics and Automation Letters 7(2), 5591–5598 (2022)

    2022

  2. [10]

    arXiv preprint arXiv:1807.06096 (2018) 20 Davide Corsi , Kaushik Mallik , Andoni Rodríguez, and César Sánchez

    Jansen, N., Könighofer, B., Junges, S., Bloem, R.: Shielded decision-making in mdps. arXiv preprint arXiv:1807.06096 (2018) 20 Davide Corsi , Kaushik Mallik , Andoni Rodríguez, and César Sánchez

    2018 arXiv

  3. [11]

    Formal Methods in System Design51, 332–361 (2017)

    Könighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., Könighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods in System Design51, 332–361 (2017)

    2017

  4. [12]

    Könighofer, B., Rudolf, J., Palmisano, A., Tappler, M., Bloem, R.: Online shielding forreinforcementlearning.InnovationsinSystemsandSoftwareEngineering 19(4), 379–394 (2023)

    2023

  5. [13]

    In: 2020 IEEE International Conference on Robotics and Automation (ICRA)

    Li, S., Bastani, O.: Robust model predictive shielding for safe reinforcement learn- ing with stochastic dynamics. In: 2020 IEEE International Conference on Robotics and Automation (ICRA). pp. 7166–7172. IEEE (2020)

    2020

  6. [14]

    The International Journal of Robotics Research36(8), 947–982 (2017)

    Majumdar, A., Tedrake, R.: Funnel libraries for real-time robust feedback motion planning. The International Journal of Robotics Research36(8), 947–982 (2017)

    2017

  7. [15]

    In: International Conference on Computer Aided Verification

    Majumdar, R., Mallik, K., Rychlicki, M., Schmuck, A.K., Soudjani, S.: A flex- ible toolchain for symbolic rabin games under fair and stochastic uncertainties. In: International Conference on Computer Aided Verification. pp. 3–15. Springer (2023)

    2023

  8. [16]

    Nonlinear Analysis: Hybrid Systems 51, 101430 (2024)

    Majumdar, R., Mallik, K., Schmuck, A.K., Soudjani, S.: Symbolic control for stochastic systems via finite parity games. Nonlinear Analysis: Hybrid Systems 51, 101430 (2024)

    2024

  9. [17]

    IEEE Open Journal of Control Systems 2, 277–296 (2023)

    Nayak,S.P.,Egidio,L.N.,DellaRossa,M.,Schmuck,A.K.,Jungers,R.M.:Context- triggered abstraction-based control design. IEEE Open Journal of Control Systems 2, 277–296 (2023)

    2023

  10. [18]

    Discrete Event Dynamic Systems27(2), 301–340 (2017)

    Nilsson, P., Ozay, N., Liu, J.: Augmented finite transition systems as abstractions for control synthesis. Discrete Event Dynamic Systems27(2), 301–340 (2017)

    2017

  11. [19]

    SIAM Journal on Control and Optimization 48(2), 719–733 (2009)

    Pola, G., Tabuada, P.: Symbolic models for nonlinear control systems: Alternating approximate bisimulations. SIAM Journal on Control and Optimization 48(2), 719–733 (2009)

    2009

  12. [20]

    In: Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast,QLD,Australia,October18–22,2021,Proceedings19.pp.222–228.Springer (2021)

    Pranger, S., Könighofer, B., Posch, L., Bloem, R.: Tempest-synthesis tool for reac- tive systems and shields in probabilistic environments. In: Automated Technology for Verification and Analysis: 19th International Symposium, ATVA 2021, Gold Coast,QLD,Australia,October18–22,20...

    2021

  13. [21]

    In: 2021 American Control Conference (ACC)

    Pranger, S., Könighofer, B., Tappler, M., Deixelberger, M., Jansen, N., Bloem, R.: Adaptive shielding under uncertainty. In: 2021 American Control Conference (ACC). pp. 3467–3474. IEEE (2021)

    2021

  14. [22]

    In: 2021 IEEE International Conference on Robotics and Automation (ICRA)

    Quan, L., Zhang, Z., Zhong, X., Xu, C., Gao, F.: Eva-planner: Environmental adaptive quadrotor planning. In: 2021 IEEE International Conference on Robotics and Automation (ICRA). pp. 398–404. IEEE (2021)

    2021

  15. [23]

    International Journal of Engineering 38(1), 21–34 (2025)

    Raeesi,H.,Khosravi,A.,Sarhadi,P.:Safereinforcementlearningbyshieldingbased reachable zonotopes for autonomous vehicles. International Journal of Engineering 38(1), 21–34 (2025)

    2025

  16. [24]

    IEEE Transactions on Automatic Control62(4), 1781–1796 (2016)

    Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the syn- thesis of symbolic controllers. IEEE Transactions on Automatic Control62(4), 1781–1796 (2016)

    2016

  17. [25]

    In: Proceedings of the 19th international conference on hybrid systems: Computation and control

    Rungger, M., Zamani, M.: Scots: A tool for the synthesis of symbolic controllers. In: Proceedings of the 19th international conference on hybrid systems: Computation and control. pp. 99–104 (2016)

    2016

  18. [26]

    IEEE Transactions on Automatic Control53(6), 1406–1418 (2008)

    Tabuada, P.: An approximate simulation approach to symbolic control. IEEE Transactions on Automatic Control53(6), 1406–1418 (2008)

    2008

  19. [27]

    Van Dijk, T., Van De Pol, J.: Sylvan: Multi-core decision diagrams. In: Tools and Algorithms for the Construction and Analysis of Systems: 21st International Efficient Dynamic Shielding for Parametric Safety Specifications 21 Conference, TACAS 2015, Held as Part of the Europea...

    2015

  20. [28]

    In: International Workshop on Hybrid Systems: Computation and Control

    Vidal, R., Schaffert, S., Lygeros, J., Sastry, S.: Controlled invariance of discrete time systems. In: International Workshop on Hybrid Systems: Computation and Control. pp. 437–451. Springer (2000)

    2000

  21. [29]

    In: International Symposium on Automated Technology for Verification and Analysis

    Waga, M., Castellano, E., Pruekprasert, S., Klikovits, S., Takisaka, T., Hasuo, I.: Dynamic shielding for reinforcement learning in black-box environments. In: International Symposium on Automated Technology for Verification and Analysis. pp. 25–41. Springer (2022)

    2022

Pith tools

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