| Bat-L |
f1 |
(◇[4.0,10.0] ((d2 ≥ 4) → (□[4.0,10.0] (b2 = 2)))) |
30 |
0.1 |
12868 |
15.16559 |
⊤ |
20 |
- |
1-step |
| f2 |
((◇[3.0,6.0] (g2 ≤ 5)) U[5.0,20.0] (d2 ≥ 4.5)) |
30 |
3.5 |
20470 |
24.55406 |
⊤ |
20 |
- |
1-step |
| f3 |
(□[1.0,10.0] ((d1 > 8) R[6.0,15.0] (g1 < 1))) |
30 |
0.1 |
20306 |
24.44851 |
⊤ |
20 |
- |
1-step |
| Wat-L |
f1 |
(□[1.0,3.0] ((x1 ≤ 7) R[1.0,10.0] (x2 ≤ 3))) |
20 |
2.5 |
18848 |
22.84081 |
⊤ |
20 |
- |
1-step |
| f2 |
((◇[1.0,10.0) (x2 < 5.5)) U[2.0,5.0] (x1 ≥ 5)) |
20 |
0.1 |
18848 |
22.78498 |
⊤ |
20 |
- |
1-step |
| f3 |
(◇[4.0,10.0] ((x1 ≥ 4) → (□[2.0,5.0] (x2 ≤ 2)))) |
20 |
0.01 |
11234 |
13.67317 |
⊤ |
20 |
- |
1-step |
| Car-L |
f1 |
(◇[1.0,3.0] (□[10.0,25.0] (x > 24))) |
40 |
0.1 |
9949 |
12.60745 |
⊤ |
20 |
- |
1-step |
| f2 |
((◇[1.0,5.0] (y ≥ 10)) R[10.0,20.0] (y < -2)) |
40 |
0.5 |
15885 |
20.80548 |
⊤ |
20 |
- |
1-step |
| f3 |
(□[5.0,15.0] ((x > 14) U[13.0,22.0] (y < -10))) |
40 |
1 |
19585 |
24.42104 |
⊤ |
20 |
- |
1-step |
| Rail-L |
f1 |
(◇[3.0,10.0] ((tx < 50) U[0.0,10.0] (bx > 5))) |
30 |
2 |
17935 |
21.57898 |
⊤ |
20 |
- |
1-step |
| f2 |
((□[2.0,10.0] (tx > 20)) R[0.0,15.0] (bx > 30)) |
30 |
1 |
1246 |
3.62403 |
⊥ |
3 |
- |
1-step |
| f3 |
(□[0.0,5.0] (◇[0.0,10.0] (bx ≥ 50))) |
30 |
0.5 |
802 |
2.64121 |
⊥ |
3 |
- |
1-step |
| Thm-L |
f1 |
(◇[2.0,5.0] ((x1 < 23) R[2.0,10.0] (x2 > 24))) |
30 |
3 |
16839 |
21.25650 |
⊤ |
20 |
- |
1-step |
| f2 |
(□[1.0,4.0] ((x2 < 19) → (◇[5.0,15.0] (x2 > 23)))) |
30 |
1 |
11079 |
15.23610 |
⊤ |
20 |
- |
1-step |
| f3 |
((x2 > 18) U[10.0,20.0] (□[3.0,5.0] (x1 < 19))) |
30 |
2.5 |
975 |
3.56442 |
⊥ |
2 |
- |
1-step |
| Bat-P |
f1 |
(◇[3.0,5.0] ((g2 ≤ 3) U[6.0,10.0] (d2 ≥ 4))) |
25 |
2.5 |
1667 |
5.05166 |
⊥ |
3 |
- |
1-step |
| f2 |
((□[4.0,14.0] (g2 > 4)) U[4.0,10.0] (d2 > 1)) |
25 |
1 |
1753 |
4.56259 |
⊥ |
3 |
- |
1-step |
| f3 |
(□[3.0,10.0] ((d1 ≥ 2) R[0.0,6.0] (g1 ≥ 4))) |
25 |
0.5 |
1671 |
4.67419 |
⊥ |
3 |
- |
1-step |
| Wat-P |
f1 |
(□[1.0,4.0] ((x1 ≥ 6) R[2.0,5.0] (x2 ≥ 3))) |
10 |
0.5 |
917 |
2.59399 |
⊥ |
2 |
- |
1-step |
| f2 |
(◇[0.0,3.0] ((x1 ≥ 7) → (□[3.0,4.0] (x2 ≥ 4)))) |
10 |
2 |
4055 |
6.33861 |
⊤ |
10 |
- |
1-step |
| f3 |
(□[3.0,6.0] ((x2 ≤ 8) U[2.0,3.0] (x1 ≤ 2))) |
10 |
0.1 |
975 |
2.62146 |
⊥ |
2 |
- |
1-step |
| Car-P |
f1 |
(□[0.0,4.0] ((vx < -2) → (◇[2.0,5.0] (rx ≤ -2)))) |
15 |
0.5 |
2236 |
5.74172 |
⊥ |
5 |
- |
1-step |
| f2 |
((◇[0.0,4.0] (ry > 3)) U[0.0,5.0] (vy > 1.5)) |
15 |
2.0 |
1700 |
4.35086 |
⊥ |
3 |
- |
1-step |
| f3 |
(◇[0.0,3.0] ((rx ≤ 5) U[0.0,5.0] (not ix))) |
15 |
0.1 |
7328 |
7.66662 |
⊤ |
10 |
- |
1-step |
| Rail-P |
f1 |
(◇[0.0,5.0] ((pb ≥ 40) U[1.0,8.0] (x < 40))) |
20 |
1.0 |
2318 |
2.90348 |
⊥ |
5 |
- |
1-step |
| f2 |
(◇[0.0,4.0] ((x < 50) → (□[2.0,10.0] (pb > 40)))) |
20 |
5.0 |
3763 |
3.75537 |
⊤ |
10 |
- |
1-step |
| f3 |
(□[0.0,5.0) ((x < 50) U[2.0,10.0] (pb > 5))) |
20 |
4.0 |
1889 |
2.74213 |
⊥ |
4 |
- |
1-step |
| Thm-P |
f1 |
(□[2.0,5.0] ((x1 ≤ 17) R[1.0,4.0] (x2 ≤ 24))) |
10 |
0.5 |
905 |
2.16355 |
⊥ |
2 |
- |
1-step |
| f2 |
(◇[0.0,5.0] ((x1 > 22) → (□[2.0,5.0) (x1 < 18)))) |
10 |
0.1 |
3939 |
6.04902 |
⊤ |
10 |
- |
1-step |
| f3 |
(◇[0.0,10.0] ((x2 ≤ 25) R[2.0,4.0] (x1 > 22.5))) |
10 |
1 |
5683 |
7.31639 |
⊤ |
10 |
- |
1-step |
| Bat-N |
f1 |
(◇[0.0,4.0] ((d ≥ 1) R[0.0,5.0] (g ≤ 7))) |
10 |
1 |
1254 |
81.37168 |
⊥ |
3 |
258 |
2-step |
| f2 |
(□[3.0,4.0] ((g < 6) → (◇[0.0,6.0] (d ≥ 3)))) |
10 |
1.5 |
868 |
46.56047 |
⊥ |
3 |
251 |
2-step |
| f3 |
(□[1.0,3.0] (◇[0.0,5.0] (d > 1.5))) |
10 |
1 |
838 |
81.68621 |
⊥ |
3 |
439 |
2-step |
| Thm-N |
f1 |
(◇[0.0,15.0] ((x0 ≥ 14) U[0.0,inf) (x1 ≤ 19))) |
25 |
0.5 |
1205 |
725.67633 |
⊤ |
5 |
3420 |
2-step |
| f2 |
(□[2.0,4.0] (((x0 - x1) ≥ 4) → (◇[3.0,10.0] ((x0 - x1) ≤ -3)))) |
25 |
2.0 |
744 |
10.97285 |
⊥ |
2 |
70 |
2-step |
| f3 |
(□[0.0,10.0] ((x0 > 23) R[0.0,inf) ((x0 - x1) ≥ 4))) |
25 |
2.0 |
1150 |
84.08775 |
⊥ |
4 |
201 |
2-step |
| Oscil-N |
f1 |
(◇[0.0,3.0] ((x3 ≥ 1) R[0.0,inf) (y ≤ 10))) |
8 |
0.1 |
1543 |
81.59113 |
⊤ |
5 |
264 |
2-step |
| f2 |
(◇[2.0,5.0] (□[0.0,3.0] (x2 < 4))) |
8 |
1.0 |
1234 |
241.90643 |
⊥ |
3 |
801 |
2-step |
| f3 |
((□[1.0,3.0] (x ≤ 2)) R[2.0,5.0] (x3 > 2)) |
8 |
0.1 |
1762 |
58.70690 |
⊥ |
3 |
193 |
2-step |
| Space-N |
f1 |
(□[0.0,2.0] (((vx + vy) ≤ -2) → (◇[0.0,3.0] ((vx + vy) > 10)))) |
5 |
1.5 |
786 |
1179.39166 |
⊥ |
2 |
75 |
2-step |
| f2 |
(◇[2.0,3.0] (□[1.0,2.0] (x ≤ 40))) |
5 |
0.1 |
1074 |
20.79598 |
⊥ |
3 |
79 |
2-step |
| f3 |
(◇[0.0,4.0] ((x ≥ 30) U[0.0,inf) (vx ≤ -2))) |
5 |
0.5 |
1289 |
634.59946 |
⊤ |
5 |
2588 |
2-step |
| Nav-N |
f1 |
(◇[2.0,4.0] ((y ≥ 30) → (□[1.0,5.0] (y ≥ 60)))) |
10 |
3 |
1168 |
130.12802 |
⊥ |
3 |
529 |
2-step |
| f2 |
(□[3.0,7.0] (◇[1.0,2.0] (vy ≥ 5))) |
10 |
2 |
1138 |
129.72835 |
⊥ |
3 |
511 |
2-step |
| f3 |
(◇[1.0,5.0] ((vx ≥ 2) R[0.0,inf) (x ≤ 80))) |
10 |
1 |
1399 |
786.11321 |
⊤ |
5 |
2949 |
2-step |
| Wat-N |
f1 |
((x ≥ 2) R[0.0,3.0] (◇[2.0,4.0] (x > 5))) |
8 |
2 |
1142 |
60.28788 |
⊥ |
3 |
212 |
2-step |
| f2 |
(◇[0.0,4.0] ((x > 3) → (□[2.0,3.0] (x ≤ 2.5)))) |
8 |
0.1 |
756 |
59.09845 |
⊥ |
3 |
318 |
2-step |
| f3 |
(□[2.0,4.0] (◇[0.0,4.0] (x < 3))) |
8 |
0.5 |
726 |
72.63571 |
⊥ |
3 |
413 |
2-step |
| Car-N |
f1 |
(◇[1.0,3.0] (□[0.0,2.0] (theta1 > 1))) |
5 |
1 |
1218 |
21.42666 |
⊥ |
2 |
85 |
2-step |
| f2 |
((◇[1.0,2.0] (ry ≥ 1)) R[0.0,2.0] (theta1 > 2)) |
5 |
0.5 |
1498 |
34.32676 |
⊥ |
2 |
129 |
2-step |
| f3 |
(□[0.0,2.0] ((rx > 2) → (◇[2.0,3.0] (ry < -1)))) |
5 |
2 |
1242 |
17.67457 |
⊥ |
2 |
70 |
2-step |
| Rail-N |
f1 |
(□[1.0,3.0] ((vb > 6) → (◇[2.0,4.0] (b > 60)))) |
8 |
2 |
848 |
49.30031 |
⊥ |
3 |
244 |
2-step |
| f2 |
((◇[1.0,3.0] (b ≥ 5)) R[0.0,inf) (vb ≤ 10)) |
8 |
0.1 |
919 |
951.34660 |
⊤ |
5 |
4016 |
2-step |
| f3 |
(◇[0.0,4.0] (□[2.0,4.0] (b ≥ 80))) |
8 |
1 |
570 |
64.42260 |
⊥ |
2 |
66 |
2-step |