[Publisher's information] (PDF)

pp. 326

[Copyright notice] (PDF)

pp. iv

Steering Committee (PDF)

pp. xv

Table of contents (PDF)

pp. v-viii

[Front cover] (PDF)

pp. C1

Technical Program Committee (PDF)

pp. xiv

Title Page i (PDF)

pp. i

Title Page iii (PDF)

pp. iii

Message from General Chair (PDF)

pp. ix-x

Message from Program Chairs (PDF)

pp. xi-xii

Organizing Committee (PDF)

pp. xiii

Autonomous Model Learning for Reinforcement Learning (Abstract)

Michael Littman

pp. 3

PDF

A Control-Theoretic Modeling Approach for Service Differentiation in Multi-hop Ad-hoc Networks (Abstract)

Yimeng Yang

Boudewijn R. Haverkort

Geert J. Heijenk

pp. 7-16

PDF

On the Data Delivery Delay taken by Random Walks in Wireless Sensor Networks (Abstract)

pp. 17-26

PDF

Analysis of an M/G/1 Queue with Repeated Inhomogeneous Vacations with Application to IEEE 802.16e Power Saving Mechanism (Abstract)

pp. 27-36

PDF

CaVi -- Simulation and Model Checking for Wireless Sensor Networks (Abstract)

pp. 37-38

PDF

Performance Model Generation for MPSoC Design-Space Exploration (Abstract)

B.D. Theelen

pp. 39-40

PDF

M?bius Trace Analysis with Traviando (Abstract)

Ruth Lamprecht

Peter Kemper

pp. 41-42

PDF

Reduction Techniques for Model Checking Markov Decision Processes (Abstract)

pp. 45-54

PDF

Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics (Abstract)

pp. 55-64

PDF

Symbolic Partition Refinement with Dynamic Balancing of Time and Space (Abstract)

pp. 65-74

PDF

Cell Assisted APMC (Abstract)

pp. 75-76

PDF

ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems (Abstract)

pp. 77-78

PDF

Prism2Promela (Abstract)

Christopher Power

Alice Miller

pp. 79-80

PDF

KPC-Toolbox: Simple Yet Effective Trace Fitting Using Markovian Arrival Processes (Abstract)

pp. 83-92

PDF

VATS: Virtualized-Aware Automated Test Service (Abstract)

pp. 93-102

PDF

Symbolic Magnifying Lens Abstraction in Markov Decision Processes (Abstract)

pp. 103-112

PDF

Recent Extensions to the Stochastic Process Algebra Tool CASPA (Abstract)

pp. 113-114

PDF

A Tool Supporting Evaluation of Non-markovian Fault Trees (Abstract)

pp. 115-116

PDF

The Performability Tool P'ility (Abstract)

Lucia Cloth

Boudewijn R. Haverkort

pp. 117-118

PDF

Composing Web Services in an Open World: QoS Issues (Abstract)

Albert Benveniste

pp. 121

PDF

A Joint Moments Based Analysis of Networks of MAP/MAP/1 Queues (Abstract)

pp. 125-134

PDF

Product Form Approximations for Communicating Markov Processes (Abstract)

Peter Buchholz

pp. 135-144

PDF

Discrete Time Markov Chains Competing over Resources: Product Form Steady-State Distribution (Abstract)

Jean-Michel Fourneau

pp. 147-156

PDF

Memory Efficient Calculation of Path Probabilities in Large Structured Markov Chains (Abstract)

Paolo Ballarini

Andr? Horv?th

pp. 157-166

PDF

Hintikka Games for PCTL on Labeled Markov Chains (Abstract)

pp. 169-178

PDF

Regular Expressions for PCTL Counterexamples (Abstract)

pp. 179-188

PDF

Debugging of Dependability Models Using Interactive Visualization of Counterexamples (Abstract)

Husain Aljazzar

Stefan Leue

pp. 189-198

PDF

Linear Programming, Lyapunov Functions, and Performance Analysis (Abstract)

Peter Glynn

pp. 201

PDF

Automatic Translation of UML Sequence Diagrams into PEPA Models (Abstract)

Mirco Tribastone

Stephen Gilmore

pp. 205-214

PDF

Analysis of Large Scale Interacting Systems by Mean Field Method (Abstract)

pp. 215-224

PDF

Polynomial Throughput Bounds for Equal Conflict Petri Nets with Multi-guarded Transitions (Abstract)

Jorge J?lvez

pp. 225-234

PDF

New Solvers for Asymmetric Systems in GreatSPN (Abstract)

Souheib Baarir

Marco Beccuti

Giuliana Franceschinis

pp. 235-236

PDF

A Parallel and Distributed Analysis Pipeline for Performance Tree Evaluation (Abstract)

Darren K. Brien

Nicholas J. Dingle

William J. Knottenbelt

Harini Kulatunga

Tamas Suto

pp. 237-238

PDF

An Experimental Framework for PIPE2 (Abstract)

pp. 239-240

PDF

Quasi-Birth-Death Processes, Tree-Like QBDs, Probabilistic 1-Counter Automata, and Pushdown Systems (Abstract)

pp. 243-253

PDF

Computing Expected Absorption Times for Parametric Determinate Probabilistic Timed Automata (Abstract)

pp. 254-263

PDF

Approximate Analysis of Probabilistic Processes: Logic, Simulation and Games (Abstract)

pp. 264-273

PDF

Conflict-Tolerant Real-Time Features (Abstract)

Deepak D'Souza

Madhu Gopinathan

S. Ramesh

Prahladavaradan Sampath

pp. 274-283

PDF

Cross-Profiling for Embedded Java Processors (Abstract)

pp. 287-296

PDF

Characterization of the E-commerce Storage Subsystem Workload (Abstract)

pp. 297-306

PDF

Modeling Peer-to-Peer Botnets (Abstract)

Elizabeth Van Ruitenbeek

William H. Sanders

pp. 307-316

PDF

Perfect Generation, Monotonicity and Finite Queueing Networks (Abstract)

Jean-Marc Vincent

pp. 319

PDF

Randomness in Wireless Networks: How to Deal with It (Abstract)

Merouane Debbah

pp. 320

PDF

Correctness Verification and Quantitative Evaluation of Timed Systems Based on Stochastic State Classes (Abstract)

Enrico Vicario

pp. 321

PDF

Model Checking and Decision Procedures for Probabilistic Automata and Markov Chains (Abstract)

James Worrell

pp. 322

PDF

Author Index (PDF)

pp. 323-324