research
∙
07/19/2023
Learning Formal Specifications from Membership and Preference Queries
Active learning is a well-studied approach to learning formal specificat...
share
research
∙
05/23/2023
Search and Explore: Symbiotic Policy Synthesis in POMDPs
This paper marries two state-of-the-art controller synthesis methods for...
research
∙
05/01/2023
Efficient Sensitivity Analysis for Parametric Robust Markov Chains
We provide a novel method for sensitivity analysis of parametric robust ...
research
∙
01/26/2023
Robust Almost-Sure Reachability in Multi-Environment MDPs
Multiple-environment MDPs (MEMDPs) capture finite sets of MDPs that shar...
research
∙
01/24/2023
A Practitioner's Guide to MDP Model Checking Algorithms
Model checking undiscounted reachability and expected-reward properties ...
research
∙
09/15/2022
COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking
This paper presents COOL-MC, a tool that integrates state-of-the-art rei...
research
∙
07/14/2022
Parameter Synthesis in Markov Models: A Gentle Survey
This paper surveys the analysis of parametric Markov models whose transi...
research
∙
06/06/2022
Abstraction-Refinement for Hierarchical Probabilistic Models
Markov decision processes are a ubiquitous formalism for modelling syste...
research
∙
05/17/2022
Sampling-Based Verification of CTMCs with Uncertain Rates
We employ uncertain parametric CTMCs with parametric transition rates an...
research
∙
05/12/2022
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
A desired property of randomized systems, represented by probabilistic p...
research
∙
04/02/2022
Safe Reinforcement Learning via Shielding for POMDPs
Reinforcement learning (RL) in safety-critical environments requires an ...
research
∙
03/21/2022
Inductive Synthesis of Finite-State Controllers for POMDPs
We present a novel learning framework to obtain finite-state controllers...
research
∙
12/24/2021
Scenario-Based Verification of Uncertain Parametric MDPs
We consider parametric Markov decision processes (pMDPs) that are augmen...
research
∙
12/01/2021
Querying Labelled Data with Scenario Programs for Sim-to-Real Validation
Simulation-based testing of autonomous vehicles (AVs) has become an esse...
research
∙
11/08/2021
Gradient-Descent for Randomized Controllers under Partial Observability
Randomization is a powerful technique to create robust controllers, in p...
research
∙
06/30/2021
Convex Optimization for Parameter Synthesis in MDPs
Probabilistic model checking aims to prove whether a Markov decision pro...
research
∙
05/27/2021
Model Repair Revamped: On the Automated Synthesis of Markov Chains
This paper outlines two approaches|based on counterexample-guided abstra...
research
∙
05/26/2021
Model Checking Finite-Horizon Markov Chains with Probabilistic Inference
We revisit the symbolic verification of Markov chains with respect to fi...
research
∙
05/26/2021
Runtime Monitoring for Markov Decision Processes
We investigate the problem of monitoring partially observable systems wi...
research
∙
03/09/2021
Entropy-Guided Control Improvisation
High level declarative constraints provide a powerful (and popular) way ...
research
∙
01/29/2021
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
This paper presents a novel method for the automated synthesis of probab...
research
∙
09/28/2020
The Complexity of Reachability in Parametric Markov Decision Processes
This article presents the complexity of reachability decision problems f...
research
∙
09/24/2020
Robust Finite-State Controllers for Uncertain POMDPs
Uncertain partially observable Markov decision processes (uPOMDPs) allow...
research
∙
06/30/2020
Verification of indefinite-horizon POMDPs
The verification problem in MDPs asks whether, for any policy resolving ...
research
∙
06/30/2020
Enforcing Almost-Sure Reachability in POMDPs
Partially-Observable Markov Decision Processes (POMDPs) are a well-known...
research
∙
04/30/2020
PrIC3: Property Directed Reachability for MDPs
IC3 has been a leap forward in symbolic model checking. This paper propo...
research
∙
02/17/2020
The Probabilistic Model Checker Storm
We present the probabilistic model checker Storm. Storm supports the ana...
research
∙
12/24/2019
Scenario-Based Verification of Uncertain MDPs
We consider Markov decision processes (MDPs) in which the transition pro...
research
∙
07/19/2019
Are Parametric Markov Chains Monotonic?
This paper presents a simple algorithm to check whether reachability pro...
research
∙
04/28/2019
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Probabilistic programs are key to deal with uncertainty in e.g. controll...
research
∙
04/02/2019
On the Complexity of Reachability in Parametric Markov Decision Processes
This paper studies parametric Markov decision processes (pMDPs), an exte...
research
∙
03/16/2019
Parameter Synthesis for Markov Models
Markov chain analysis is a key technique in reliability engineering. A p...
research
∙
03/13/2019
Safety Analysis for Vehicle Guidance Systems with Dynamic Fault Trees
This paper considers the design-phase safety analysis of vehicle guidanc...
research
∙
02/15/2019
Shepherding Hordes of Markov Chains
This paper considers large families of Markov chains (MCs) that are defi...
research
∙
09/28/2018
The Partially Observable Games We Play for Cyber Deception
Progressively intricate cyber infiltration mechanisms have made conventi...
research
∙
07/16/2018
Shielded Decision-Making in MDPs
A prominent problem in artificial intelligence and machine learning is t...
research
∙
03/14/2018
One Net Fits All: A unifying semantics of Dynamic Fault Trees using GSPNs
Dynamic Fault Trees (DFTs) are a prominent model in reliability engineer...
research
∙
10/24/2017
Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
We study finite-state controllers (FSCs) for partially observable Markov...
research
∙
08/14/2017
Motion Planning under Partial Observability using Game-Based Abstraction
We study motion planning problems where agents move inside environments ...
research
∙
10/28/2016
Probabilistic Model Checking for Complex Cognitive Tasks -- A case study in human-robot interaction
This paper proposes to use probabilistic model checking to synthesize op...
research
∙
10/27/2016