Published: 11th June 2013
DOI: 10.4204/EPTCS.117
ISSN: 2075-2180

EPTCS 117

Proceedings 11th International Workshop on
Quantitative Aspects of Programming Languages and Systems
Rome, 23rd-24th March 2013

Edited by: Luca Bortolussi and Herbert Wiklicky

Preface
Preserving differential privacy under finite-precision semantics.
Ivan Gazeau, Dale Miller and Catuscia Palamidessi
1
Indexed Labels for Loop Iteration Dependent Costs
Paolo Tranquilli
19
Quantitative Security Analysis for Multi-threaded Programs
Tri Minh Ngo and Marieke Huisman
34
Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance
Viktor Schuppan
49
Modal Specifications for Probabilistic Timed Systems
Tingting Han, Christian Krause, Marta Kwiatkowska and Holger Giese
66
The Spectrum of Strong Behavioral Equivalences for Nondeterministic and Probabilistic Processes
Marco Bernardo, Rocco De Nicola and Michele Loreti
81
Probabilistic Concurrent Kleene Algebra
Annabelle McIver, Tahiry Rabehaja and Georg Struth
97
Solving Stochastic Büchi Games on Infinite Arenas with a Finite Attractor
Nathalie Bertrand and Philippe Schnoebelen
116
The Complexity of Robot Games on the Integer Line
Arjun Arul and Julien Reichert
132

Preface

This volume contains the proceedings of the Eleventh Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013), held in Rome, Italy, on 23 and 24 March, 2013. QAPL 2013 was a satellite event of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013).

The central theme of the workshop is that of quantitative aspects of computation. These aspects are related to the use of physical quantities (storage space, time, bandwidth, etc.) as well as mathematical quantities (e.g. probability and measures for reliability, security and trust), and play an important (sometimes essential) role in characterising the behaviour and determining the properties of systems. Such quantities are central to the definition of both the model of systems (architecture, language design, semantics) and the methodologies and tools for the analysis and verification of the systems properties. The aim of this workshop is to discuss the explicit use of quantitative information such as time and probabilities either directly in the model or as a tool for the analysis of systems. In particular, the workshop focuses on:

The history of QAPL starts in 2001, when its first edition was held in Florence, Italy, as a satellite event of the ACM Principles, Logics, and Implementations of high-level programming languages, PLI 2001. The second edition, QAPL 2004, was held in Barcelona, Spain, as a satellite event of ETAPS 2004. Since then, QAPL has become a yearly appointment with ETAPS. In the following years, QAPL was held in Edinburgh, Scotland (QAPL 2005), Vienna, Austria (QAPL 2006), Braga, Portugal (QAPL 2007), Budapest, Hungary (QAPL 2008), York, UK (QAPL 2009), Paphos, Cyprus (QAPL 2010), Saarbru _cken, Germany (QAPL 2011) and Tallinn, Estonia (QAPL 2012).
The proceedings of the workshops upto and including 2009 are published as volumes in Electronic Notes in Theoretical Computer Science (ENTCS). The editions of 2010, 2011 and 2012 are published as volume 28, volume 57, and volume 85, respectively, of the Electronic Proceedings in Theoretical Computer Science (EPTCS).
Three special issues of the journal of Theoretical Computer Science are dedicated to the QAPL 2004, QAPL 2006 and QAPL 2010 events, and are published in Volume 346(1), Volume 382(1) and Volume 413(1) respectively. A special issue of the journal of Theoretical Computer Science dedicated to QAPL 2011 and QAPL 2012 is in preparation.

The workshop programme included two QAPL keynote presentations: Alessandra Di Pierro (University of Verona, Italy): Probabilistic static analysis and security trade-offs, and Paolo Zuliani (University of Newcastle, UK): Statistical Model Checking for Cyber-Physical Systems as well as two keynotes shared with MLQA: Martin Franzle (University of Oldenburg, Germany): A tight integration of symbolic, numeric, and statistical methods for the analysis of cyber-physical systems, and Flemming Nielson (Technical University of Denmark): Guarding against Denial of Service Attacks.

Furthermore, the Program Committee of QAPL 2013 which comprised of:

selected 9 regular papers and 3 presentation-only papers. All regular papers were reviewed by at least three reviewers. After the workshop, the authors of regular papers were asked to submit a revised version, incorporating the comments made during the discussion at the workshop, which are included here.

We would like to thank the QAPL steering committee for its support, the ETAPS 2013 organisers and furthermore all the authors, the invited speakers, the programme committee and the external referees for their valuable contributions.

May 2013

Luca Bortolussi and Herbert Wiklicky
Program Co-chairs