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.
Hallo David,
Great idea! I would keep the name short, just "inf".
Best regards,
Ivan
On Tue, May 21, 2013 at 5:37 PM, David N. Jansen dnjansen@cs.ru.nl wrote:
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. _______________________________________________ MRMC-users mailing list MRMC-users@lists.rwth-aachen.de https://mailman.rwth-aachen.de/mailman/listinfo/mrmc-users
mrmc-users@lists.rwth-aachen.de
-
David N. Jansen -
Ivan Zapreev