Evènement pour le groupe
Séminaire Méthodes Formelles
Date | 2021-06-29 07:00-07:00 |
Titre | Multi-cost Bounded Tradeoff Analysis in MDP |
Résumé | We present a memory-efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures. The key problem at hand is to check whether there exists a scheduler for a given MDP such that all objectives over cost vectors are fulfilled. We cover multi-objective reachability and expected cost objectives, and combinations thereof. An empirical evaluation using a prototypical implementation on top of the Storm model checker shows the scalability of our approach both in terms of memory consumption and runtime.
(Joint work with Arnd Hartmanns, Sebastian Junges and Tim Quatmann) |
Lieu | Online |
Orateur | Joost-Pieter Katoen |
Url | RWTH Aachen University and University of Twente |
Aucun document lié à cet événement.
RetourRetour à l'index