Model Checking

Caesar can export HeyVL programs to the jani-model format so they can be analyzed using probabilistic model checkers. The JANI project defines exchange formats for quantitative model checking problems (and more). Caesar outputs Markov chains (MCs) or Markov decision processes (MDPs), depending on which HeyVL language features are used.

The translation supports executable HeyVL programs. These are written in a subset of HeyVL, for which we have well-defined forwards-stepping MC/MDP semantics. Not supported right now is local unbounded nondeterminism (havoc or uninitialized local variables), procedure calls or quantitative assume statements.

After exporting HeyVL programs to JANI, we can use probabilistic model checkers to calculate and/or verify expected rewards. In contrast to Caesar, these do not need user annotations like invariants, but are fully automatic. On the other hand, probabilistic model checkers often struggle with large or infinite state spaces. Thus, the two approaches complement each other.

We like the probabilistic model checker Storm. Caesar has a dedicated backend for Storm to automatically run Storm and extract the results.

Note: Caesar should not be confused with the set of tools in the CADP toolbox by INRIA, which includes tools like CAESAR, CAESAR.ADT, or OPEN/CAESAR. These also enable model checking of software, but are unrelated to this project.

Usage

For a simple example, consider the HeyVL program below.

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

You can either use Caesar's automatic Storm backend or generate JANI manually to use them however you wish.

Caesar will assign arbitrary initial values to output parameters and assumes that they are never read before they are written to. To disable this or learn more, read the section on initial values of output parameters. In addition, note that we always use least-fixed point semantics for loops in the JANI translation, therefore wlp semantics is not supported.

The generated Markov chain model is finite-state and has a single initial state (no input parameters). You'll usually want to maintain these restrictions when using a model checker. Read more about infinite-state and parametric models below.

Option A: Caesar's Storm Backend

Caesar can automatically generate JANI files and run the probabilistic model checker Storm.

To enable it, pass the --run-storm OPTION parameter to the command-line with one of the following values for OPTION:

• path: Search for the Storm binary on the PATH.
• docker-stable: Run Storm via the movesrwth/storm:stable Docker image.
• docker-ci: Run Storm via the movesrwth/storm:ci Docker image.

The latter two options need to have Docker installed and running. If the images are not installed, Docker will download them automatically. This might take a while.

Caesar does not automatically update these images. To update the :ci image for example, run docker pull movesrwth/storm:ci.

The above flag can be used with Caesar's mc command: For example:

caesar mc --run-storm path example.heyvl

The result will look like this:

Expected reward from Storm: ≈ 0.9999995232

The result is approximate because it was computed via floating-point arithmetic. To get exact results at the expense of slower computation, you can add the --storm-exact flag.

You can also use the --run-storm flag with the verify command or with our LSP server. Furthermore, you can set the --no-verify flag to only run model checking and not run Caesar's deductive verification.

Option B: Generating JANI Manually

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

caesar mc example.heyvl --jani-dir DIR

The output JANI files will have the following structure that you can use:

• Properties:
  • reward: This is the expected value of the verification conditions (cf. Statements).
  • diverge_prob: The probability of not reaching the end of the (co)proc.
  • can_diverge: Boolean property whether the program has a path that does not reach the end of the (co)proc.¹
• Constants:
  • One constant for each input variable of the (co)proc (constant has same name as variable).

Now you can use your favorite model checker with the resulting JANI files.

Running Storm Manually

Quick Start: Using Storm via Docker.

Using Docker, you can download and run the latest version of Storm with just one command.

docker run --mount type=bind,source="$(pwd)",target=/pwd -w /pwd --rm -it --name storm movesrwth/storm:stable storm [ARGS...]

This command will automatically download the latest stable build of Storm (c.f. list of Storm Docker image releases). The container will have the current directory mounted as /pwd and the container will use that as the working directory. Note that this means you can only access files from your working directory inside the container. After running the command, the container will be deleted.

Read more on Storm's documentation page for its Docker containers.

Running Storm on the produced file computes the expected reward.²

storm --jani DIR/FILE.jani -jprop reward --exact --sound

Part of the output:

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

Parametric and Infinite-State Models

Model checkers usually work with finite-state models with a single initial state, therefore programs that do not fit into this category are often not so simple to model check. We modified our original example and added an input parameter init_c (multiple initial states, therefore "parametric") and removed the bound on the loop (infinite number of states).

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

