search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
135 stars 74 forks source link

Support JANI's Forall and Exists Quantifiers #529

Open Philipp15b opened 4 months ago

Philipp15b commented 4 months ago

Hello! I am working on the probabilistic program deductive verifier Caesar, and I have recently added support to generate JANI files from HeyVL files, Caesar's input. The idea is to replace the recently deleted storm-pgcl. Caesar's feature is documented here. To enable model-checking probabilistic programs with infinity-wlp semantics, i.e. using the greatest fixpoint for the while loop's fixpoint iteration starting at infinity, I need to check whether there exists a path that does not reach the sink (not just with probability 1).

JANI has the Boolean quantifiers Exists and Forall, which seem ideal for this purpose. However, they are not implemented right now as far as I can tell. It would be great if Storm added support for them :)

Philipp15b commented 4 months ago

Another motivation for this would be checking for over-approximations from the --build:state limit option (in the currently unmerged PR https://github.com/moves-rwth/storm/pull/521) by checking whether unexplored states are reachable.

sjunges commented 4 months ago

So this is basically asking for (regular) CTL model checking support? 👍

Philipp15b commented 4 months ago

I’m not an expert in the JANI spec, but I’d guess that’s what it is I’m asking for :)