|
Published: 26th October 2010 DOI: 10.4204/EPTCS.38 ISSN: 2075-2180 |
This volume contains the proceedings of the 3rd Interaction and Concurrency Experience (ICE 2010) workshop, which was held in Amsterdam, Netherlands on 10th of June 2010 as a satellite event of DisCoTec'10.
The experimental aspect of the ICE workshop series consists of two aspects: firstly, each year, the workshop focuses on a different topic related to interactions in concurrent systems and, secondly, it features a novel review and selection procedure.
The previous editions of ICE were affiliated to ICALP 2008 (Reykjavik, Iceland) and CONCUR 2009 (Bologna, Italy), with focus on Synchronous and Asynchronous Interactions and on Structured Interactions respectively. The topic of ICE 2010 was Guaranteed Interactions, by which we mean, for example, guaranteeing safety, reactivity, quality of service or satisfaction of analysis hypotheses. In order to provide such guarantees, a number of directions are being explored to develop appropriate models, methodologies and tools, like, for instance, behavioural types, component-based model checking, assume-guarantee and, recently, "by construction" techniques such as glue synthesis. Considering interaction as a first class entity is crucial for overcoming complexity issues of distributed systems, such as state space explosion. In this context, coordination can be viewed as imposing constraints on the interaction among the actors. Such constraints and guarantees of their satisfaction play an important role in the analysis of distributed systems.
ICE innovative paper selection mechanism is based on an interactive discussion amongst authors and PC members. During the review phase, each submitted paper is published on a Wiki and associated with a discussion forum whose access is restricted to the authors and to all the PC members not in conflict of interests. The PC members post comments and questions that the authors reply to. As at the past two editions, the forum discussion during the review and selection phase of ICE 2010 has considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and stimulated the discussion during the workshop.
The interactive selection procedure implies additional effort for both authors and PC members. However, as any scientific debate, this effort mainly consists in formulating and writing down arguments supporting or criticising the ideas advanced in the papers under review. The effort and time spent in the forum interaction is rewarding for both authors—when updating their papers—and reviewers—when writing their reviews: the forum discussion helps to discover and correct typos in key definitions and mispelled statements, to improve examples and presentation of critical cases, to confute reviewers counterexamples and solve any misunderstanding at the very early stage of the review process.
Each full paper was reviewed by four PC members, and altogether 6 full papers (out of 9) and 3 short papers (out of 4) were accepted for publication in the ICE 2010. Final versions of these papers, taking into account both the comments of the PC members and the discussion at the workshop, are included in this volume together with the abstracts of the two invited talks by Thomas A. Henzinger and Joost-Pieter Katoen. The accepted contributions are included in the same order as they were presented at the workshop.
We would like to thank the authors of all the submitted papers for their interest in the workshop, the PC members for their efforts, and the workshop participants for active participation in the discussion, all of which together have provided for the success of the ICE workshop. We thank Thomas A. Henzinger and Joost-Pieter Katoen for accepting our invitations to present their recent work, and the DisCoTec'10 organisers—particularly the workshop chair Marcello Bonsangue—for providing an excellent environment for the preparation and staging of the event. We are grateful to the EPTCS editors for the publication of these proceedings and to the sponsors of the event, namely CEA LIST, ArtistDesign network of excellence and Institute for Programming research and Algorithmics who made it possible to waive many costs from the registration fees and to offer travel grants to students.
Simon Bliudze – CEA LIST (France)
Roberto Bruni – University of Pisa (Italy)
Davide Grohmann – University of Udine (Italy)
Alexandra Silva – CWI (The Netherlands)
The traditional view holds that there is a boolean satisfaction or refinement relation between system implementations and system specifications. Reactive models have been extended to accommodate certain numerical quantities, such as transition times and probabilities. However, the boolean view is still prevalent, for example, in checking whether a timed automaton satisfies a formula of a real-time logic, or whether a stochastic process satisfies a formula of a probabilistic logic. We advocate the fully quantitative view, where a specification can be satisfied to different degrees, that is, the value of a given specification over a given implementation is a real number rather than a boolean. We survey some results in this direction and present some potential applications, not only in the timed and probabilistic domains, but also for specifying and analyzing the resource use, cost, performance, robustness, and reliability of a system.
We consider a continuous-time stochastic model —called interactive Markov chains (IMCs)— which allows interaction and concurrency in a process-algebraic fashion. We discuss notions of strong and weak (bi)simulation and their congruence properties. We show how simulation pre-congruences provide the basis for compositional abstraction where abstract models are a mixture of interval IMCs and modal transition systems. A key problem in model checking IMCs, in fact stochastic real-time games, is computing maximal time-bounded reachability probabilities. We show a greedy approach to determine optimal time-abstract policies, and a discretisation approach to determine optimal timed (measurable) policies, and report on some practical results. Finally, we show that IMCs are the semantical backbone for higher-level formalisms from various domains such as generalized stochastic Petri nets (GSPNs) used in performance evaluation, dynamic fault trees (DFTs) used in reliability and safety engineering, and the standardised architectural description language AADL, as used in hardware/software co-design.
This talk focuses on a simple combination of continuous-time Markov chains (CTMCs) and labeled transition systems (LTSs). CTMCs are perhaps the most well-studied stochastic model in performance evaluation, are at the heart of dependability analysis, and naturally reflect the random real-time behaviour of stoichiometric equations in systems biology. LTSs are one of the main operational models for concurrency and are equipped with a rich plethora of behavioural equivalences like bisimulation and trace equivalences. CTMCs + LTSs yield so-called interactive Markov chains (IMCs), originally proposed by Hermanns [10] as semantical model of stochastic process algebras. In this talk, we reflect on more than a decade of research on IMCs by various researchers. The main issues we will address are:
IMC theory. We survey the main results on weak and strong bisimulation on IMCs that go back to the initial work by Hermanns and co-workers, and summarize their congruence results with respect to two operations: CSP-like parallel composition and hiding [10]. We’ll show that parallel composition allows for the constraint-oriented specification [18] of random timing behaviour, i.e., existing LTSs can be extended with random timing in a fully compositional manner [12]. Bisimulation minimisation can be performed by a small twist of Paige and Tarjan’s seminal partition-refinement minimisation algorithm. That is to say, the coarsest bisimulation quotient can be determined in a worst-case time complexity that is linear in the number of transitions and logarithmically in the number of states. The congruence results allow for compositional minimisation, i.e., IMCs can be minimised prior to putting them in parallel with other components (i.e., other IMCs) [10, 12]. This drastically reduces peak memory consumption.
IMCs analysis. Determining qualitative properties of IMCs, such as universal or existential reachability can be done in a standard way, as if IMCs were Kripke structures. To determine reachability probabilities, such as the minimal or maximal probability to eventually reach a set of goal states —without imposing a time bound— it suffices to consider the “embedded” discrete probabilistic process of an IMC. This is an interactive probabilistic chain (IPC), which is akin to a Markov decision process. Computing reachability probabilities can be performed using MDP techniques such as value iteration or policy iteration. Determining time-bounded reachability probabilities is much harder. Optimal time-abstract policies, policies that cannot decide on the basis of the timings in a history, can be computed using a polynomial-time greedy algorithm [1]. This however only applies to uniform IMCs, IMCs in which the residence time in each state is governed by the same negative exponential distribution. Recently, Brázdil et al. provided an exponential-time algorithm that is generally applicable [6]. Determining timed policies (which can improve time-abstract ones) is more sophisticated. A discretisation approach can be used to compute ε-optimal timed policies for maximising time-bounded reachability probabilities [19]. Experimental data shows the current state of practice of this technique.
IMC abstraction. Bisimulation minimisation can be considered as a fully automated abstraction technique. Thanks to the fact that bisimulation preserves (time-bounded) reachability probabilities, prior to any such analysis, IMCs can be minimised. As this is not an on-the-fly technique, this requires the generation of the entire state space which is certainly a serious bottleneck. As a next step, we therefore consider three-valued abstraction of IMCs. The main idea is to partition the (potentially infinite) state space such that finitely many partitions result. Each partition is represented by a single state. As transition probabilities may differ, probability intervals are used to label transitions [14]. Secondly, in order to deal with the absence or presence of transitions between concrete states, we use may and must transitions as in modal transition systems [16]. As non-equivalent states may be grouped, we resort to a three-valued semantics. It will be shown that abstract IMCs simulate concrete IMCs, and that thanks to the fact that simulation is a pre-congruence, abstraction can be done in a compositional manner [15]. As simulation preserves lower bounds on (time-bounded) probabilistic reachability properties, this abstraction technique is conservative for such properties, but not for long-run averages. In case several IMCs can be abstracted by the same abstract model, symmetric parallel composition can be used in addition to obtain even smaller equivalent models.
IMC as semantical model. The simplicity of IMCs and their compositional nature make them attractive to act as semantical backbone of several formalisms. One may even argue the other way around: many formalisms are in fact high-level specification languages for IMCs. This is true for stochastic process algebras [5, 11]. But this comes as no surprise, as IMCs were developed for that purpose. It also applies to dynamic fault trees [8]. This extension of static fault trees is used in reliability engineering for safety analysis purposes and specifies the causal relationship between failure occurrences. If failures occur according to an exponential distribution —quite a common assumption in reliability analysis— dynamic fault trees are in fact IMCs [3]. This is not an exception. Generalised stochastic Petri nets (GSPNs) [17], one of the most common modeling formalisms in performance analysis, are in fact IMCs [13]. The same applies to the standardised Architectural Analysis and Design Language (AADL) [9] in which nominal behaviour is extended with error modeling. IMCs are a natural semantical model for AADL [4]. Other examples are stochastic extensions of Statecharts [2], and hardware descriptions (for a discrete version of IMCs [7]).
The baseline of my talk will be: IMCs are much more useful and beautiful than you think!
[1] C. Baier, H. Hermanns, J.-P. Katoen, and B. R. Haverkort Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comp. Sc., vol. 345(1) (2005) 2–26.
[2] Boede, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R., Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for STATEMATE. IEEE Trans. on Software Engineering 35 (2009) 274–292
[3] Boudali, H., Crouzen, P., Stoelinga, M. I. A.: Rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. on Secure and Dependable Computing 7(2) (2009) 128–143.
[4] Bozzano, M., Cimatti, A., Katoen, J.-P., Nguyen, V., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. The Computer Journal (2010).
[5] Bravetti, M., Hermanns, H., Katoen, J.-P.: YMCA: Why Markov chain algebra? In: Electronic Notes in Theoretical Computer Science, Vol. 162. (2006) 107–112.
[6] Brázdil, T., Forejt, V., Krcal, J., Kretinsky, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. In: Found. of Softw. Technology and Theor. Comp. Sc. (FSTTCS). LIPIcs 4. (2009) 61–72.
[7] Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Computer Aided Verification (CAV). LNCS Vol. 5643. (2009) 204– 218
[8] Dugan, J., Bavuso, S., Boyd, M.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. on Reliability 41 (1992) 363–77
[9] Feiler, P. H., Rugina, A.: Dependability modeling with the Architecture Analysis & Design Language (AADL). Technical Note CMU/SEI-2007-TN-043, CMU Software Engineering Institute (2007)
[10] Hermanns, H.: Interactive Markov Chains: the Quest for Quantified Quality. LNCS, Vol. 2428. Springer (2002)
[11] Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comp. Sc. 274 (2002) 43–87
[12] Hermanns, H., Katoen, J.-P.: Automated compositional Markov chain generation for a plain-old telephone system. Science of Comp. Progr. 36 (2000) 97–127
[13] Hermanns, H., Katoen, J.-P., Neuhaeußer, M. R., Zhang, L.: GSPN model checking despite confusion. Technical report, RWTH Aachen University (2010)
[14] Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Computer Aided Verification (CAV). LNCS, Vol. 4590. (2007)
[15] Katoen, J.-P., Klink, D., Neuhaeußer, M. R.: Compositional abstraction for stochastic systems. In: Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, Vol. 5813. (2009) 195–211
[16] Larsen, K. G.: Modal specifications. In: Automatic Verification Methods for Finite State Systems. LNCS, Vol. 407. (1989) 232–246
[17] Marsan, M. A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. John Wiley & Sons (1995)
[18] Vissers, C., Scollo, G., van Sinderen, M., Brinksma, E.: On the use of specification styles in the design of distributed systems. Theor. Comp. Sci. 89 (1991) 179–206
[19] Zhang, L., Neuhaeußer, M. R.: Model checking interactive Markov chains. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS Vol. 6015. (2010) 53–68.