Easy-to-Use Shielding for Reinforcement Learning

Bettina K\"onighofer; Stefan Pranger

arxiv: 2606.03804 · v1 · pith:TNZPBX65new · submitted 2026-06-02 · 💻 cs.LG

Easy-to-Use Shielding for Reinforcement Learning

Stefan Pranger , Bettina K\"onighofer This is my paper

Pith reviewed 2026-06-28 10:59 UTC · model grok-4.3

classification 💻 cs.LG

keywords safe explorationreinforcement learningshieldingformal methodsGymnasiumstochastic gamesMiniGridsafe RL

0 comments

The pith

A library integrates formal shield synthesis into the Gymnasium API to enable safe exploration in reinforcement learning.

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

The paper presents a Python library that connects formal shield synthesis with standard reinforcement learning frameworks through the Gymnasium API. This addresses the challenge of safe exploration remaining difficult to apply because it has required expertise in formal methods and substantial custom engineering. A sympathetic reader would care because the integration allows shields to be synthesized and deployed inside existing RL pipelines without those barriers. The paper also extends the underlying synthesis to handle stochastic multiplayer games while keeping formal guarantees intact and supplies new modeling tools and environments for testing.

Core claim

The central claim is that a Python library can integrate Tempest-based shield synthesis directly into the Gymnasium API, allowing shields to be synthesized and deployed within existing RL pipelines. This turns formal safe-exploration methods into a usable component for RL practitioners. The work extends algorithmic support to compute sound shields for stochastic multiplayer games while preserving formal safety guarantees. It demonstrates an end-to-end workflow and evaluates shielded versus unshielded RL across environments, supported by symbolic models for MiniGrid and a new collection of safety-oriented playground environments called MiniGridSafe.

What carries the argument

The Python library that integrates shield synthesis directly into the Gymnasium API, serving as the bridge that makes formal shielding deployable inside standard RL code.

If this is right

Shields become synthesizable and deployable inside existing RL pipelines with minimal extra engineering.
Formal safety guarantees remain intact when the approach is applied to stochastic multiplayer games.
Symbolic models for MiniGrid make it straightforward to create safety scenarios for shielding experiments.
MiniGridSafe supplies ready environments with probabilistic transitions and multiple agents for studying safety.
End-to-end evaluation of shielded and unshielded agents becomes possible across multiple test cases.

Where Pith is reading between the lines

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

The same API-wrapping pattern could be applied to other RL libraries to widen access to shielding.
Researchers could test the library on environments outside the provided MiniGrid collection to check generality.
The lowered barrier might encourage hybrid combinations of shielding with other safe-RL techniques.

Load-bearing premise

That wrapping the shield synthesis inside the Gymnasium API preserves the original formal safety guarantees without introducing implementation errors or requiring users to supply accurate environment models.

What would settle it

An experiment in which a shielded agent produced by the library violates a safety property in one of the provided environments that the formal shield model should have blocked.

Figures

Figures reproduced from arXiv: 2606.03804 by Bettina K\"onighofer, Stefan Pranger.

**Figure 2.** Figure 2: The two types of shield application. Left: Pre-shielding restricts the choices of the agent. Right: Post-shielding prevents unsafe actions from being executed. when the agent’s chosen action is unsafe, leaving the agent’s behaviour unaffected otherwise. The choice of f is left to the user. A simple choice is a fixed, safe action asafe ∈ A, such as a no-op or a braking action. Alternatively, f can select th… view at source ↗

