24 papers
formal-methods
Efficient Model Checking of Safety Properties
. We consider the problems of identifying LTL safety proper- ties and translating them to finite automata. We present an algorithm for constructing a finite automata recognising informative prefixes of LTL formulas based on [1]. The implementation also includes a procedure for de...
Transition Systems over Games
1. A game, which is essentially a bipartite graph describing the We describe a framework for game semantics combining opera- moves that can be made as play passes between the different tional and denotational accounts. A game is a bipartite graph of positions of the two players....
Shield Synthesis: Runtime Enforcement for Reactive Systems
. Scalability issues may prevent users from verifying critical proper- ties of a complex hardware design. In this situation, we propose to synthesize a “safety shield” that is attached to the design to enforce the properties at run time. Shield synthesis can succeed where model c...
Safe Reinforcement Learning via Shielding
reward Environment Learning Agent Reinforcement learning algorithms discover policies that observation maximize reward, but do not necessarily guarantee safety dur- actions ing learning or execution phases. We introduce a new ap- proach to learn optimal policies while enforcing p...
Sound Value Iteration
. Computing reachability probabilities is at the heart of prob- abilistic model checking. All model checkers compute these probabilities in an iterative fashion using value iteration. This technique approximates a xed point from below by determining reachability probabilities for...
Symbolic Verification of GOLOG Programs with First-Order BDDs
loop: while (∃x.OnRobot(x)) do πx:Dish unload (x) endWhile; G OLOG is an agent language that allows defining behaviours πy:Room { goto(y); in terms of programs over actions defined in a Situation Cal- while (∃xDirty(x, y)) do culus action theory. Often it is vital to verify such...
A Symbolic Approach to Safety LTL Synthesis
. Temporal synthesis is the automated design of a system that interacts with an environment, using the declarative specification of the system’s behavior. A popular language for providing such a specification is Linear Temporal Logic, or LTL. LTL synthesis in the general case has...
Safe Multi-Agent Reinforcement Learning via Shielding
A recent work [1] developed a shielding framework for single- Multi-agent reinforcement learning (MARL) has been increasingly agent reinforcement learning (RL), which synthesizes a shield to used in a wide range of safety-critical applications, which require enforce the correctne...
Automata Cascades: Expressivity and Sample Complexity
Every automaton can be decomposed into a cascade of ba- sic automata. This is the Prime Decomposition Theorem by Krohn and Rhodes. We show that cascades allow for describ- ing the sample complexity of automata in terms of their com- ponents. In particular, we show that the sample...
First-Order Game Logic and Modal Mu-Calculus
Three decades later, Parikh’s problem has been solved: This paper investigates first-order game logic and first-order Game logic is less expressive than the modal μ-calculus [2], modal μ-calculus, which extend their propositional modal because it embeds into the two-variable frag...
Verifiable and Compositional Reinforcement Learning Systems
However, there remain significant barriers to their deploy- ment in safety-critical engineering applications. Autonomous We propose a framework for verifiable and compositional vehicles, manufacturing robotics, and power systems manage- reinforcement learning (RL) in which a coll...
Complexity of Safety and coSafety Fragments of Linear Temporal Logic
ones in such a way to satisfy the formula. LTL realizability Linear Temporal Logic (LTL) is the de-facto standard tempo- is 2EXPTIME-complete, on both infinite (Rosner 1992) and ral logic for system specification, whose foundational prop- finite (De Giacomo and Vardi 2015) traces...
Correct-by-Construction Reinforcement Learning of Cardiac Pacemakers from Duration Calculus Requirements
A common cardiac arrhythmia, known as heart block or AV block, is a condition where the electrical signal con- As the complexity of artificial pacemakers continues to grow, trolling the ventricular contractions are partially or com- the importance of capturing its functional corr...
Temporal Logics
Pure-Past Action Masking
by (default or sampled) safe ones; action projection, e.g., (Cheng et al. 2019), where unsafe actions are replaced by We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for safe reinforcement learning. projecting them to the safe action space; an...
Symbolic Solution of Emerson-Lei Games for Reactive Synthesis
. Emerson-Lei conditions have recently attracted attention due to both their succinctness and their favorable closure properties. In the current work, we show how infinite-duration games with Emerson-Lei objectives can be analyzed in two different ways. First, we show that the Zi...
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
approaches aim to provide high-assurance quantitative guar- Ensuring that AI systems reliably and robustly antees about the safety of an AI system’s behaviour through avoid harmful or dangerous behaviours is a cru- the use of three core components — a formal safety specifi- cial...
Explainably Safe Reinforcement Learning
Trust in a decision-making system requires both safety guarantees and the ability to interpret and understand its behavior. This is particularly important for learned systems, whose decision-making processes are often highly opaque. Shielding is a prominent model-based technique...
Probabilistic Shielding for Safe Reinforcement Learning
at least some probability p. This framework comes from a probabilistic version of what is usually called the “safety” In real-life scenarios, a Reinforcement Learning (RL) agent aiming to maximise their reward, must often also behave in a fragment of Linear Temporal Logic (LTL) (...
ProSh: Probabilistic Shielding for Model-free Reinforcement Learning
not assume access to a simulator or environment abstraction, and Safety is a major concern in reinforcement learning (RL): we aim at is compatible with continuous environments. developing RL systems that not only perform optimally, but are also We also show that optimizing over s...