Information Technology Reference
In-Depth Information
incorporated via the
elapse
-operator. Symbolic (i. e. BDD-based) representations
and compositional methods are exploited to keep the model sizes manageable.
The complexity challenges posed by this problem domain could only be ad-
dressed by (1) performing a state space reduction on the non-deterministic part
of the model by means of a
symbolic
minimisation capable of handling huge state
spaces and (2) constraint-oriented specification of time-constraints
after
this re-
duction into the model. The developed technology was applied to a non-trivial
case study from the train control domain with an explication of the improve-
ments contributed by each of the relevant translation steps. In Figure 5 we quote
a fraction of the relevant information from [8], illustrating the effects and costs
of compositional minimisation.
Tracks -
Compositional Construction
Final Quotient IMC
Choices
States Transitions Time (sec.) States Transitions
1-1
71
261
18.70
16
55
1-2
79
325
22.58
29
101
1-3
99
419
26.87
39
143
1-4
119
513
30.43
49
185
2-1
731
3888
31.72
187
1006
2-2
1755
11059
39.55
665
3442
2-3
3127
20737
47.71
1281
6991
2-4
4899
33495
57.83
2097
11780
3-1
10075
75377
50.01
2573
18260
3-2
53858
387501
293.53
16602
112011
3-3
134555
1061958
1114.82
44880
320504
4-1
143641
1343747
785.30
35637
313270
4-2 1350908
11619969
243687.33 416274
3452502
Fig. 5.
Composition and minimisation statistics [8]
6 Concluding Remarks
This paper has presented an overview of foundational, algorithmic and pragmatic
aspects of IMCs, a simple generalisation of both CTMCs and LTS with a fully
compositional semantics. There are other approaches that give a compositional
semantics in a continuous time Markov setting, among them popular formalisms
such as PEPA [43], EMPA [6] or MTIPP [41], the latter being the semantic ba-
sis of the PRISM toolkit [44] in 'ctmc' mode. None of these formalisms has the
properties that IMCs possess. In particular, they do not extend classical concur-
rency models in a conservative fashion. For each of these calculi the role of an
atomic action is particular. This affects the synchronisation of actions, and thus
the final performance results - in different ways for each of these calculi. It is
not easy to explain what is happening precisely, and this is not the topic of this
paper; the interested reader may consult [17]. In IMC, the separation of delays
and actions allows to treat action synchronisation as in standard concurrency
