13th Workshop on Quantitative Aspects of Programming Languages

Saturday, April 11th
09h30 - 10h30
11h00 - 12h30
  • Fabio Martinelli, Ilaria Matteucci and Francesco Santini. Semiring-based Specification Approaches for Quantitative Security.
  • Rajesh Kumar, Dennis Guck and Marielle Stoelinga. Time Dependent Analysis with Dynamic Counter Measure Trees
  • Yusuke Kawamoto and Thomas Given-Wilson. Quantitative Information Flow for Scheduler-Dependent Systems
14h30 - 16h00
  • Matias David Lee and Erik de Vink. Rooted probabilistic branching bisimulation as a congruence
  • Diego Latella, Mieke Massink and Erik De Vink. A Definition Scheme for Quantitative Bisimulations
  • Alessandro Aldini and Marco Bernardo. Expected-Delay-Summing Weak Bisimilarity for Markov Automata
16h30 - 17h30
  • Luca Bortolussi and Jane Hillston. Efficient Checking of Individual Rewards Properties in Markov Population Models
  • Arnd Hartmanns and Holger Hermanns. Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage
Sunday, April 12th
09h30 - 10h30
  • Invited talk Holger Hermanns Optimal Continuous Time Markov Decisions

    One of the most intriguing challenges in the veri fication of stochastic and non-deterministic systems is the time optimal scheduling of Markov decision processes running in continuous time. A multitude of sophisticated model checking algorithms have been proposed especially in the context of fi nite horizon reachability objectives since this is the basis of temporal-logic model checking. However, no proper benchmarking has been performed thus far.
    We present a comparative evaluation of the core algorithmic concepts on an extensive set of benchmarks varying over all key parameters: model size, amount of non-determinism, time horizon, and precision. As the second main contribution, we discuss a novel and yet simple solution: an algorithm originally developed for a restricted subclass of both models and schedulers can be twisted so as to become competitive with the more sophisticated algorithms in full generality.
    Joint work with Yuliya Butkova, Hassan Hatefi, and Jan Krcal

11h00 - 12h30
  • Invited talk - TBC. Title to be announced
  • Luca Bortolussi, Rocco De Nicola, Vashti Galpin, Stephen Gilmore, Jane Hillston, Diego Latella, Michele Loreti and Mieke Massink. CARMA: Collective Adaptive Resource-sharing Markovian Agents
  • Mads Rosendahl and Maja Kirkeby. Probabilistic Output Analysis by Program Manipulation
  • Closing.

Last modified: Tue Apr 7 14:25:15 CEST 2015