**Figure 3.** Figure 3: Two environments illustrating the safety-critical extensions of [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗

**Figure 4.** Figure 4: Training results for the environments in Figure 3. Thick lines show the [PITH_FULL_IMAGE:figures/full_fig_p012_4.png] view at source ↗

read the original abstract

Safe exploration is a key challenge in Reinforcement Learning (RL) that aims to prevent agents from making harmful decisions while exploring their environment. Safe exploration is a key challenge in Reinforcement Learning (RL) that aims to prevent agents from making harmful decisions while exploring their environment. Shielding is one such technique that assumes domain knowledge in the form of an environment model to decide upon action safety. Although well-established, shielding has seen limited adoption in RL due to the lack of accessible end-to-end infrastructure connecting formal shield synthesis with standard RL frameworks. Applying shielding typically requires expertise in formal methods and substantial engineering effort, keeping it outside the typical RL workflow. We address this by extending our shield synthesis tool Tempest into a practical backend for safe RL. Our core contribution is tempestpy, a Python library that integrates Tempest-based shield synthesis directly into the Gymnasium API, allowing shields to be synthesized and deployed within existing RL pipelines. This lowers the barrier to entry for shielding and turns formal safe-exploration methods into a usable component for RL practitioners. We also extend Tempest's algorithmic support to compute sound shields for stochastic multiplayer games, preserving formal safety guarantees. We demonstrate the resulting workflow end to end and evaluate shielded and unshielded RL across multiple environments. To facilitate modeling, we provide symbolic models for MiniGrid and introduce MiniGridSafe, a collection of playground environments designed to make shielding easily accessible and experimentally transparent. MiniGridSafe extends MiniGrid with safety-oriented scenarios featuring probabilistic transitions and additional agents, enabling the study of challenging safety aspects in a simple and intuitive setting.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper ships tempestpy as a Gymnasium wrapper around Tempest shielding plus some new environments and a multiplayer extension, but the advance is packaging rather than new theory or algorithms.

read the letter

The core thing to know is that this work packages Tempest shield synthesis into a Python library called tempestpy that plugs directly into the Gymnasium API, plus they added support for stochastic multiplayer games and released MiniGridSafe as a set of test environments.

What is actually new is the library integration, the Tempest extension for multiplayer stochastic settings, and the MiniGridSafe collection with its symbolic models. The paper does a reasonable job showing an end-to-end workflow so that someone already using Gymnasium can synthesize and deploy a shield without starting from scratch on formal methods. That kind of engineering effort can matter for adoption even when the underlying shield synthesis stays the same.

The soft spots are modest but real. The safety claims rest entirely on Tempest being correct and the wrapper introducing no bugs, yet the text gives no separate checks or tests for the integration itself. The evaluation is described as comparing shielded and unshielded RL but supplies no numbers, overhead figures, or error analysis in the abstract, so it is hard to judge how much practical difference the shields make. Model accuracy is still required, and the paper does not explore what happens when that assumption slips.

This is for RL people who want to try shielding in their existing pipelines without heavy formal-methods overhead. A reader focused on usable tools rather than new theorems will find something concrete here. It deserves a serious referee because the artifacts are new, the claims are scoped to integration, and the goal of lowering barriers is worth checking in review.

Referee Report

2 major / 2 minor

Summary. The paper introduces tempestpy, a Python library that integrates Tempest-based shield synthesis directly into the Gymnasium API for reinforcement learning. It extends Tempest to compute sound shields for stochastic multiplayer games while preserving formal safety guarantees, provides symbolic models for MiniGrid, introduces the MiniGridSafe collection of environments with probabilistic transitions and multiple agents, and demonstrates an end-to-end shielded RL workflow with evaluation across environments.

Significance. If the integration correctly preserves Tempest's formal guarantees without introducing implementation errors, this work would meaningfully lower the barrier for RL practitioners to adopt shielding for safe exploration. The engineering contribution of an accessible Gymnasium-compatible backend, combined with the provision of transparent playground environments and symbolic models, supports reproducibility and could accelerate adoption of formal methods in RL pipelines.

major comments (2)

[Abstract / core contribution description] The central claim that the Gymnasium wrapper preserves formal safety guarantees (abstract and core contribution paragraph) rests on the assumption that the integration introduces no errors in shield synthesis or deployment; however, the manuscript provides no explicit verification steps, model accuracy checks, or implementation details to substantiate this for the stochastic multiplayer extension.
[Evaluation description] The evaluation of shielded vs. unshielded RL is described as having been performed across multiple environments, but the provided text supplies no quantitative results, performance metrics, safety violation counts, or error analysis, which is load-bearing for assessing the practical utility of the library.

minor comments (2)

[Abstract] The first sentence of the abstract is duplicated verbatim; this should be removed for clarity.
[Library description] Notation for the Gymnasium integration and Tempest extensions could be clarified with a diagram or pseudocode snippet showing the API calls for shield synthesis and deployment.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment and recommendation of minor revision. We address each major comment below and will incorporate the suggested clarifications and additions in the revised manuscript.

read point-by-point responses

Referee: [Abstract / core contribution description] The central claim that the Gymnasium wrapper preserves formal safety guarantees (abstract and core contribution paragraph) rests on the assumption that the integration introduces no errors in shield synthesis or deployment; however, the manuscript provides no explicit verification steps, model accuracy checks, or implementation details to substantiate this for the stochastic multiplayer extension.

Authors: We agree that the manuscript would benefit from more explicit discussion of the integration. tempestpy is implemented as a thin wrapper that invokes Tempest's existing shield synthesis routines (whose soundness for stochastic multiplayer games is established in prior work) and applies the resulting shield to Gymnasium actions without alteration. In the revision we will add a dedicated subsection describing the wrapper architecture, the interface to Tempest, the assumptions under which formal guarantees are inherited, and any manual or automated checks performed to confirm fidelity between the synthesized shield and its runtime application. revision: yes
Referee: [Evaluation description] The evaluation of shielded vs. unshielded RL is described as having been performed across multiple environments, but the provided text supplies no quantitative results, performance metrics, safety violation counts, or error analysis, which is load-bearing for assessing the practical utility of the library.

Authors: The evaluation section of the manuscript reports results from shielded and unshielded runs on the MiniGridSafe environments, but we acknowledge that the quantitative metrics, safety-violation counts, and error analysis are not presented with sufficient clarity or detail. In the revision we will expand this section to include explicit tables of performance metrics, violation counts, and any observed discrepancies, together with a brief error analysis. revision: yes

Circularity Check

0 steps flagged

No significant circularity; engineering contribution with no derivation chain

full rationale

The paper describes the development and integration of the tempestpy library for shielding in RL, extending Tempest to stochastic multiplayer games and providing Gymnasium-compatible interfaces plus MiniGridSafe environments. No equations, predictions, fitted parameters, or first-principles derivations are present that could reduce to inputs by construction. The contribution is tool-building and API wrapping; formal guarantees are explicitly attributed to the prior Tempest tool rather than re-derived here. Self-citation of Tempest is present but not load-bearing for any claimed result, as the paper makes no uniqueness theorems or ansatz-based claims. The work is self-contained as an engineering artifact evaluated on provided environments.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based solely on the abstract, no free parameters, axioms, or invented entities are identifiable; the work is an engineering integration rather than a theoretical derivation.

pith-pipeline@v0.9.1-grok · 5805 in / 964 out tokens · 38476 ms · 2026-06-28T10:59:24.534980+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

23 extracted references · 9 canonical work pages · 1 internal anchor

[1]

MIT Press (2008)

Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)

