Information Technology Reference
In-Depth Information
models. It is surprising that given the advantages of IMCs, recent approaches
for CTMC-variants of process calculi for mobility and service-oriented comput-
ing [59] and interesting new developments in structured operational semantics
for such calculi [50,24] do not adopt this approach.
An extension of IMC towards time-inhomogeneous continuous-time dynamics
is provided in [33]. In the discrete time setting, a model class with similarly distin-
guishing properties is provided by probabilistic automata [60]. Probabilistic au-
tomata can be integrated into the IMC model, retaining full compositionality [26].
We have reviewed the theoretical basis of IMC, and have discussed two re-
cent algorithmic achievements that foster the applicability of IMC: analysis
techniques in the presence of nondeterminism, and compositional abstraction
techniques. IMCs practical relevance has been highlighted by reviewing in ap-
plications of various domains, ranging from dynamic fault trees to generalized
stochastic Petri nets. While the first generation of tool support, CADP, has
found several academic and non academic uses, the recent algorithmic advances
described in this paper are not yet fully integrated in a tool. This is a major
topic of ongoing work.
References
1. Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and sim-
ilarity for probabilistic processes. Journal of Computer and System Sciences 60,
187-231 (2000)
2. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algo-
rithms for continuous-time Markov chains. IEEE TSE 29, 524-541 (2003)
3. Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time
semantics for Markov chains. Information and Computation 200, 149-214 (2005)
4. Barendregt, H.: The quest for correctness. In: Images of SMC Research 1996. Sticht-
ing Mathematisch Centrum, pp. 39-58 (1996)
5. Bergstra, J.A., Ponse, A. (eds.): Handbook of Process Algebra. Elsevier Publishers
B.V, Amsterdam (2001)
6. Bernardo, M., Gorrieri, R.: Corrigendum to “A tutorial on EMPA: A theory of
concurrent processes with nondeterminism, priorities, probabilities and time. TCS
202 254, 1-54 (1998); Theoretical Computer Science 254, 691-694 (2001)
7. Bertsekas, D.: Dynamic Programming and Optimal Control, vol. II. Athena Scien-
tific, Belmont (1995)
8. Bode, E., Herbstritt, M., Hermanns, H., Johr, S., Peikenkamp, T., Pulungan, R.,
Rakow, J., Wimmer, R., Becker, B.: Compositional dependability evaluation for
STATEMATE. IEEE TSE 35, 274-292 (2009)
9. Boudali, H., Crouzen, P., Haverkort, B.R., Kuntz, M., Stoelinga, M.I.A.: Architec-
tural dependability evaluation with Arcade. In: Dependable Systems and Networks
(DSN), pp. 512-521. IEEE, Los Alamitos (2008)
10. Boudali, H., Crouzen, P., Stoelinga, M.: A compositional semantics for dynamic
fault trees in terms of interactive Markov chains. In: Namjoshi, K.S., Yoneda, T.,
Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 441-456.
Springer, Heidelberg (2007)
11. Boudali, H., Crouzen, P., Stoelinga, M.I.A.: Dynamic fault tree analysis using
input/output interactive Markov chains. In: Dependable Systems and Networks
(DSN). IEEE, Los Alamitos (2007)
