(Counter)Example Generation

[BitVortex]

The tool paper "A Storm is Coming: A Modern Probabilistic Model Checker" describes a counterex engine (cp. Fig. 1), which is currently neither documented online nor available for use with the -e switch.

I would like to obtain examples of paths/states where a verified property either holds or is violated, especially in a non-deterministic MDP. Is the aforementioned engine implemented and could be used for this purpose? If not, what other approaches could lead to solving this issue, which data is either already available or could be exposed by Storm that could help with this cause?

[sjunges]

Hi,

there are various notion of counterexamples, and some of them are built into storm. Some are available via the command line, some are only present in the APIs.

I do not yet understand what kind of counterexample you expect: In particular: What is a verified property? What do you mean with paths where a property does not hold? What is the role of the scheduler/policy here? Is your notion of a counterexample described somewhere in the literature? To help describe what you want, it would be fabulous if you would add what kind of input and what kind of output you expect. There is a PhD thesis by Nils Jansen (2015) that might help to identify what you want to do.

However, if you just want to know which states satisfy a PCTL property, there is no need to compute counterexamples: the model checking result should suffice.

To conclude: Storm does support various types of counterexamples, but most of the documentation on this is currently in papers and not yet on our website.

P.S. Various key developers are currently on a holiday---including me. Thus, support might be a bit slow.

[BitVortex]

Hi, thanks for the fast answer, especially during the holiday. I'd like to obtain counterexamples or witnesses as described in 'The Principles of Model Checking' by C. Baier and J.-P. Katoen in chapter 6.6 'Counterexamples and Witnesses'. With verified property I mean the property passed to the model checker using the --prop parameter; I would like to not only get a probability as a result, but also a description of a transition sequence that led to the result, e.g. a sequence where P=1 for the passed property holds.

I know about the Storm tool paper mentioned in my original question. Thank you for pointing me to the thesis of Dr. Jansen, it describes what I want to obtain quite good. Apart from the COMICS example it seems to be rather theoretical, though, are the described methods (partly) implemented in Storm already? Could you point me to the papers you mentioned that describe the functionality of Storm which is not yet available on the website?

[sjunges]

The main problem is that in DTMCs, a single path in general does not suffice to prove (or reject) the property. Thus, before we can help you further, I think you might have to dive into a bit of theory.... :-)

We can compute k-Shortest paths (which should be described in the thesis), or high-level counterexamples, see also the thesis of Christian Hensel (formerly Christian Dehnert) https://moves.rwth-aachen.de/research/publications/?authorid=413

[arturrataj]

I have a similar question. To give a concrete example, Prism when asked a question "E [ F c_update=1 ]" showed this:

Result: true (property satisfied in the initial state)

Counterexample/witness: (0,0,2,0,0,0,0,0,0,0,0,0,0) (1,0,2,1,0,0,0,0,0,0,0,0,0) (1,0,2,1,0,0,0,0,1,0,0,0,0)

i.e. an example path which leads to some state where c_update=1. This very useful, for example answers the question "give a concrete example where the system does not work". In Prism the functionality is rather limited, for example I can not get all paths which satisfy a property, or n best paths which minimise/maximise a property. I get just a random witness, but it is still much better than nothing.

[arturrataj]

In what I would think is an equivalent in Storm (just a basic case of an adversary) what I get instead is:

Command line arguments: --prism simple_model.nm --prop 'Pmax>0 [ F c_update=1 ]' --counterexample
Current working directory: /home/art/projects/hedgeelleth/Ctira

Time for model input parsing: 0.011s.

Time for model construction: 0.828s.

-------------------------------------------------------------- 
Model type:     MDP (sparse)
States:     52421
Transitions:    426835
Choices:    426835
Reward Models:  none
State Labels:   3 labels
   * deadlock -> 0 item(s)
   * (c_update = 1) -> 12447 item(s)
   * init -> 1 item(s)
