Publications

| Sorted by Date | Classified by Publication Type | Classified by Research Category |

Abstraction-Refinement for Hierarchical Probabilistic Models

Sebastian Junges and Matthijs T. J. Spaan. Abstraction-Refinement for Hierarchical Probabilistic Models. In Proc. Int. Conf. on Computer Aided Verification, pp. 102–123, 2022.

Download

pdf 

Abstract

Markov decision processes are a ubiquitous formalism for modelling systems with non-deterministic and probabilistic behavior. Verification of these models is subject to the famous state space explosion problem. We alleviate this problem by exploiting a hierarchical structure with repetitive parts. This structure not only occurs naturally in robotics, but also in probabilistic programs describing, e.g., network protocols. Such programs often repeatedly call a subroutine with similar behavior. In this paper, we focus on a local case, in which the subroutines have a limited effect on the overall system state. The key ideas to accelerate analysis of such programs are (1) to treat the behavior of the subroutine as uncertain and only remove this uncertainty by a detailed analysis if needed, and (2) to abstract similar subroutines into a parametric template, and then analyse this template. These two ideas are embedded into an abstraction-refinement loop that analyses hierarchical MDPs. A prototypical implementation shows the efficacy of the approach.

BibTeX Entry

@InProceedings{Junges22cav,
  author =       {Sebastian Junges and Matthijs T. J. Spaan},
  title =        {Abstraction-Refinement for Hierarchical
                  Probabilistic Models},
  booktitle =    {Proc. Int. Conf. on Computer Aided Verification},
  year =         2022,
  pages =        {102--123}
}

Note: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

Generated by bib2html.pl (written by Patrick Riley) on Thu Feb 29, 2024 16:15:45 UTC