Stochastic Job Scheduling Problem
Introduction
This case studie is based on the stochastic job scheduling problem (sJSP) from [BDF81]. The modelation of the sJSP as IMC is based on the modelling as CTMDP in Model Checking Nondeterministic and Randomly Timed Systems. The figure below depicts a fragment of the IMC model induced by the (2,4,r) sJSP.
The example source of the model with the rates r1=0.25, r2=0.33, r3=1.25, and r4=1.5 can be found here: sJSP.imc
Model
| We construct the (2,4,r) sJSP with rates r1=0.25, r2=0.33, r3=1.25, and r4=1.5. |  |
Time-Bounded Reachability
We have computed the minimum and maximum time-bounded reachability probability for a time-bound z=14.
minimum | maximum | |
| time interval: | [0,14] | [0,14] |
| error bound: | 0.0001 | 0.0001 |
| time: | 3.61088 seconds | 3.606 seconds |
