 |
 |
Selected Papers of the "10th International Conference on Quantitative Evaluation of SysTems (QEST 2013)"
2013
Editor: Markus Siegle
This volume of Logical Methods in Computer Science contains five papers as extended versions of papers presented at the 10th International Conference on Quantitative Evaluation of Systems (QEST 2013). The conference took place in Buenos Aires, Argentina, in August 2013, and its proceedings were published as Springer Lecture Notes in Computer Science, vol. 8054.
After the conference, the authors of the most highly ranked papers were invited to submit an extended version of their work for a special issue of LMCS. In the sequel, a lot of extra work was invested in order to improve and augment the papers contained in this volume. While the themes of the articles collected here do not span the entire thematic range of QEST, they represent current hot topics of the research community.
We would like to cordially thank all authors for extending their conference papers and submitting them to this special issue. Special thanks goes to all reviewers who invested a lot of time and effort into this publication project. Their insightful comments were extremely valuable and helped to produce the final papers of excellent quality. Last but not least, we would also like to thank the team of LMCS for their help and support.
Kaustubh Joshi, Markus Siegle
QEST 2013 Guest Editors
QEST 2013 Guest Editors
1. Refinement and Difference for Probabilistic Automata
This paper studies a difference operator for stochastic systems whose specifications are represented by Abstract Probabilistic Automata (APAs). In the case refinement fails between two specifications, the target of this operator is to produce a specification APA that represents all witness PAs of this failure. Our contribution is an algorithm that allows to approximate the difference of two APAs with arbitrary precision. Our technique relies on new quantitative notions of distances between APAs used to assess convergence of the approximations, as well as on an in-depth inspection of the refinement relation for APAs. The procedure is effective and not more complex to implement than refinement checking.
2. Analysis of Timed and Long-Run Objectives for Markov Automata
Markov automata (MAs) extend labelled transition systems with random delays and probabilistic branching. Action-labelled transitions are instantaneous and yield a distribution over states, whereas timed transitions impose a random delay governed by an exponential distribution. MAs are thus a nondeterministic variation of continuous-time Markov chains. MAs are compositional and are used to provide a semantics for engineering frameworks such as (dynamic) fault trees, (generalised) stochastic Petri nets, and the Architecture Analysis & Design Language (AADL). This paper considers the quantitative analysis of MAs. We consider three objectives: expected time, long-run average, and timed (interval) reachability. Expected time objectives focus on determining the minimal (or maximal) expected time to reach a set of states. Long-run objectives determine the fraction of time to be in a set of states when considering an infinite time horizon. Timed reachability objectives are about computing the probability to reach a set of states within a given time interval. This paper presents the foundations and details of the algorithms and their correctness proofs. We report on several case studies conducted using a prototypical tool implementation of the algorithms, driven by the MAPA modelling language for efficiently generating MAs.
3. Stochastic Parity Games on Lossy Channel Systems
We give an algorithm for solving stochastic parity games with almost-sure winning conditions on {\it lossy channel systems}, under the constraint that both players are restricted to finite-memory strategies. First, we describe a general framework, where we consider the class of 2 1/2-player games with almost-sure parity winning conditions on possibly infinite game graphs, assuming that the game contains a {\it finite attractor}. An attractor is a set of states (not necessarily absorbing) that is almost surely re-visited regardless of the players' decisions. We present a scheme that characterizes the set of winning states for each player. Then, we instantiate this scheme to obtain an algorithm for {\it stochastic game lossy channel systems}.
4. High-level Counterexamples for Probabilistic Automata
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of the system's states, both of which are of limited use in manual debugging. Many probabilistic systems are described in a guarded command language like the one used by the popular model checker PRISM. In this paper we describe how a smallest possible subset of the commands can be identified which together make the system erroneous. We additionally show how the selected commands can be further simplified to obtain a well-understandable counterexample.
5. Learning and Designing Stochastic Processes from Logical Constraints
Stochastic processes offer a flexible mathematical formalism to model and reason about systems. Most analysis tools, however, start from the premises that models are fully specified, so that any parameters controlling the system's dynamics must be known exactly. As this is seldom the case, many methods have been devised over the last decade to infer (learn) such parameters from observations of the state of the system. In this paper, we depart from this approach by assuming that our observations are {\it qualitative} properties encoded as satisfaction of linear temporal logic formulae, as opposed to quantitative observations of the state of the system. An important feature of this approach is that it unifies naturally the system identification and the system design problems, where the properties, instead of observations, represent requirements to be satisfied. We develop a principled statistical estimation procedure based on maximising the likelihood of the system's parameters, using recent ideas from statistical machine learning. We demonstrate the efficacy and broad applicability of our method on a range of simple but non-trivial examples, including rumour spreading in social networks and hybrid models of gene regulation.