2008
[2]

In: Globersons, A., Mackey, L., Bel- grave, D., Fan, A., Paquet, U., Tomczak, J.M., Zhang, C

Banerjee, A., Rahmani, K., Biswas, J., Dillig, I.: Dynamic model predictive shield- ing for provably safe reinforcement learning. In: Globersons, A., Mackey, L., Bel- grave, D., Fan, A., Paquet, U., Tomczak, J.M., Zhang, C. (eds.) Advances in Neural Information Processing Systems 38: Annual Conference on Neural Inform- ation Processing Systems 2024, NeurI...

2024
[3]

In: International Conference on Tools and Al- gorithms for the Construction and Analysis of Systems (TACAS)

Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: Runtime enforcement for reactive systems. In: International Conference on Tools and Al- gorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 9035, pp. 533–548. Springer (2015)

2015
[4]

In: International Conference on Bridging the Gap between AI and Reality

Brorholt, A.H., Jensen, P.G., Larsen, K.G., Lorber, F., Schilling, C.: Shielded re- inforcement learning for hybrid systems. In: International Conference on Bridging the Gap between AI and Reality. pp. 33–54. Springer (2023)

2023
[5]

In: Das, S., Nowé, A., Vorobeychik, Y

Brorholt, A.H., Larsen, K.G., Schilling, C.: Compositional shielding and reinforce- ment learning for multi-agent systems. In: Das, S., Nowé, A., Vorobeychik, Y. (eds.) Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025, Detroit, MI, USA, May 19-23, 2025. pp. 399–407. International Foundation for Auton...

work page doi:10.5555/3709347.3743554 2025
[6]

In: Williams, B., Chen, Y., Neville, J

Carr, S., Jansen, N., Junges, S., Topcu, U.: Safe reinforcement learning via shield- ing under partial observability. In: Williams, B., Chen, Y., Neville, J. (eds.) Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty- Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, 14 S. Pranger and B. Könighofer...

