-
Tools at the Frontiers of Quantitative Verification
Authors:
Roman Andriushchenko,
Alexander Bork,
Carlos E. Budde,
Milan Češka,
Kush Grover,
Ernst Moritz Hahn,
Arnd Hartmanns,
Bryant Israelsen,
Nils Jansen,
Joshua Jeppson,
Sebastian Junges,
Maximilian A. Köhl,
Bettina Könighofer,
Jan Křetínský,
Tobias Meggendorfer,
David Parker,
Stefan Pranger,
Tim Quatmann,
Enno Ruijters,
Landon Taylor,
Matthias Volk,
Maximilian Weininger,
Zhen Zhang
Abstract:
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused o…
▽ More
The analysis of formal models that include quantitative aspects such as timing or probabilistic choices is performed by quantitative verification tools. Broad and mature tool support is available for computing basic properties such as expected rewards on basic models such as Markov chains. Previous editions of QComp, the comparison of tools for the analysis of quantitative formal models, focused on this setting. Many application scenarios, however, require more advanced property types such as LTL and parameter synthesis queries as well as advanced models like stochastic games and partially observable MDPs. For these, tool support is in its infancy today. This paper presents the outcomes of QComp 2023: a survey of the state of the art in quantitative verification tool support for advanced property types and models. With tools ranging from first research prototypes to well-supported integrations into established toolsets, this report highlights today's active areas and tomorrow's challenges in tool-focused research for quantitative verification.
△ Less
Submitted 22 May, 2024;
originally announced May 2024.
-
Automata Learning meets Shielding
Authors:
Martin Tappler,
Stefan Pranger,
Bettina Könighofer,
Edi Muškardin,
Roderick Bloem,
Kim Larsen
Abstract:
Safety is still one of the major research challenges in reinforcement learning (RL). In this paper, we address the problem of how to avoid safety violations of RL agents during exploration in probabilistic and partially unknown environments. Our approach combines automata learning for Markov Decision Processes (MDPs) and shield synthesis in an iterative approach. Initially, the MDP representing th…
▽ More
Safety is still one of the major research challenges in reinforcement learning (RL). In this paper, we address the problem of how to avoid safety violations of RL agents during exploration in probabilistic and partially unknown environments. Our approach combines automata learning for Markov Decision Processes (MDPs) and shield synthesis in an iterative approach. Initially, the MDP representing the environment is unknown. The agent starts exploring the environment and collects traces. From the collected traces, we passively learn MDPs that abstractly represent the safety-relevant aspects of the environment. Given a learned MDP and a safety specification, we construct a shield. For each state-action pair within a learned MDP, the shield computes exact probabilities on how likely it is that executing the action results in violating the specification from the current state within the next $k$ steps. After the shield is constructed, the shield is used during runtime and blocks any actions that induce a too large risk from the agent. The shielded agent continues to explore the environment and collects new data on the environment. Iteratively, we use the collected data to learn new MDPs with higher accuracy, resulting in turn in shields able to prevent more safety violations. We implemented our approach and present a detailed case study of a Q-learning agent exploring slippery Gridworlds. In our experiments, we show that as the agent explores more and more of the environment during training, the improved learned models lead to shields that are able to prevent many safety violations.
△ Less
Submitted 4 December, 2022;
originally announced December 2022.
-
TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments
Authors:
Stefan Pranger,
Bettina Könighofer,
Lukas Posch,
Roderick Bloem
Abstract:
We present Tempest, a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. A shield is a special type of reactive system used for run-time enforcement; i.e., a shield enforces a given qualitative or quantitative specification of a running system while interfering with its operation…
▽ More
We present Tempest, a synthesis tool to automatically create correct-by-construction reactive systems and shields from qualitative or quantitative specifications in probabilistic environments. A shield is a special type of reactive system used for run-time enforcement; i.e., a shield enforces a given qualitative or quantitative specification of a running system while interfering with its operation as little as possible. Shields that enforce a qualitative or quantitative specification are called safety-shields or optimal-shields, respectively. Safety-shields can be implemented as pre-shields or as post-shields, optimal-shields are implemented as post-shields. Pre-shields are placed before the system and restrict the choices of the system. Post-shields are implemented after the system and are able to overwrite the system's output. Tempest is based on the probabilistic model checker Storm, adding model checking algorithms for stochastic games with safety and mean-payoff objectives. To the best of our knowledge, Tempest is the only synthesis tool able to solve 2-1/2-player games with mean-payoff objectives without restrictions on the state space. Furthermore, Tempest adds the functionality to synthesize safe and optimal strategies that implement reactive systems and shields
△ Less
Submitted 26 May, 2021;
originally announced May 2021.
-
Adaptive Shielding under Uncertainty
Authors:
Stefan Pranger,
Bettina Könighofer,
Martin Tappler,
Martin Deixelberger,
Nils Jansen,
Roderick Bloem
Abstract:
This paper targets control problems that exhibit specific safety and performance requirements. In particular, the aim is to ensure that an agent, operating under uncertainty, will at runtime strictly adhere to such requirements. Previous works create so-called shields that correct an existing controller for the agent if it is about to take unbearable safety risks. However, so far, shields do not c…
▽ More
This paper targets control problems that exhibit specific safety and performance requirements. In particular, the aim is to ensure that an agent, operating under uncertainty, will at runtime strictly adhere to such requirements. Previous works create so-called shields that correct an existing controller for the agent if it is about to take unbearable safety risks. However, so far, shields do not consider that an environment may not be fully known in advance and may evolve for complex control and learning tasks. We propose a new method for the efficient computation of a shield that is adaptive to a changing environment. In particular, we base our method on problems that are sufficiently captured by potentially infinite Markov decision processes (MDP) and quantitative specifications such as mean payoff objectives. The shield is independent of the controller, which may, for instance, take the form of a high-performing reinforcement learning agent. At runtime, our method builds an internal abstract representation of the MDP and constantly adapts this abstraction and the shield based on observations from the environment. We showcase the applicability of our method via an urban traffic control problem.
△ Less
Submitted 8 October, 2020;
originally announced October 2020.
