This document describes command line options and interface commands of the Markov Reward Model Checker (below referenced as MRMC) version 1.1 beta. ----------------------------------------------------------------- Contents ----------------------------------------------------------------- 0. General information 1. Command line options 1.1 An example of .tra file 1.2 An example of .lab file 1.3 An example of .rew file 1.4 An example of .rewi file 2. Interface commands 2.1 PCTL logic formulas 2.2 PRCTL logic formulas 2.3 CSL logic formulas 2.4 PRCTL logic formulas ----------------------------------------------------------------- 0. General information ----------------------------------------------------------------- MRMC is a command-line model checker for discrete-time and continuous-time Markov reward models implemented in C. It supports reward extensions of PCTL and CSL (PRCTL and CSRL), and allows for the automated verification of properties concerning long-run and instantaneous rewards as well as cumulative rewards. In particular, it supports to check the reachability of a set of goal states (by only visiting legal states before) under a time and an accumulated reward constraint. MRMC has an interactive interface i.e. a command line. First in section "1. Command line options" we will explain how to start MRMC and then in section "2. Interface commands" we will talk about how to interact with MRMC. ----------------------------------------------------------------- 1. Command line options ----------------------------------------------------------------- Starting MRMC without parameters will give the following output: Usage: mrmc <.tra file> <.lab file> <.rew file> <.rewi file> - could be one of {csl, pctl, prctl, csrl}. <.tra file> - is the file with the matrix of transitions. <.lab file> - contains labeling. <.rew file> - contains state rewards (for PRCTL/CSRL). <.rewi file> - contains impulse rewards (for CSRL, optional). Note: In the '.tra' file transitions should be ordered by rows and columns! The format of the .tra and .lab file is similar to format of ETMCC. Note that state indexes start from 1. ----------------------------------------------------------------- 1.1 An example of .tra file ----------------------------------------------------------------- Contains the matrix with rates of probabilities: STATES 5 TRANSITIONS 11 1 2 0.0004 1 5 0.0001 2 1 0.05 2 3 0.0004 2 5 0.0001 3 2 0.05 3 4 0.0004 3 5 0.0001 4 3 0.05 4 5 0.0001 5 1 0.06 The header defines the number of states and transitions in the system. The rest are transitions in the format: Note that transitions are (and should be) ordered by row and column index! ----------------------------------------------------------------- 1.2 An example of .lab file ----------------------------------------------------------------- Contains labeling states with atomic propositions: # DECLARATION Thup Twup Onup Zeup Sup vdown failed #END 1 Thup Sup 2 Twup Sup 3 Onup failed 4 Zeup failed 5 vdown failed Here in the header section we define all atomic propositions (labels), such as "Thup" and "Twup". Then atomic propositions are assigned to states in the format: Note that we allow quite complicated names for atomic propostions, such as: p1+p0<=p2+p3 To be more precise a state label (any atomic propostion) should fit the following regular expression: "{let}{alnum}*" where let [_a-zA-Z] alnum [_a-zA-Z0-9<>_^*+-=] For more detailes see MRMC/parser/la_etmcc2.l ----------------------------------------------------------------- 1.3 An example of .rew file ----------------------------------------------------------------- Defines state rewards: 1 8 2 9 3 10 4 11 5 13 This is just a list of the form: ----------------------------------------------------------------- 1.4 An example of .rewi file ----------------------------------------------------------------- Defines state impulse rewards: TRANSITIONS 11 1 2 3 1 5 3 2 1 1 2 3 3 2 5 3 3 2 1 3 4 3 3 5 3 4 3 1 4 5 3 5 1 5 In the header we define the number of transitions, then assign rewards to transitions in the format: ----------------------------------------------------------------- 2. Interface commands ----------------------------------------------------------------- After MRMC is on and running you may start interacting with it using commands. The first one you should learn is: help which provides you with the output like the following: help - display this help quit - exit the program print - print parameters ssd_on - Turn on the steady-state detection in uniformization of bounded untill, for CSL logic ssd_off - Turn off the steady-state detection in uniformization of bounded untill, for CSL logic set * - Where * is one of the following: error_bound R - Error Bound for all methods. max_iter I - Number of Max Iterations for all methods. overflow R - Overflow for the Fox-Glynn algorithm. underflow R - Underflow for the Fox-Glynn algorithm. method_path M - Method for path formulas. method_steady M - Method for steady state formulas. method_until_rewards MU - Method for time-reward-bounded until formula. w R - The probability threshold for uniformization Qureshi-Sanders d R - The discretization factor for state rewards Here: I is a natural number. R is a real value. M is one of {gauss_jacobi,gauss_seidel}. MU is one of {uniformization_sericola, uniformization_qureshi_sanders, discretization_tijms_veldman}. All commands are quite clear, but there are some important notes, which we should make: 1. "set error_bound R" - sets error bound for the analysis, for example it defines the overall error for the time-bounded reachability of CSL logic (such as property P{>0.1}[ Sup U[0,50] failed]). 2. "set method_path M" - currently supports only M=gauss_jacobi 3. "set method_until_rewards uniformization_sericola" - is currently unsupported 4. "ssd_on" - turnes on precize on-the-fly steady-state detection for the time-bounded reachability of CSL logic 5. "print" - allowes to check the runtime values of error bound, default methods set for the analysis, etc. ----------------------------------------------------------------- 2.1 PCTL logic formulas ----------------------------------------------------------------- Here is the E-BNF notation for the PCTL logic formulas accepted by MRMC: PCTL logic formulas: CONST = ff | tt R = 'real number' OP = > | < | <= | >= SFL = CONST | LABEL | ! SFL | SFL && SFL | SFL || SFL | ( SFL ) | L{ OP R }[ SFL ] | P{ OP R }[ PFL ] PFL = X SFL | SFL U SFL | SFL U[ R, R ] SFL Here are some details: tt - atomic proposition TRUE ff - atomic proposition FALSE SFL - is state formula PFL - is path formula X SFL - Next operator SFL U SFL - Unbounded until operator SFL U[ R, R ] SFL - Time bounded until operator L{ OP R }[ SFL ] - Long-run operator, the probability bound for being in SFL states in the long run. P{ OP R }[ PFL ] - Checks the probability bound for any path formula. ----------------------------------------------------------------- 2.2 PRCTL logic formulas ----------------------------------------------------------------- Here is the E-BNF notation for the PRCTL logic formulas accepted by MRMC: PRCTL logic formulas: CONST = ff | tt R = 'real number' OP = > | < | <= | >= SFL = CONST | LABEL | ! SFL | SFL && SFL | SFL || SFL | ( SFL ) | E [ R, R] [ SFL ] | E [n][ R, R] [ SFL ] | C [n][ R, R] [ SFL ] | Y [n][ R, R] [ SFL ] | L{ OP R }[ SFL ] | P{ OP R }[ PFL ] PFL = X SFL | SFL U SFL | SFL U[ R, R ][ R, R ] SFL | SFL U[ R, R ] SFL Here are some details "2.1 PCTL logic formulas" and below: E [ R, R] SFL - the long-run expected reward rate per time-unit for SFL-states meets the bounds [ R, R] E [n][ R, R] SFL - asserts that the expected reward rate in SFL-states up to n transitions is within the interval [ R, R] C [n][ R, R] SFL - asserts that the instantaneous reward in SFL-states at the n'th epoch meets the bounds of [ R, R] Y [n][ R, R] SFL - asserts that the expected accumulated reward in SFL-states until the n'th transition meets the bounds of [ R, R] SFL U[ R, R ][ R, R ] SFL - Bounded until operator with time and reward bound, first [R, R] defines time bounds, second [R, R] defines reward bound For details on PRCTL see: 1. S. Andova, H. Hermanns, and J.-P. Katoen. Discrete-time rewards model-checked. In Formal Modeling and Analysis of Timed Systems (FORMATS 2003), Marseille, France, 2003. Lecture Notes in Computer Science, Springer-Verlag. ----------------------------------------------------------------- 2.3 CSL logic formulas ----------------------------------------------------------------- Here is the E-BNF notation for the CSL logic formulas accepted by MRMC: CSL logic formulas: CONST = ff | tt R = 'real number' OP = > | < | <= | >= SFL = CONST | LABEL | ! SFL | SFL && SFL | SFL || SFL | ( SFL ) | S{ OP R }[ SFL ] | P{ OP R }[ PFL ] PFL = X SFL | X[ R, R ] SFL | SFL U SFL | SFL U[ R, R ] SFL This is similar to PCTL logic, but just remember that we work with CTMCs, and thus: 1. Instead of the Long-run operator L{ OP R }[ SFL ] we have a steady-state operator S{ OP R }[ SFL ] 2. There is a time bounded Next operator X[ R, R ] SFL For details on CSL see: 1. C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-checking algorithms for continuous-time Markov Chains. IEEE Transactions on Software Engineering, 29(7), 2003. ----------------------------------------------------------------- 2.4 CSRL logic formulas ----------------------------------------------------------------- Here is the E-BNF notation for the CSRL logic formulas accepted by MRMC: CSRL logic formulas: CONST = ff | tt R = 'real number' OP = > | < | <= | >= SFL = CONST | LABEL | ! SFL | SFL && SFL | SFL || SFL | ( SFL ) | S{ OP R }[ SFL ] | P{ OP R }[ PFL ] PFL = X SFL | X [R, R] SFL | X [R, R][R, R] SFL | SFL U SFL | SFL U[ R, R ] SFL | SFL U[ R, R ] [ R, R ] SFL Here are some details "2.3 CSL logic formulas" and below: X [R, R][R, R] SFL - Next operator with time and reward bound, first [R, R] defines time bounds, second [R, R] defines reward bound SFL U[ R, R ] [ R, R ] SFL - Bounded until operator with time and reward bound, first [R, R] defines time bounds, second [R, R] defines reward bound For details on CSRL see: 1. C. Baier, B. R. Haverkort, H. Hermanns, and J.-P. Katoen. On the Logical Characterisation of Performability Properties. In ICALP '00: Proceedings of the 27th International Colloquium on Automata, Languages and Programming, pages 780-792, London, UK, 2000. Springer-Verlag. 2. B. Haverkort, L. Cloth, H. Hermanns, J.-P. Katoen, and C. Baier. Model-checking performability properties. In International Conference on Dependable Systems and Networks (DSN), pages 103-112. IEEE CS Press, 2002.