[Front cover]

[Copyright notice] (PDF)

pp. iv

Table of contents (PDF)

pp. v-viii

Steering Committee (PDF)

pp. xiv

Title Page i (PDF)

pp. i

Title Page iii (PDF)

pp. iii

Message from the General Chair (PDF)

pp. ix-x

Message from the Program Committee Co-chairs (PDF)

pp. xi-xii

Organizing Committee (PDF)

pp. xiii

Simulation + Hypothesis Testing for Model Checking of Probabilistic Systems (Abstract)

Axel Legay

Mahesh Viswanatha

pp. 3

PDF

Infinite-State Verification: From Transition Systems to Markov Chains (Abstract)

Parosh Aziz Abdulla

pp. 4

PDF

Analyzing Large Sparse Markov Chains of Kronecker Products (Abstract)

Tugrul Dayar

pp. 5

PDF

An Introduction to Monte Carlo Methods and Rare Event Simulation (Abstract)

Gerardo Rubino

Bruno Tuffin

pp. 6

PDF

Petri Net Analysis Using Decision Diagrams (Abstract)

Gianfranco Ciardo

pp. 7

PDF

Nondeterministic Labeled Markov Processes: Bisimulations and Logical Characterization (Abstract)

pp. 11-20

PDF

Quantitative Model Checking of Systems with Degradation (Abstract)

pp. 21-30

PDF

Simulation-Based CTMC Model Checking: An Empirical Evaluation (Abstract)

Joost-Pieter Katoen

Ivan S. Zapreev

pp. 31-40

PDF

On the Impact of Modelling Choices for Distributed Information Spread (Abstract)

Rena Bakhshi

Ansgar Fehnker

pp. 41-50

PDF

A Heuristic Approach for Fitting MAPs to Moments and Joint Moments (Abstract)

Peter Buchholz

Jan. Kriege

pp. 53-62

PDF

Acyclic Minimality by Construction---Almost (Abstract)

Reza Pulungan

Holger Hermanns

pp. 63-72

PDF

Faster Maximum Likelihood Estimation Algorithms for Markovian Arrival Processes (Abstract)

Hiroyuki Okamura

Tadashi Dohi

pp. 73-82

PDF

TimerMeter: Quantifying Properties of Software Timers for System Analysis (Abstract)

pp. 85-94

PDF

Modular Construction of Dependability Models from System Architecture Models: A Tool-Supported Approach (Abstract)

Melinda Magyar

István Majzik

pp. 95-96

PDF

A Performance Model of Zoned Disk Drives with I/O Request Reordering (Abstract)

Abigail S. Lebrecht

Nicholas J. Dingle

William J. Knottenbelt

pp. 97-106

PDF

Locating Performance Bottlenecks in Embedded Java Software with Calling-Context Cross-Profiling (Abstract)

pp. 107-108

PDF

Design Space Exploration for Java Processors with Cross-Profiling (Abstract)

pp. 109-118

PDF

COBAREA: The COpula-BAsed REliability and Availability Modeling Environment (Abstract)

pp. 119-120

PDF

Exploiting Restricted Transitions in Quasi-Birth-and-Death Processes (Abstract)

Juan F. Pérez

Benny Van Houdt

pp. 123-132

PDF

Time-Bounded Reachability in Tree-Structured QBDs by Abstraction (Abstract)

Daniel Klink

Anne Remke

Boudewijn R. Haverkort

Joost-Pieter Katoen

pp. 133-142

PDF

Comparison of Two Output Models for the BMAP/MAP/1 Departure Process (Abstract)

pp. 143-152

PDF

Aggregated Stochastic State Classes in Quantitative Evaluation of non-Markovian Stochastic Petri Nets (Abstract)

András Horvath

Enrico Vicario

pp. 155-164

PDF

The Ins and Outs of the Probabilistic Model Checker MRMC (Abstract)

pp. 167-176

PDF

Using Stochastic Comparison for Efficient Model Checking of Uncertain Markov Chains (Abstract)

Serge Haddad

Nihal Pekergin

pp. 177-186

PDF

A Modest Approach to Checking Probabilistic Timed Automata (Abstract)

Arnd Hartmanns

Holger Hermanns

pp. 187-196

PDF

[Publisher's information] (PDF)

pp. 314

Generation of Counterexamples for Model Checking of Markov Decision Processes (Abstract)

Husain Aljazzar

Stefan Leue

pp. 197-206

PDF

Remote Job Management in the Möbius Modeling Framework (Abstract)

pp. 209-210

PDF

FlowSim Simulation Benchmarking Platform (Abstract)

pp. 211-212

PDF

PerDaCol and PerfAnalysis - A Tool Set for Performance Measurement Data Collection and Evaluation of Real-Time Communication Systems (Abstract)

Antonius Erdmann

Dietmar Weber

pp. 213-214

PDF

Demultiplexing in Network Calculus- A Stochastic Scaling Approach (Abstract)

Jens B. Schmitt

Ivan Martinovic

pp. 217-226

PDF

The Multi-branched Method of Moments for Queueing Networks (Abstract)

Giuliano Casale

pp. 227-236

PDF

Quantifying the Trade-off Between the Level of Connectivity and Local Complexity in Random Wireless Network Topologies (Abstract)

András Faragó

pp. 237-246

PDF

Mean-Field Analysis for the Evaluation of Gossip Protocols (Abstract)

pp. 247-256

PDF

On the Detection of Symmetries in Compositional Markov Models (Abstract)

Ruth Lamprecht

Peter Kemper

pp. 259-268

PDF

Reachable State Space Generation for Structured Models which Use Functional Transitions (Abstract)

Afonso Sales

Brigitte Plateau

pp. 269-278

PDF

GTAexpress: A Software Package to Handle Kronecker Descriptors (Abstract)

pp. 281-282

PDF

Recent Extensions to Traviando (Abstract)

Peter Kemper

pp. 283-284

PDF

Integrating TPNs and Performance Bound Techniques in ITPN-PerfBound: A New Import Functionality (Abstract)

Elina Pacini Naumovich

Simona Bernardi

pp. 285-286

PDF

Language-Level Symmetry Reduction for Probabilistic Model Checking (Abstract)

Alastair F. Donaldson

Alice Miller

David Parker

pp. 289-298

PDF

Safety Analysis of an Airbag System Using Probabilistic FMEA and Probabilistic Counterexamples (Abstract)

Florian Leitner-Fischer

Stefan Leue

pp. 299-308

PDF

The Bio-PEPA Tool Suite (Abstract)

Federica Ciocchetta

Adam Duguid

Stephen Gilmore

Maria Luisa Guerriero

Jane Hillston

pp. 309-310

PDF

Author Index (PDF)

pp. 311-312