Skip to main content

Model Checking

Caesar has some support to export probabilistic programs written in (an executable fragment of) HeyVL to the jani-model format. The JANI project defines exchange formats for quantitative model checking problems (and more).

Executable HeyVL programs are essentially programs without verification statements, where therefore the Markov chain semantics is clearly defined and the program can be executed forwards in a step-by-step fashion.

After exporting HeyVL programs to JANI, we can use our favorite probabilistic model checkers to calculate and/or verify expected rewards. For now, we have only tested with the model checker Storm.

caution

This feature is still under development. There are sure to be bugs and missing functionality. The encoding is sure to change in the near future.

Usage​

For a simple example, consider the HeyVL program below.

@wp
proc geo_mc(init_c: UInt) -> (c: UInt, cont: Bool)
    post [!cont]
{
    c = init_c
    cont = true
    while cont && c <= 20 {
        var prob_choice: Bool = flip(0.5)
        if prob_choice { cont = false } else { c = c + 1 }
    }
}

To export JANI files for the model checker, simply run Caesar with the --jani-dir DIR option to instruct it to save all translateable (co)procs to .jani files in the directory DIR:

caesar example.heyvl --jani-dir DIR

We use the probabilistic model checker Storm. Running Storm on the produced file gives us the optimal value.1 Procedure inputs to are translated to JANI's constants, and must be given to Storm via the flag --constants init_c=0 (any other initial value can be chosen).

$ storm --jani DIR/FILE.jani -jprop reward --exact --sound --constants init_c=0

Part of the output:

Model checking property "reward": R[exp]{"reward"}min=? [C] ...
Result (for initial states): 2097151/2097152 (approx. 0.9999995232)
note

In this particular case, we can obtain the optimal lower bound in Caesar by using the unrolling proof rule. The annotation @unroll(22, 0) for unrolling depth 22 finds the fixpoint in this case. But this is only exact if we can bound the number of loop iterations statically.

Supported Programs​

The currently implemented translation only supports a subset of the executable fragment of HeyVL.

Supported Declarations​

  • proc and coproc specifications with:
    • Inputs and output declarations,
    • pre declarations that are only Boolean conditions of the form ?(b).
    • post declarations (arbitrary operands).

Supported Statements​

In the body, statements:

Loop Semantics​

danger

In the JANI translation, while loops are always assumed to have least fixed-point semantics when model-checking.2 That means we just accumulate total expected rewards over all terminating executions in the Markov chain. This corresponds to wp/ert semantics.

Notice that in procs, this is different from the default behavior of Caesar's proof rules such as induction. They would assume greatest fixed-point (wlp) semantics in procs. We recommend always adding the @wp or @ert annotations to your proc/coproc. They instruct Caesar to enforce that sound proof rules for least fixed-point semantics are being used.

If you want one-bounded wlp semantics (greatest fixed-points), then you can use the generated property diverge_prob to obtain the probability of divergence. Then the result should be the sum of the reward and diverge_prob properties (Storm: -jprop reward,diverge_prob).3

If you want unbounded greatest fixed-point semantics, then you can use the generated property can_diverge to check whether there is a diverging path. Then the result is \infty if can_diverge is true, otherwise the result is reward.4 This property is currently not supported by Storm.5

We intentionally avoid using the reachability reward properties (i.e. setting the reach property of ExpectedValueExpression in JANI) as it will assign the expected reward \infty to any state from which goal states are not reachable with probability 1. If the program is not AST, then this does not correspond to either least or greatest fixpoint semantics weakest pre-expectation style semantics that we know of.

Supported Types​

The supported types of values are:

Make sure to check in your model checker's documentation how these types are realized. For example, Storm assumes 32-bit numbers by default for unbounded integer types.

EUReal values are currently only supported as values in pre/post declarations and in assert statements. The value \infty cannot be explicitly represented in JANI, therefore EUReal expressions that go beyond the specific supported verification constructs are not supported.

Not Supported​

In particular, the following constructs are not supported:

  • Calls to uninterpreted functions or to procs/coprocs,
  • Uninitialized variable declarations or havoc/cohavoc statements,
  • Quantitative verification statements such as assume/assert in arbitrary locations.
  • User-defined domains, axioms will be ignored.
  1. We use the --exact and --sound flags to ensure that Storm is forced to use exact arithmetic and only sound algorithms to produce the solution. Consult your chosen model checker's documentation to see which guarantees they give.↩
  2. We always use least-fixed point semantics because encoding greatest fixpoint/weakest liberal pre-expectation semantics seems to be impossible with a single JANI property right now.↩
  3. Corollary 4.26 of Benjamin Kaminski's PhD thesis states that (one-bounded) wlp can be computed via wp plus the probability of divergence.↩
  4. This is similar to the qualitative wlp, which evaluates to the top element of the Boolean lattice (true) if the loop has a possibility of nontermination. In the quantitative setting, we have \infty as our top element of the EUReal lattice.↩
  5. Storm currently does not support the qualitative analysis required for the can_diverge property and will throw an error. The feature is tracked in the issue moves-rwth/storm#529.↩