7 papers
model-checking
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...
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...
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...