Program
Wednesday, September 15
| QEST/NSMC | ||
|---|---|---|
| 9:00-4:30 | Tutorials | |
| 9:00-12:00 | Jane Hillston and Mirco Tribastone. Scalable Differential Analysis of Large Process Algebra Models | |
| 10:30-11:00 | Break | |
| 9:00-12:00 | Larry Leemis. Reliability Models | |
| 12:00-1:30 | Lunch | |
| 1:30-4:30 | Maria Grazia Vigliotti and Andrea Marin. From Systems to Components: Constructive Methods for Product-Form Solutions | |
| 3:00-3:30 | Break | |
| 1:30-4:30 | William H. Sanders. Quantitative Evaluation of Security Metrics | |
| 6:30 pm | Reception at the Wren Building | |
Thursday, September 16
| QEST | NSMC | |
|---|---|---|
| 8:00-8:30 | Opening Remarks | |
| 8:30-9:30 | Invited Talk: Joseph L. Hellerstein |
|
| 9:30-10:00 | Coffee Break | |
| 10:00-12:00 | Probabilistic Model Checking Session Chair: Susanna Donatelli |
Matrix Analytic Methods Session Chair: Peter Buchholz |
| 10:00-10:30 | Bo Friis Nielsen, Flemming Nielson, and Hanne Riis Nielson. Model checking multivariate state rewards | Juan F. Perez and Benny Van Houdt. Analyzing M/G/1-type Markov chains with low-rank downward transitions |
| 10:30-11:00 | Miguel E. Andres, Catuscia Palamidessi, Peter van Rossum, and Ana Sokolova. Information hiding in probabilistic concurrent systems | Bruno Iannazzo and Federico Poloni. The worst-case scenario in nonlinear matrix equations |
| 11:00-11:30 | Ralf Wimmer, Bettina Braitling, Bernd Becker, Ernst Moritz Hahn, Pepijn Crouzen, Holger Hermanns, Abhishek Dhama, and Oliver Theel. Symblicit calculation of long-run averages for concurrent probabilistic systems | Giuliano Casale, Peter G. Harrison, and Maria Grazia Vigliotti. Product-form approximation of tandem queues via matrix geometric methods |
| 11:30-12:00 | Nils Jansen, Erika Ábrahám, Ralf Wimmer, Bernd Becker, and Joost-Pieter Katoen. DTMC model checking by SCC reduction | Dario A. Bini, Beatrice Meini, and Federico Poloni. On the solution of a quadratic vector equation arising in Markovian binary trees |
| 12:00-1:30 | Lunch | |
| 1:30-3:30 | Performance Evaluation and Queuing Theory Session Chair: Vittoria de Nitto |
Bounding Techniques Session Chair: Ivana Pultarova |
| 1:30-2:00 | Benny Van Houdt. A phase-type representation for the queue length distribution of a semi-Markovian queue | Ana Busic, Hilal Djafri, and Jean-Michel Fourneau. Stochastic bounds for censored Markov chains |
| 2:00-2:30 | Jens Happe, Henning Groenda, Michael Hauck, and Ralf H. Reussner. A prediction model for software performance in symmetric multiprocessing environments | Ana Busic and Jean-Michel Fourneau. Iterative component-wise bounds for the steady-state distribution of a Markov chain |
| 2:30-3:00 | Adetokunbo Makanju, Nur Zincir-Heywood, and Evangelos Milios. An evaluation of entropy based approaches to alert detection in high performance cluster logs | Peter Buchholz. Bounding reward measures of Markov models using Markov decision processes |
| 3:00-3:10 | Susanna Donatelli and Elvio Gilberto Amparore. A new DSPN and GSPN solver for GreatSPN | Jeffrey P. Buzen and Mark Tomasik. Shaped simulation of stationary Markov chains |
| 3:10-3:20 | Ana Busic and Jean-Michel Fourneau. A toolbox for component-wise bounds of the steady-state distribution of a DTMC | |
| 3:20-3:30 | Ana Busic, Bruno Gaujal, Gael Gorgo, and Jean-Marc Vincent. PSI2: Envelope perfect sampling of non monotone systems | |
| 3:30-4:00 | Coffee Break | |
| 4:00-5:00 | Distribution Fitting Session Chair: Giuliano Casale |
Transient Solutions Session Chair: William Knottenbelt |
| 4:00-4:30 | Falko Bause, Peter Buchholz, and Jan Kriege. ProFiDo - the processes fitting toolkit Dortmund | Andras Horvath, Lorenzo Ridi, and Enrico Vicario. Approximating distributions and transient probabilities of Markov chains by Bernstein expolynomial functions |
| 4:30-5:00 | Falko Bause and Gábor Horváth. Fitting Markovian arrival processes by incorporating correlation into phase type renewal processes | Roger B. Sidje. Inexact uniformization and GMRES for computing transient and stationary probabilities |
| 5:00-6:30 | Distribution Fitting Session Chair: Giuliano Casale |
Practical Considerations 1 Session Chair: Benny Van Houdt |
| 5:00-5:30 | Levente Bodrog, Peter Buchholz, Jan Kriege, and Miklos Telek. Canonical form based MAP(2) fitting | Ho Woo Lee, Jung Woo Baek, Se Won Lee, and Soohan Ahn. A MAP-modulated fluid flow queueing model under workload control |
| 5:30-6:00 | Bruno R. C. Magalhaes, Nicholas J. Dingle, and William J. Knottenbelt. GPU-enabled steady-state solution of large Markov models | |
| 6:00-6:30 | Elvio Amparore Gilberto and Susanna Donatelli. Revisiting the iterative solution of Markov regenerative processes | |
Friday, September 17
| QEST | NSMC | |
|---|---|---|
| 8:30-9:30 | Invited Talk: William J. Stewart |
|
| 9:30-10:00 | Coffee Break | |
| 10:00-11:00 | Compositional Probabilistic Model Checking Session Chair: Andrew Miner |
Nearly Completely Decomposable Markov Chains Session Chair: Roger Sidje |
| 10:00-10:30 | Benoît Caillaud, Benoit Delahaye, Kim G. Larsen, Axel Legay, Mikkel Larsen Pedersen, and Andrzej Wasowski. Compositional design methodology with constraint Markov chains | Ralph Abbey and Carl Meyer. Algorithm comparisons for decoupling nearly completely decomposable Markov chains |
| 10:30-11:00 | Lu Feng, Marta Kwiatkowska, and David Parker. Compositional verification of probabilistic systems using learning | Carl D. Meyer and Charles D. Wessell. Stochastic consensus clustering |
| 11:00-12:00 | Compositional Probabilistic Model Checking Session Chair: Andrew Miner |
Markov Population Models Session Chair: Michele Benzi |
| 11:00-11:30 | Jayanand Asok Kumar and Shobha Vasudevan. Automatic compositional reasoning for probabilistic model checking of hardware designs | Hal Caswell. Perturbation analysis of absorbing Markov chains: A matrix calculus approach |
| 11:30-11:40 | Susanna Donatelli and Elvio Gilberto Amparore. MC4CSLTA: An efficient model checking tool for CSLTA | Tugrul Dayar, Holger Hermanns, David Spieler, and Verena Wolf. Bounding the equilibrium distribution of Markov population models |
| 11:40-11:50 | Michael Smith. Abstraction and model checking in the PEPA plug-in for Eclipse | |
| 11:50-12:00 | Xin Zhang and Franck van Breugel. Model checking randomized algorithms with Java PathFinder | |
| 12:00-1:30 | Lunch | |
| 1:30-3:30 | Foundations Session Chair: Franck van Breugel |
MultiLevel Methods Session Chair: Tugrul Dayar |
| 1:30-2:00 | Michael Huth, Nir Piterman, and Daniel Wagner. p-Automata: New foundations for discrete-time probabilistic verification | Hans De Sterck, Killian Miller, Manda Winlaw, Geoffrey Sanders, Eran Treister, and Irad Yavneh. Fast multilevel methods for Markov chains |
| 2:00-2:30 | Radu Mardare and Luca Cardelli. The measurable space of stochastic processes | Ivo Marek, Petr Mayer, and Ivana Pultarova. A study of convergence of multilevel iterative aggregation-disaggregation methods |
| 2:30-3:00 | Luca Bortolussi, Vashti Galpin, Jane Hillston, and Mirco Tribastone. Hybrid semantics for PEPA | Michele Benzi and Verena Kuhlemann. Restricted additive Schwarz methods for Markov chains |
| 3:00-3:10 | Gabriele Kotsis and Martin Pinzger. AWPS - Simulation based automated web performance analysis and prediction | Johann Schuster and Markus Siegle. Speeding up the symbolic multilevel algorithm |
| 3:10-3:20 | Frederic Didier, Maria Mateescu, Verena Wolf, and Thomas A. Henzinger. SABRE: A tool for stochastic analysis of biochemical reaction networks | |
| 3:20-3:30 | Junaid Babar and Andrew Miner. Meddly: Multi-way and edge-valued decision diagram library | |
| 3:30-4:00 | Coffee Break | |
| 4:00-5:30 | Markov Decision Processes Session Chair: Roberto Segala |
Practical Considerations 2 Session Chair: Susanna Donatelli |
| 4:00-4:30 | Vijay Anand Korthikanti, Mahesh Viswanathan, YoungMin Kwon, and Gul Agha. Reasoning about MDPs as transformers of probability distributions | Ricardo M. Czekster, Paulo Fernandes, Afonso Sales, and Thais Webber. Restructuring tensor products to enhance the numerical solution of structured Markov chains |
| 4:30-5:00 | Martin R. Neuhäußer and Lijun Zhang. On continuous-time Markov decision processes | Benny Van Houdt. Numerical solution of polling systems for analyzing networks on chips |
| 5:00-5:30 | Ashutosh Trivedi and Dominik Wojtczak. Timed branching processes | |
| 7:15 | Banquet at Christiana Campbell's Tavern | |
Saturday, September 18
| QEST | |
|---|---|
| 9:00-10:30 | Solution Techniques Session Chair: Jean Michel Fourneau |
| 9:00-9:30 | Andras Horvath, Lorenzo Ridi, and Enrico Vicario. Transient analysis of generalised semi-Markov processes using transient stochastic state classes |
| 9:30-10:00 | Rena Bakhshi, Joerg Endrullis, Stefan Endrullis, Wan Fokkink, and Boudewijn Haverkort. Automating the mean-field method for large dynamic networks |
| 10:00-10:30 | Daniel Reijsbergen, Pieter-Tjerk de Boer, Werner Scheinhardt, and Boudewijn Haverkort. Rare event simulation for highly dependable systems with fast repairs |
| 10:30-11:00 | Coffee Break |
| 11:00-12:00 | Applications 1 Session Chair: William Sanders |
| 11:00-11:30 | Béatrice Bérard, John Mullins, and Mathieu Sassolas. Quantifying opacity |
| 11:00-11:30 | Jasper Berendsen, David N. Jansen, and Frits Vaandrager. Fortuna: Model checking priced probabilistic timed automata |
| 12:00-1:30 | Lunch |
| 1:30-3:00 | Applications 2 Session Chair: Peter Buchholz |
| 1:30-2:00 | Derek Doran and Swapna Gokhale. Searching for heavy tails in web robot traffic |
| 2:00-2:30 | Parasara Sridhar Duggirala, Sayan Mitra, Rakesh Kumar, and Dean Glazeski. On the theory of stochastic processors | 3:00-3:30 | QEST Closing Remarks |
