Using POPACheck

Usage

POPACheck can be executed on an input file file.pomc as follows:

stack exec popacheck -- file.pomc {args}

POPACheck stack commands take a few arguments:

• --noovi [default: False]. When set, POPACheck uses Z3 instead of OVI for computing upper bounds to termination probabilities. As the experimental evaluation of [16] suggests, this leads almost always to timeouts, and will probably will be removed in then near future.

• --gauss [default: False]. When set, POPACheck uses Value Iteration with Gauss-Seidel update for computing lower bounds to termination probabilities, and to fractions in quantitative model checking. The default method is Newton’s iterative method. We refer to PreMo publications [17, 18] for a detailed description of these two numerical methods. In our experiments, Newton’s method tends to be slightly faster than Gauss-Seidel Value Iteration.

• --verbose [default: 0]. Logging level. 0 = no logging, 1 = show info, 2 = debug mode.

Directory eval contains the Python script probbench.py, which may be useful to evaluate POPACheck input files, as it also prints a summary of the resources used by POPACheck. It must be executed with a subdirectory of ~/path/to/POPACheck-sources as its working directory, and either --print to print the results in the shell, or --raw_csv file_name for saving results in .csv format in file_name.

cd ~/path/to/POPACheck-sources/eval
./probbench.py prob/established/qualitative/schelling --print

evaluates all *.pomc files in directory ~/path/to/POPACheck-sources/eval/prob/established/qualitative/schelling.

Input Format

POPACheck input files contain probabilistic programs in the MiniProb programming language. Learn how to write them in the section about MiniProb Syntax. The structure of input files depends on the type of query that we are asking POPACheck to solve.

Probabilistic Queries

A probabilistic query must be put at the beginning of a .pomc file, before the program. Queries follow the syntax:

\(\texttt{probabilistic query:} \, \, q \texttt{;}\)

where \(q\) is one of the queries in the table below:

Query	Meaning	Formula?
\(\texttt{approximate}\)	what is the program’s termination probability?	No
\(\texttt{qualitative}\)	Does the program satisfy formula \(f\) almost surely?	Yes
\(\texttt{quantitative}\)	What is the probability that the program satisfies formula \(f\)?	Yes

When a formula is needed, it has to be placed on a new line with syntax:

\(\texttt{formula:} \, \, f \texttt{;}\)

where \(f\) follows the syntax reported in Writing Requirements. For technical reasons explained in [8], POPACheck does not support the whole POTL logic, but only the operators marked with a ✓ in column POTL \(\chi\) of the table in Writing Requirements. Though, POPACheck supports full LTL. To get an idea of queries, consider inspecting different experiments in eval/prob/established/, where the same programs are verified against different queries.

Plain reachability queries are supported through the LTL \(\texttt{Eventually}\) operator at the moment. We plan to optimize them in future work, as they could be encoded as termination queries.

Additionally, POPACheck supports also the query \(\texttt{unfold\&export}\), which constructs a Markov Chain in explicit Storm format for a given program by unfolding the program’s stack. Argument maxDepth to the stack command specifies the maximum stack depth to unfold [default: 100]. When maxDepth is reached, recursion is not unfolded anymore, and a simple self-loop is added. Note that MiniProb programs may have infinite recursion. We use this feature for testing purposes, and do not advertise users to try it out.

An example: Pre/Post Conditions.

With POTLf\(\chi\) it is possible to express and check automatically pre/post conditions on recursive programs. Consider the following Hoare triple:

\(\varphi \, \, \{ \, P \, \} \,\, \theta\)

where \(P\) is a potentially recursive program. We want to check whether, if \(\varphi\) holds at a call of \(P\) (pre-condition), then \(\theta\) holds at the corresponding return (post-condition). This requirement cannot be expressed with LTL as it is a context-free requirement, but it can be expressed with POTLf\(\chi\) via:

\(\texttt{probabilistic query: qualitative;}\) \(\texttt{formula: G ((call And P And } \varphi \texttt{) Implies (XNu (ret And P And } \theta \texttt{)))}\)

which means that always (G), if the program is in a state calling \(P\) and where \(\varphi\) holds, then (Implies) this call has a matching return (XNu (ret And P)) where \(\theta\) holds. Note that this formula does not hold almost surely if \(P\) has non zero probability of non terminating—nonterminating runs do not have a matching return.

Interpreting the output

The output of running a query is quite verbose at the moment. For example:

stack exec -- popacheck eval/prob/established/quantitative/schelling/Q03.pomc

prints

Quantitative Probabilistic Model Checking
Query: G (((call And alice) And [| (p == [4]4)]) --> (~ (XNu obs)))
Result:
  Lower bound: 0.8947
  Upper bound: 0.8947

Total elapsed time: 21.06 s (2.1061e1 s)

POPACheck outputs a lower and an upper bound to the probability that the Schelling model satisfies formula Q03.

When given the flag --stats, POPACheck yields a more verbose output:

Quantitative Probabilistic Model Checking
Query: G (((call And alice) And [| (p == [4]4)]) --> (~ (XNu obs)))
Result:  (5064173399 % 5660011320,6145 % 6868)
Floating Point Result:  (0.8947284930518479,0.894729178800233)
Elapsed time: 20.74 s (total), 2.3883e-2 s (upper bounds), 2.8956e-2 s (PAST certificates), 1.1778e0 s (graph analysis),1.1905e1 s
(upper bounds with OVI for quant MC),7.5453e-4 s (eq system for quant MC).
Input pOPA state count: 311
Support graph size: 682
Equations solved for termination probabilities: 1230
Non-trivial equations solved for termination probabilities: 266
SCC count in the support graph: 1117
Size of the largest SCC in the support graph: 24
Largest number of non trivial equations in an SCC in the Support Graph: 52
Size of graph G: 44
Equations solved for quant mc: 893036
Non-trivial equations solved for quant mc: 68226
SCC count in quant mc weight computation: 336410
Size of the largest SCC in quant mc weight computation: 144
Largest number of non trivial equations in an SCC in quant mc weight computation: 7318

Most of lines just print statistics about the experiment. The important line is:

Floating Point Result:  (0.8947284930518479,0.894729178800233)

which shows, respectively, a lower and an upper bound to the probability that the model satisfies the formula. It might be of general interest to inspect the overall number of equations solved (i.e., the size of the PPS), 893036 in this case, or the number of states in the input model, 311.