Choice Labels:  none
-------------------------------------------------------------- 
ERROR (model-handling.h:561): The selected counterexample formalism is unsupported.
ERROR (storm.cpp:23): An exception caused Storm to terminate. The message of the exception is: NotSupportedException: The selected counterexample formalism is unsupported.

[cdehnert]

Hi,

if you specify the formula as P<=0 [F c_update=1] and provide --counterexample --counterexample:mincmd maxsat, you should be able to get a subset of the commands of the PRISM program that by itself violates the formula. In this particular case, this means that the commands allow a path (with non-zero probability) from an initial state to a state with c_update=1.

a) Does this work for you? If not, what output do you see? (Note that generating the counterexample may take a while as this is an NP-hard problem.) b) Does this help you at all?

Best, Chris

[arturrataj]

Yes, it is about an adversary for the user, in the sense of additional useful data whose generation may take time. After the post of sjunges, I thought that you talk about an adversary needed to prove a property. I am sorry for the misunderstanding, I will look into your papers for details. Thanks.

[arturrataj]

What I get is a list of statements. I wonder if their order is important, because the output looks like a complete Prism source file, where the order is not important. In general it might be useful to have just a list of subsequent states, so that there is no need of re-interpreting these statements. Possibly it is what you call a low-level counterexample.

[arturrataj]

Is it an MDP which covers all DTMCs which violate the property?

[arturrataj]

Is the state space always completely reduced to the counterexamples? I will look into "High-Level Counterexamples for Probabilistic Automata" for details. At first glance, it is not. With the option MILP the automaton has been so reduced it does not represent even a single counterexample (which exists in reality).

For the same model, Prism can compute a concrete counterexample path in seconds, while Storm generates the high-level representation for very long times. All in all, a fast method of just generating any chosen witness would be very useful.

[cdehnert]

What Storm gives you, is a sub-MDP M of the original model such that M violates the property. By adding more commands in the PRISM program, reachability probabilities can only increase. This means that every extension of the selected commands will also give rise to an MDP that violates the property. The order of PRISM commands is generally not of importance in the model, so the selection you get are also not ordered. Note that what is minimized here is the number of commands in the PRISM model and not the number of states of the underlying MDP. The latter can also be computed with a slight extension of what we have internally, but is computationally much more involved. Approximations are presented by Nils Jansen's PhD thesis, but are not implemented (at least not in an accessible way).

Low-level counterexamples are currently not exposed to the outside, so there is no way to obtain paths violating a given property. In your case (P<= 0 [...]), a single path suffices but with arbitrary probability bounds, the set of necessary paths may grow very large or even infinite (for strict probability comparison in the formula). Hence, it is not entirely clear whether they are useful in general. Internally, the building blocks to compute path-based counterexamples are there, but it has not been a priority to expose them because it's yet to be seen how to make effective use of them.

If selecting MILP gives you different results than maxsat, we would be interested in fixing this behaviour (one potential source of error are inaccuracies in the MILP solver). If you could provide us with the model, this would be a great help. Also high-level counterexamples are harder to compute because of the combinatoric nature of the problem. Path search is fast, but as argued above in the general case (where more than one path is needed) it is not clear how to effectively use the results. There is a tool called COMICS that may be a bit outdated by now, but is more focused on finding paths and concrete sub-models.

[arturrataj]

Thank you for the details. I guess that P<=0 [ ... ] is a frequent corner case in validating a system, supporting just this would suffice in many cases.

I do not know if I can attach a file here, so I sent the model via e-mail with necessary information to storm-dev@i2.informatik.rwth-aachen.de.

[arturrataj]

As of me, I suppose that I never needed a counterexample for something different that P<=0 [ ... ] or P>=1 [ ... ].

[volkm]

Path-based counterexamples are now available from the CLI (b0abbb5088a56588590aff80b89ec2f679d717d3).

For a reachability property of the form P<=0.2 [F "target"] we can now compute a shortest paths counterexample by providing the arguments -cex --cextype shortestpath. Storm then outputs the most probable paths reaching the target state(s) whose accumulated probability already exceeds the given threshold. With the additional argument --shortestpath-maxk <k> one can limit the number of printed paths to at most k. Note that the states are given by their id and their labeling. If one further provides the argument --buildstateval all variable valuations are also printed.