work page doi:10.1609/aaai.v37i12.26723 2023
[7]

In: Flanagan, C., König, B

Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 18th In- ternational Conference, TACAS 2012, Held as Part of the European Joint Con- ferences on Theory and Practice of Software,...

work page doi:10.1007/978-3-642-28756-5 2012
[8]

RLJ4, 1759–1780 (2024),https: //rlj.cs.umass.edu/2024/papers/Paper224.html

Corsi, D., Amir, G., Rodríguez, A., Katz, G., Sánchez, C., Fox, R.: Verification- guided shielding for deep reinforcement learning. RLJ4, 1759–1780 (2024),https: //rlj.cs.umass.edu/2024/papers/Paper224.html

2024
[9]

Information and Computation285, 104886 (2022)

Eisentraut, J., Kelmendi, E., Křetínsk` y, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Information and Computation285, 104886 (2022)

2022
[10]

In: International Conference on Computer Aided Verification

Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Köhl, M.A., Wolf, V.: Mo- gym: using formal models for training and verifying decision-making agents. In: International Conference on Computer Aided Verification. pp. 430–443. Springer (2022)

2022
[11]

In: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications

Gross, D., Jansen, N., Junges, S., Pérez, G.A.: Cool-mc: a comprehensive tool for reinforcement learning and model checking. In: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. pp. 41–49. Springer (2022)

2022
[12]

In: Rocha, A.P., Steels, L., van den Herik, H.J

Gross, D., Spieker, H.: Probabilistic model checking of stochastic reinforcement learning policies. In: Rocha, A.P., Steels, L., van den Herik, H.J. (eds.) Pro- ceedings of the 16th International Conference on Agents and Artificial Intelli- gence, ICAART 2024, Volume 3, Rome, Italy, February 24-26, 2024. pp. 438–445. SCITEPRESS (2024). https://doi.org/10....

work page doi:10.5220/0012357700003636 2024
[13]

International Journal on Software Tools for Technology Transfer pp

Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabil- istic model checker storm. International Journal on Software Tools for Technology Transfer pp. 1–22 (2021)

2021
[14]

Könighofer, B., Bloem, R., Jansen, N., Junges, S., Pranger, S.: Shields for safe reinforcement learning. Commun. ACM68(11), 80–90 (2025). ht- tps://doi.org/10.1145/3715958,https://doi.org/10.1145/3715958

work page doi:10.1145/3715958 2025
[15]

In: Gopalakrishnan, G., Qadeer, S

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd Interna- tional Conference on Computer Aided Verification (CAV’11). LNCS, vol. 6806, pp. 585–591. Springer (2011)

2011
[16]

Reducibility among combinatorial problems

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Prism-games 3.0: Stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, LosAngeles,CA,USA,July21-24,2020,Proceedings,PartII.pp.475–487.Lecture Notes in Computer Science, Springer (2020)....

work page doi:10.1007/978-3-030- 2020
[17]

Kwiatkowski, A., Towers, M., Terry, J., Balis, J.U., Cola, G.D., Deleu, T., Goulão, M., Kallinteris, A., Krimmel, M., KG, A., Perez-Vicente, R., Pierré, A., Schulhoff, Easy-to-Use Shielding for Reinforcement Learning 15 S., Tai, J.J., Tan, H., Younis, O.G.: Gymnasium: A standard interface for rein- forcement learning environments (2024),https://arxiv.org/...

work page internal anchor Pith review Pith/arXiv arXiv 2024
[18]

In: International Conference on Computer Aided Verification

Meggendorfer, T., Weininger, M.: Playing games with your pet: Extending the par- tial exploration tool to stochastic games. In: International Conference on Computer Aided Verification. pp. 359–372. Springer (2024)

2024
[19]

In: Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016: Volume 2

Mousavi, S.S., Schukat, M., Howley, E.: Deep reinforcement learning: an overview. In: Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016: Volume 2. pp. 426–440. Springer (2018)

2016
[20]

In: Hou, Z., Ganesh, V

Pranger, S., Könighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Hou, Z., Ganesh, V. (eds.) Automated Technology for Verification and Analysis - 19th Interna- tional Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings. Lecture Notes in Computer Sc...

work page doi:10.1007/978-3-030-88885-5 2021
[21]

Raffin, A., Hill, A., Ernestus, M., Gleave, A., Kanervisto, A., Dormann, N.: Stable baselines3 (2019)

2019
[22]

In: Walsh, T., Shah, J., Kolter, Z

Rodríguez, A., Amir, G., Corsi, D., Sánchez, C., Katz, G.: Shield syn- thesis for LTL modulo theories. In: Walsh, T., Shah, J., Kolter, Z. (eds.) Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Con- ference on Innovative Applications of Artificial Intelligence, Fifteenth Sym- posium on Educational Advances in Artificial Intelligenc...

work page doi:10.1609/aaai.v39i14.33660 2025
[23]

MIT press (2018)

Sutton, R.S., Barto, A.G.: Reinforcement learning: An introduction. MIT press (2018)

2018

[1] [1]

MIT Press (2008)

Baier, C., Katoen, J.: Principles of Model Checking. MIT Press (2008)

2008

[2] [2]

In: Globersons, A., Mackey, L., Bel- grave, D., Fan, A., Paquet, U., Tomczak, J.M., Zhang, C

Banerjee, A., Rahmani, K., Biswas, J., Dillig, I.: Dynamic model predictive shield- ing for provably safe reinforcement learning. In: Globersons, A., Mackey, L., Bel- grave, D., Fan, A., Paquet, U., Tomczak, J.M., Zhang, C. (eds.) Advances in Neural Information Processing Systems 38: Annual Conference on Neural Inform- ation Processing Systems 2024, NeurI...

2024

[3] [3]

In: International Conference on Tools and Al- gorithms for the Construction and Analysis of Systems (TACAS)

Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis: Runtime enforcement for reactive systems. In: International Conference on Tools and Al- gorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 9035, pp. 533–548. Springer (2015)

2015

[4] [4]

In: International Conference on Bridging the Gap between AI and Reality

Brorholt, A.H., Jensen, P.G., Larsen, K.G., Lorber, F., Schilling, C.: Shielded re- inforcement learning for hybrid systems. In: International Conference on Bridging the Gap between AI and Reality. pp. 33–54. Springer (2023)

2023

[5] [5]

In: Das, S., Nowé, A., Vorobeychik, Y

Brorholt, A.H., Larsen, K.G., Schilling, C.: Compositional shielding and reinforce- ment learning for multi-agent systems. In: Das, S., Nowé, A., Vorobeychik, Y. (eds.) Proceedings of the 24th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2025, Detroit, MI, USA, May 19-23, 2025. pp. 399–407. International Foundation for Auton...

work page doi:10.5555/3709347.3743554 2025

[6] [6]

In: Williams, B., Chen, Y., Neville, J

Carr, S., Jansen, N., Junges, S., Topcu, U.: Safe reinforcement learning via shield- ing under partial observability. In: Williams, B., Chen, Y., Neville, J. (eds.) Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty- Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, 14 S. Pranger and B. Könighofer...

work page doi:10.1609/aaai.v37i12.26723 2023

[7] [7]

In: Flanagan, C., König, B

Chen, T., Forejt, V., Kwiatkowska, M.Z., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 18th In- ternational Conference, TACAS 2012, Held as Part of the European Joint Con- ferences on Theory and Practice of Software,...

work page doi:10.1007/978-3-642-28756-5 2012

[8] [8]

RLJ4, 1759–1780 (2024),https: //rlj.cs.umass.edu/2024/papers/Paper224.html

Corsi, D., Amir, G., Rodríguez, A., Katz, G., Sánchez, C., Fox, R.: Verification- guided shielding for deep reinforcement learning. RLJ4, 1759–1780 (2024),https: //rlj.cs.umass.edu/2024/papers/Paper224.html

2024

[9] [9]

Information and Computation285, 104886 (2022)

Eisentraut, J., Kelmendi, E., Křetínsk` y, J., Weininger, M.: Value iteration for simple stochastic games: Stopping criterion and learning algorithm. Information and Computation285, 104886 (2022)

