OmegaHyper

OmegaHyper is an explicit-state model checker for HyperLTL over NuSMV models. It takes one model per trace variable (or one model for all of them) and a HyperLTL formula, and answers whether the formula holds, with a witness or counterexample over the models' variables on request. It is a fork of AutoHyper, keeping most of its command line, input formats and core algorithm. Its pipeline is described in ARCHITECTURE.md, and notes for developers can be found in EXTENDING.md.

Usage

$ OmegaHyper [options] <system> ... <system> <formula>

One system file per trace variable of the formula, in the order of the quantifier prefix, or a single file for all of them, followed by the formula file. OmegaHyper --help lists the options. The last line of the output is SAT (the formula holds) or UNSAT. With --witness, witness traces are given for all systems in the outermost block. Each witness is one lasso over states, defined as a prefix and a loop of states written {"x":1, "y":true}.

Examples

Consider the CNI benchmark, that checks conditional noninterference of a three-bit PIN checker (forall A. exists B.: under fair scheduling, every trace has a counterpart with a different PIN and the same observable result once the masks are cleared).

On a model that admits an arbitrary PIN:

$ OmegaHyper benchmarks/HyperLasso/CNI/cni_any_3.smv benchmarks/HyperLasso/CNI/cni_3.ah --witness
======= Witnesses =======
A: ({"MASK_0":false, "MASK_1":true, "MASK_2":false, "RESULT_0":false, "RESULT_1":false, "RESULT_2":false, "pc_0":0, "pc_1":0, "pc_2":0, "trigger_0":false, "trigger_1":false, "trigger_2":0, "PIN_0":true, "PIN_1":false, "PIN_2":false, "turn":1} ...) ({...} {...} {...})
=========================
UNSAT

The formula is false, and OmegaHyper has found a trace A that has no counterpart with another PIN and the same result.

On another model whose initial condition constraints the PIN by the mask:

$ OmegaHyper benchmarks/HyperLasso/CNI/cni_lte_3.smv benchmarks/HyperLasso/CNI/cni_3.ah --witness
SAT

The formula is true, so there is no witness to print.

Input formats

Formula

A formula is a quantifier prefix followed by an LTL body with Boolean expressions over the model variables of the quantified traces, such as:

forall A. exists B. G ("x"_A > "x"_B + 1) & G F "y"_B

Boolean subexpressions may be marked in braces, { "x"_A > "x"_B + 1 }, to make each mark one atomic proposition (AP), as AutoHyper requires. OmegaHyper infers APs itself, so braces are optional; no user-marked AP is unfolded.

As in AutoHyper, formulas may be in HyperQPTL, whose prefix also quantifies over propositions bound to no model.

Models

Models are NuSMV modules (--nusmv, by default): one MODULE over Boolean, integer-range and enumerated variables, with VAR and FROZENVAR declarations, ASSIGN, INIT, TRANS, INVAR, DEFINE and specifications or fairness constraints. AutoHyper's explicit-state systems (--explicit) and Boolean programs (--bp) are also accepted.

Benchmarks

In the folder benchmarks you can find three benchmarks suites, inherented from other tools, along with their detailed description.

Docker

The image hugopacheco/omegahyper:latest (:arm64 and :amd64) holds OmegaHyper, every backend, other HyperLTL model checkers for comparative evaluation and the benchmarks. To launch the image, run:

docker pull hugopacheco/omegahyper:latest
docker run --rm -it hugopacheco/omegahyper:latest

The shell opens in /OmegaHyper/benchmarks, laid out as this repository. When you run the benchmarks, reports and logs will land in image's the working directory. To persist those in your host machine, bind your local directory instead:

docker run --rm -it -v "$PWD/benchmarks:/OmegaHyper/benchmarks" hugopacheco/omegahyper:latest

Build

Dependencies:

• the .NET 9 SDK (tested with 9.0.318);
• spot 2.12 or later (tested with 2.16);
• our own fork of kofola, as the submodule app/kofola;
• optionally, the .jar files of RABIT, BAIT, FORKLIFT and ROLL, for the alternative inclusion backends.

First clone and build kofola:

git submodule update --init
cd app/kofola && cmake -B build -DBUILD_TESTS=OFF && cmake --build build && cd ../..

Then build OmegaHyper into app/:

cd src && dotnet build -c release -o ../app && cd ..
app/OmegaHyper --version

app/paths.json, next to the executable, names the tools (absolute paths; the optional ones may be left out):

{
    "autfilt": "<path>/autfilt",
    "ltl2tgba": "<path>/ltl2tgba",
    "ltlfilt": "<path>/ltlfilt",
    "kofola": "<repo>/app/kofola/build/src/kofola",
    "rabit": "<path>/RABIT.jar",
    "bait": "<path>/bait.jar",
    "forklift": "<path>/forklift.jar",
    "roll": "<path>/ROLL.jar"
}

References

[1] OmegaHyper: Explicit-State HyperLTL Model Checking on an ω-Automaton Diet. Hugo Pacheco.