Hi Ana,
I am getting familiar with the MRMC tool and I would appreciate if somebody can provide a simple example on how to use the tool to get an optimal policy for a CTMDP given a specification in CSL. Any help will be very appreciated.
I have implemented (but not invented) the current algorithms for CTMDPs in the MRMC. Thus far, there is no way to extract the policy (or scheduler) leading to optimal reachability properties.
To see what I can do, there are some other things to be discussed: At first, in the official versions there is only an implementation of bounded-reachability (or, bounded until) properties but not steady-state (long-run average) or unbounded reachability (or unbounded until). Indeed, we have implemented algorithms for such properties in an unofficial version, hopefully to be integrated in the main branch at some point.
For bounded-reachability properties, the algorithms implemented in MRMC 1.5 and previous versions only maximise/minimise over the time-abstract, history-dependent policy (scheduler) class. Such a scheduler does know which states have been visited in the past and in which order. It does however not know any exact point of time, neither of when some state in the past was visited nor the current point of time. This scheduler class usually leads to the best bounds when considering CTMDPs resulting from abstractions of CTMCs. The algorithm for uniform CTMDPs is also very efficient, while the one to handle non-uniform CTMDPs is surely not.
In the current unofficial branch, there is an algorithm in which minimisation/maximisation is done over schedulers which do know the exact points of time, and which can also change the decision after having waited a while in a state without anything happened. This is the most powerful scheduler class for this property. The algorithm is however more costly than the one for the less-powerful scheduler class. It should be used in case you can assume that the instance resolving the nondeterminism does know exact time points.
Optimal schedulers for uniform CTMDPs over time-abstract, history dependent schedulers look like
w b^\omega ,
that is a finite prefix w of different decisions w = a1 a2 s3... an and then an infinite repetition of the same choice (choices may be different for each state, of course).
Optimal time-dependent schedulers for reachability are a finite collection of intervals
II = {{I1=[0,t1), I2=[t1,t2), ..., In=[tm-1,tm)}}
with tm=T, where T is a time bound and a function
f: II -> Decisions
mapping each interval to the decision to be chosen during this time.
For steady-state properties, optimal policies just need to map each state constantly to an optimal decision.
In case of nested properties, there is no single optimal scheduler for the whole formula, but only schedulers for the different subformulae.
In total, it depends very much on what property and scheduler class you want to consider. If you can give me more details in what you are planning, maybe I can probably provide some patch, though I'm not exactly sure when. In case you have further questions please ask.
Best regards, Moritz