2022

[10] [10]

In: International Conference on Computer Aided Verification

Gros, T.P., Hermanns, H., Hoffmann, J., Klauck, M., Köhl, M.A., Wolf, V.: Mo- gym: using formal models for training and verifying decision-making agents. In: International Conference on Computer Aided Verification. pp. 430–443. Springer (2022)

2022

[11] [11]

In: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications

Gross, D., Jansen, N., Junges, S., Pérez, G.A.: Cool-mc: a comprehensive tool for reinforcement learning and model checking. In: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications. pp. 41–49. Springer (2022)

2022

[12] [12]

In: Rocha, A.P., Steels, L., van den Herik, H.J

Gross, D., Spieker, H.: Probabilistic model checking of stochastic reinforcement learning policies. In: Rocha, A.P., Steels, L., van den Herik, H.J. (eds.) Pro- ceedings of the 16th International Conference on Agents and Artificial Intelli- gence, ICAART 2024, Volume 3, Rome, Italy, February 24-26, 2024. pp. 438–445. SCITEPRESS (2024). https://doi.org/10....

work page doi:10.5220/0012357700003636 2024

[13] [13]

International Journal on Software Tools for Technology Transfer pp

Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabil- istic model checker storm. International Journal on Software Tools for Technology Transfer pp. 1–22 (2021)