With Caesar, we could run the following command to approximate the expected reward for the program with init_c = 5 with 10000 states:

caesar mc --run-storm <VALUE> example.heyvl --storm-constants init_c=5 --storm-state-limit 10000

And we get a result like this:

Expected reward from Storm: ⪆ 0.9999847412

Inputs Are Translated to Constants. The input parameters of the program are translated by Caesar to constants in the JANI model.

• For the Caesar's Storm backend can fix values with the --storm-constants <name>=<value>,...,<name>=<value> command-line flag.
• Storm itself uses the --constants <name>=<value>,...,<name>=<value> command-line flag.

Caesar can also be instructed to translate inputs to variables instead of constants with the --jani-no-constants flag.

State Limits to Approximate Infinite-State Models. Storm can be used with a state limit so that the model generation will stop its exploration at some number of states. This will yield a correct under-approximation of the expected reward.

• For Caesar's Storm backend, this as the --storm-state-limit <limit> command-line flag.
• Storm itself uses the --state-limit <limit> command-line flag.

This feature is available since Storm 1.9.0 (PR #521).

Parametric Model Checking. If the program has input variables, Storm's parametric model checking may be of interest.

Relation to Caesar's Unrolling Proof Rule

Caesar's unrolling proof rule can also be used to obtain sound bounds on expected rewards. The unrolling proof rule is also sometimes called bounded model checking. However, that proof rule is a bounded unrolling of the weakest pre-expectation semantics and therefore essentially an unrolling of all possible paths in the Markov chain. In contrast, the complexity of probabilistic model checking scales only in the number of states and not in the number of paths. Therefore, these techniques are somewhat related, but distinct.

For the original non-parametric example from the Usage section, we obtain the optimal lower bound in Caesar without using a model checker. The annotation @unroll(22, 0) for unrolling depth 22 finds the optimal value in this case.

Unrolling Proof Rule Example

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

Because we gave no pre, Caesar will try to verify whether $\infty$ is a lower bound to the expected value. We get a counter-example:

Counter-example to verification found!

the pre-quantity evaluated to:
    0.99999... (2097151/2097152)

Supported Programs

The translation to JANI supports a large subset of the HeyVL language. You can use for example assignments, loops, conditionals, and probabilistic choices. Nondeterministic choices and assertions are also supported, as well as Boolean assume statements. Not supported right now is local unbounded nondeterminism (havoc or uninitialized local variables), procedure calls or quantitative assume statements.

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).
• pure funcs (not uninterpreted functions)

Supported Statements

In the body, statements:

• Blocks,
• Variable declarations with initializers,
• Assignments with pure expressions,
• Sampling from distributions,
• If-then-else statements,
• While loops (with least-fixed point semantics — see below for semantics details),
• reward statements,
• In procs:
  • assert statements,
  • Binary demonic choices,
• In coprocs:
  • coassert statements,
  • Binary angelic choices,
• Assumptions of the form assume ?(b) and coassume !?(b),
• Annotations, in particular proof rule annotations, will be ignored.

Initial Values of Output Parameters

Caesar will try to choose valid initial values for variables of built-in types such as Bool. This reduces the number of initial states the model checker has to check. We do this in a way that is not observable to the program, with one exception.

warning

By default, the JANI translation will assign arbitrary initial values to output variables. This is correct when output variables are never read before they are written to. However, if uninitialized output variables are read, then the choice is observable.

This behavior can be disabled with the --jani-uninit-outputs option so that output variables are left uninitialized in the JANI model.

Loop Semantics

warning

In the JANI translation, while loops are always assumed to have least fixed-point semantics when model-checking.³ 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).⁴

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.⁵ This property is currently not supported by Storm.¹

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:

• Bool,
• UInt,
• Int,
• UReal,
• Real.

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 assume or coassume statements.
• In user-defined domains, uninterpreted functions are not supported and axioms will be ignored.

Footnotes

1. 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. ↩ ↩²

2. 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. ↩

3. 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. ↩

4. Corollary 4.26 of Benjamin Kaminski's PhD thesis states that (one-bounded) wlp can be computed via wp plus the probability of divergence. ↩

5. 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. ↩