Dear all,
It is possible, in MRMC, to verify several until properties of CTMCs. The general syntax is “phi U[low, high] psi”, where “low” and “high” may be real numbers. However, it should also be allowed that high = infinity. If low = 0, then one can write “phi U psi”, but what if low > 0? I propose that it becomes allowed to write “inf” or “infinity” in the position of high, similar to what is printed by printf("%g", HUGE_VAL);.
Example formula: P{<=0.1} [ tt U[10,infinity] crash ]
“The probability to crash no earlier than after 10 time units is at most 10%.”
Kind regards,
David N. Jansen.