2021

[14] [14]

Könighofer, B., Bloem, R., Jansen, N., Junges, S., Pranger, S.: Shields for safe reinforcement learning. Commun. ACM68(11), 80–90 (2025). ht- tps://doi.org/10.1145/3715958,https://doi.org/10.1145/3715958

work page doi:10.1145/3715958 2025

[15] [15]

In: Gopalakrishnan, G., Qadeer, S

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) Proc. 23rd Interna- tional Conference on Computer Aided Verification (CAV’11). LNCS, vol. 6806, pp. 585–591. Springer (2011)

2011

[16] [16]

Reducibility among combinatorial problems

Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Prism-games 3.0: Stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, LosAngeles,CA,USA,July21-24,2020,Proceedings,PartII.pp.475–487.Lecture Notes in Computer Science, Springer (2020)....

work page doi:10.1007/978-3-030- 2020

[17] [17]

Kwiatkowski, A., Towers, M., Terry, J., Balis, J.U., Cola, G.D., Deleu, T., Goulão, M., Kallinteris, A., Krimmel, M., KG, A., Perez-Vicente, R., Pierré, A., Schulhoff, Easy-to-Use Shielding for Reinforcement Learning 15 S., Tai, J.J., Tan, H., Younis, O.G.: Gymnasium: A standard interface for rein- forcement learning environments (2024),https://arxiv.org/...

work page internal anchor Pith review Pith/arXiv arXiv 2024

[18] [18]

In: International Conference on Computer Aided Verification

Meggendorfer, T., Weininger, M.: Playing games with your pet: Extending the par- tial exploration tool to stochastic games. In: International Conference on Computer Aided Verification. pp. 359–372. Springer (2024)

2024

[19] [19]

In: Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016: Volume 2

Mousavi, S.S., Schukat, M., Howley, E.: Deep reinforcement learning: an overview. In: Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016: Volume 2. pp. 426–440. Springer (2018)

2016

[20] [20]

In: Hou, Z., Ganesh, V

Pranger, S., Könighofer, B., Posch, L., Bloem, R.: TEMPEST - synthesis tool for reactive systems and shields in probabilistic environments. In: Hou, Z., Ganesh, V. (eds.) Automated Technology for Verification and Analysis - 19th Interna- tional Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings. Lecture Notes in Computer Sc...

work page doi:10.1007/978-3-030-88885-5 2021

[21] [21]

Raffin, A., Hill, A., Ernestus, M., Gleave, A., Kanervisto, A., Dormann, N.: Stable baselines3 (2019)

2019

[22] [22]

In: Walsh, T., Shah, J., Kolter, Z

Rodríguez, A., Amir, G., Corsi, D., Sánchez, C., Katz, G.: Shield syn- thesis for LTL modulo theories. In: Walsh, T., Shah, J., Kolter, Z. (eds.) Thirty-Ninth AAAI Conference on Artificial Intelligence, Thirty-Seventh Con- ference on Innovative Applications of Artificial Intelligence, Fifteenth Sym- posium on Educational Advances in Artificial Intelligenc...

work page doi:10.1609/aaai.v39i14.33660 2025

[23] [23]

MIT press (2018)

Sutton, R.S., Barto, A.G.: Reinforcement learning: An introduction. MIT press (2018)

2018