This repository contains the Rust implementation of the symbolic model checker for hybrid logic HCTL. The method is focused on the analysis of (partially specified) Boolean networks. In particular, it allows to check for any behavioural hypotheses expressible in HCTL on large, non-trivial networks. This includes properties like stability, bi-stability, attractors, or oscillatory behaviour.
To run the model checker, you will need the Rust compiler. We recommend following the instructions on rustlang.org.
This repository encompasses the CLI model-checking tool, and the model-checking library.
Given a (partially defined) Boolean network and HCTL formulae (encoding properties we want to check), the tool computes all the states of the network (and corresponding parametrizations) that satisfy the formula. Currently, there is only a command-line interface, with a GUI soon to be implemented. Depending on the mode, the program can either print the numbers of satisfying states and colours, or print all the satisfying assignments.
To directly invoke the model checker, compile the code using
cargo build --release
and then run the binary:
.\target\release\hctl-model-checker <MODEL_PATH> <FORMULAE_PATH> [-m <MODEL_FORMAT>] [-p <PRINT_OPTION>] [-h]
MODEL_PATH is a path to a file with BN model in selected format (see below, aeon is default)FORMULAE_PATH is path to a file with a set of valid HCTL formulae (one per line)PRINT_OPTION is one of no-print/summary/with-progress/exhaustive and defines the amount of information on the output (summary is a default mode)MODEL_FORMAT is one of aeon/bnet/smbl and defines the input format (aeon is default)For more help, use option -h or --help.
This package also offers an API for utilizing the model-checking functionality.
The most relevant high-level functionality can be found in modules analysis and model_checking.
Further, useful functionality and structures regarding parsing (parser, tokenizer, syntactic trees) is in preprocessing module.
The model checker takes BN models in aeon format as its default input, with many example models present in the benchmark_models directory.
You can also use sbml and bnet models by specifying the format as a CLI option (see above).
All formulae used must not contain free variables. In the input file, there has to be one formula in a correct format per line.
Several interesting formulae are listed in the benchmark_formulae.txt file.
To create custom formulae, you can use any HCTL operators and many derived ones.
We use the following syntax:
* constants: true/True/1, false/False/0
* propositions: alphanumeric characters and underscores (e.g. p_1)
* variables: alphanumeric characters and underscores enclosed in "{}" (e.g. {x_1})
* negation: ~
* boolean binary operators: &, |, =>, <=>, ^
* temporal unary operators: AX, EX, AF, EF, AG, EG
* temporal binary operators: AU, EU, AW, EW
* hybrid operators
* bind x: !{x}:
* jump x: @{x}:
* exists x: 3{x}:
* forall x: V{x}:
* parentheses: (, )
The operator precedence is following (the lower, the stronger): * unary operators (negation + temporal): 1 * binary temporal operators: 2 * boolean binary operators: and=3, xor=4, or=5, imp=6, eq=7 * hybrid operators: 8
However, it is strongly recommended to use parentheses wherever possible to prevent any parsing issues.