Author name cluster

Roderick Bloem

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

5 papers

2 author rows

I&C Journal 2023 Journal Article

Learning Mealy machines with one timer

Frits Vaandrager
Masoud Ebrahimi
Roderick Bloem

We present Mealy machines with a single timer (MM1Ts), a class of sufficiently expressive models to describe the real-time behavior of many realistic applications that we can learn efficiently. We show how we can obtain learning algorithms for MM1Ts via a reduction to the problem of learning Mealy machines. We describe an implementation of an MM1T learner on top of LearnLib and compare its performance with recent algorithms proposed by Aichernig et al. and An et al. on several realistic benchmarks.

Details DOI

ICAPS Conference 2023 Conference Paper

Safety Shielding under Delayed Observation

Filip Cano 0001
Alexander Palmisano
Martin Fränzle
Roderick Bloem
Bettina Könighofer

Agents operating in physical environments need to be able to handle delays in the input and output signals since neither data transmission nor sensing or actuating the environment are instantaneous. Shields are correct-by-construction runtime enforcers that guarantee safe execution by correcting any action that may cause a violation of a formal safety specification. Besides providing safety guarantees, shields should interfere minimally with the agent. Therefore, shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. Current shielding approaches do not consider possible delays in the input signals in their safety analyses. In this paper, we address this issue. We propose synthesis algorithms to compute delay-resilient shields that guarantee safety under worst-case assumptions on the delays of the input signals. We also introduce novel heuristics for deciding between multiple corrective actions, designed to minimize future shield interferences caused by delays. As a further contribution, we present the first integration of shields in a realistic driving simulator. We implemented our delayed shields in the driving simulator Carla. We shield potentially unsafe autonomous driving agents in different safety-critical scenarios and show the effect of delays on the safety analysis.

Details

AAAI Conference 2018 Conference Paper

Safe Reinforcement Learning via Shielding

Mohammed Alshiekh
Roderick Bloem
Rüdiger Ehlers
Bettina Könighofer
Scott Niekum
Ufuk Topcu

Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given the temporal logic speciﬁcation that is to be obeyed by the learning system, we propose to synthesize a reactive system called a shield. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the speciﬁcation. We discuss which requirements a shield must meet to preserve the convergence guarantees of the learner. Finally, we demonstrate the versatility of our approach on several challenging reinforcement learning scenarios.

PDF Details

IROS Conference 2015 Conference Paper

Synthesizing cooperative reactive mission plans

Rüdiger Ehlers
Robert Könighofer
Roderick Bloem

By performing synthesis from formal high-level mission specifications, we can obtain robot controllers that are guaranteed to operate correctly under the specified environment conditions. Such conditions must be stated in the specification whenever there is no way in which the robot's task can be fulfilled without them holding, and they relate the possible behaviors of the environment with the behavior of the robot. Contemporary synthesis algorithms however frequently construct implementations that try to trivially satisfy their specifications by actively working towards the violation of the assumptions, which is undesirable behavior.

Details

SAT Conference 2007 Conference Paper

Fault Localization and Correction with QBF

Stefan Staber
Roderick Bloem

Abstract In this paper, we study the use of QBF solvers for fault localization and correction of sequential circuits. Given a violated specification, we compute whether the circuit can be repaired by evaluating a sequence of quantified Boolean formulas. If a repair exists, it can be extracted from a certificate for another quantified Boolean formula. Because it only finds components when a repair is possible, this approach is more precise than a satisfiability-based approach that we have developed earlier. We demonstrate this in an experimental evaluation.

Details