Note that the path-based counterexamples are only supported for DTMCs. A possible workaround for MDPs would be to first export a maximising/minimizing scheduler with --exportscheduler <outputfile> and then manually adapting the model to create a DTMC on which the k-shortest path algorithm works.

I hope this helps in debugging your models.

[arturrataj]

Thanks volkm. I would have some questions.

With the workaround, the method effectively shows most probable paths within a given chosen scheduler. I wonder if it would be possible to generate multiple schedulers if they exist, so that globally most probable paths could be found. For example:

module p
  s0 : [0..3] init 0;

  [] s0=0 -> (s0'=0);
  [] s0=0 -> (s0'=1);
  [] s0=0 -> (s0'=2);
  [] s0=1 -> (s0'=3);
  [] s0=2 -> (s0'=3);
  [] s0=3 -> true;
endmodule

generates for Pmax=? [ F s0=3 ] a maximising scheduler 0 -> 1 -> 3, but there is also an equivalent scheduler 0 -> 2 -> 3.

Another question. When I try the shortest path method for the following DTMC:

module p
  s0 : [0..3] init 0;

  [] s0=0 -> 0.5:(s0'=1) + 0.5:(s0'=2);
  [] s0=1 -> (s0'=3);
  [] s0=2 -> (s0'=3);
  [] s0=3 -> true;
endmodule

and the property P<0.0 [ F s0=3 ], it shows only one path:

1-shortest path: 
    state 0: {init}
    state 2: {}
    state 3: {(s0 = 3)}

when there are two symmetric ones which reach a state of the reachability 1.0.

In turn, for the property P<1.0 [ F s0=3 ] it shows both of these paths:

1-shortest path: 
    state 0: {init}
    state 2: {}
    state 3: {(s0 = 3)}
2-shortest path: 
    state 0: {init}
    state 1: {}
    state 3: {(s0 = 3)}

And in case P<=1.0 [ F s0=3 ] where there is no counterexample if I understood it well, both of these paths are still printed.

[volkm]

With the workaround, the method effectively shows most probable paths within a given chosen scheduler. I wonder if it would be possible to generate multiple schedulers if they exist, so that globally most probable paths could be found.

We only support the extraction of one of the optimal schedulers. You could try to adapt the model by removing one of the choices of the exported scheduler in the model. This would give you a different scheduler. However, this requires manual work and also changes the structure of the model.

Another question. When I try the shortest path method for the following DTMC:

module p
  s0 : [0..3] init 0;

  [] s0=0 -> 0.5:(s0'=1) + 0.5:(s0'=2);
  [] s0=1 -> (s0'=3);
  [] s0=2 -> (s0'=3);
  [] s0=3 -> true;
endmodule

and the property P<0.0 [ F s0=3 ], it shows only one path:

1-shortest path: 
  state 0: {init}
  state 2: {}
  state 3: {(s0 = 3)}

when there are two symmetric ones which reach a state of the reachability 1.0.

As both paths are equally probable, we only output one of them, because one path is already enough as a counterexample.

In turn, for the property P<1.0 [ F s0=3 ] it shows both of these paths:

1-shortest path: 
  state 0: {init}
  state 2: {}
  state 3: {(s0 = 3)}
2-shortest path: 
  state 0: {init}
  state 1: {}
  state 3: {(s0 = 3)}

In this case we need both paths to get enough probability mass and therefore both paths together are a valid counterexample.

And in case P<=1.0 [ F s0=3 ] where there is no counterexample if I understood it well, both of these paths are still printed.

This was a bug and is fixed now. If the threshold cannot be exceeded an error is given.

One last suggestion: you can also export a model as a DOT file with --exportdot <filename> and use this to generate a visualization of the state space. For smaller models this might be helpful in debugging. Again, providing --buildstateval will give you the variable valuations.

[arturrataj]

As of me this issue can be closed, thanks a lot for help.