Table 1: LTL property verification using ProB.
| LTL property | Meaning | Result |
| G{state/ = STOP} | State stop is not reached for M1. | A counterexample has been found: (Move → changeStatetoS2)179 → move → reachStop |
| G{(theta > -50)&(theta < 50)} | Theta is in (-50, 50) | A counterexample has been found: (Move → changeStatetoS2)50 |
| G {x < 12} | The length of arm is less than 12 | A counterexample has been found: (Translation → changeStatetoS1)2 |
| G{state/ = final} | State final is not reached for M2. | A counterexample has been found: (Translation → changeStatetoS1)35 → translation → reachFinal |