Mora - Automatic Generation of Moment-Based Invariants
497
E[u
2 ] =
b
2
3
E[x
1 ] = 0
E[y
1 ] = y(0)
E[x
2 ] =
b
2 n
3
E[u
1 ] =
b
2
E[y
1
x
1 ] =
b
2 n
6 (n + 1)
E[y
2 ] =
n
18
2b
2
n
2 + 3b
2
n + b
2 + 18
+ y(0)
2
E[g
1 ] = 0
E[g
2 ] = 1
(4)
with y(0) standing for the initial value of y (treated as a parameter, since not specified).
MORA – Out Parser. MORA’s output consists of basic information about the program
and the goal, moment-based invariants computed, and computation time. By default, the
MORA output is shown only on the screen. However, an optional argument can specify
if an output file should be created. Two possible values for output format are (i)
"txt", producing a simple human-readable file, and (ii) "tex", producing a file with
invariants in L A T E X format (as given in (4) above).
5 Evaluation
A proof-of-concept implementation, together with initial experiments, were already
given in our work on generating moment-based invariants [2]. MORA comes however
with a new design and re-implementation of [2], significantly improving the experimental setting and evaluations of [2]. Table 1 compares MORA against the experiments
of [2], on a subset of Prob-solvable loops from [2], evidencing that MORA is faster
than our initial proof-of-concept implementation. This is due to the following reasons:
Program
Moment Runtime
PoC (s)
Runtime
MORA (s)
SUM RND SERIES
1
0.31
0.22
2
2.89
0.93
3
17.7
2.47
STUTTERINGA
1
0.44
0.25
2
2.20
1.07
3
8.48
3.35
STUTTERINGC
1
1.80
0.66
2
72.5
12.2
3
2144
73.9
SQUARE
1
0.38
0.22
2
2.46
0.73
3
8.70
1.67
Table 1. Comparison of MORA vs. proofof-concept (PoC) implementation of [2].
– MORA now optimizes the order in which recurrences are sent to the diofant recurrence solver. This reduces the amount of necessary symbolic computation and speeds up
the process.
– While MORA is implemented entirely in
python, with limited usage of external libraries, the previous implementation was
done in Julia and relied on calls to the
sympy library of python.
– MORA does not rely on Aligator [6] for
handling systems of recurrences, allowing us
to eliminate some intermediate and redundant
steps.
6 Conclusion
We described MORA, a fully automated tool for generating invariants of probabilistic
programs. MORA combines recurrence solving, symbolic summation and statistical reasoning, and derives higher-order moments of loop variables in probabilistic programs.
497
E[u
2 ] =
b
2
3
E[x
1 ] = 0
E[y
1 ] = y(0)
E[x
2 ] =
b
2 n
3
E[u
1 ] =
b
2
E[y
1
x
1 ] =
b
2 n
6 (n + 1)
E[y
2 ] =
n
18
2b
2
n
2 + 3b
2
n + b
2 + 18
+ y(0)
2
E[g
1 ] = 0
E[g
2 ] = 1
(4)
with y(0) standing for the initial value of y (treated as a parameter, since not specified).
MORA – Out Parser. MORA’s output consists of basic information about the program
and the goal, moment-based invariants computed, and computation time. By default, the
MORA output is shown only on the screen. However, an optional argument can specify
if an output file should be created. Two possible values for output format are (i)
"txt", producing a simple human-readable file, and (ii) "tex", producing a file with
invariants in L A T E X format (as given in (4) above).
5 Evaluation
A proof-of-concept implementation, together with initial experiments, were already
given in our work on generating moment-based invariants [2]. MORA comes however
with a new design and re-implementation of [2], significantly improving the experimental setting and evaluations of [2]. Table 1 compares MORA against the experiments
of [2], on a subset of Prob-solvable loops from [2], evidencing that MORA is faster
than our initial proof-of-concept implementation. This is due to the following reasons:
Program
Moment Runtime
PoC (s)
Runtime
MORA (s)
SUM RND SERIES
1
0.31
0.22
2
2.89
0.93
3
17.7
2.47
STUTTERINGA
1
0.44
0.25
2
2.20
1.07
3
8.48
3.35
STUTTERINGC
1
1.80
0.66
2
72.5
12.2
3
2144
73.9
SQUARE
1
0.38
0.22
2
2.46
0.73
3
8.70
1.67
Table 1. Comparison of MORA vs. proofof-concept (PoC) implementation of [2].
– MORA now optimizes the order in which recurrences are sent to the diofant recurrence solver. This reduces the amount of necessary symbolic computation and speeds up
the process.
– While MORA is implemented entirely in
python, with limited usage of external libraries, the previous implementation was
done in Julia and relied on calls to the
sympy library of python.
– MORA does not rely on Aligator [6] for
handling systems of recurrences, allowing us
to eliminate some intermediate and redundant
steps.
6 Conclusion
We described MORA, a fully automated tool for generating invariants of probabilistic
programs. MORA combines recurrence solving, symbolic summation and statistical reasoning, and derives higher-order moments of loop variables in probabilistic programs.