Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 14:00 - 14:30 at Sala III - Probabilistic Systems Chair(s): Justin Hsu

The state space explosion problem is among the largest impediments to the performance of any model checker. Modelling languages for compositional systems contribute to this problem by placing each instruction of an instruction sequence onto a dedicated transition, giving concurrent processes opportunities to interleave after every instruction. Users wishing to avoid the excessive number of interleavings caused by this default can choose to explicitly declare instruction sequences as atomic, which however requires careful considerations regarding the impact this might have on the model as well as on the properties that are to be checked. We instead propose a preprocessing technique that automatically identifies instruction sequences that can safely be considered atomic. This is done in the context of concurrent variable-decorated Markov Decision Processes. Our approach is compatible with any off-the-shelf probabilistic model checker. We prove that our transformation preserves maximal reachability probabilities and present case studies to illustrate its usefulness.

Mon 14 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Probabilistic SystemsVMCAI at Sala III
Chair(s): Justin Hsu University of Wisconsin-Madison, USA
14:00
30m
Talk
Syntactic Partial Order Compression for Probabilistic Reachability
VMCAI
Gereon Fox , Daniel Stan , Holger Hermanns Saarland University
14:30
30m
Talk
Termination of Nondeterministic Probabilistic Programs
VMCAI
Hongfei Fu IST Austria, Krishnendu Chatterjee IST Austria
15:00
30m
Talk
Combining Refinement of Parametric Models with Goal-Oriented Reduction of Dynamics
VMCAI
Stefan Haar , Juraj Kolčák LSV, CNRS & ENS Cachan, University Paris Saclay, Loïc Paulevé