#model-checking #boolean-network #symbolic #systems-biology #hctl

bin+lib biodivine-hctl-model-checker

Library for symbolic HCTL model checking on partially defined Boolean networks

3 releases

0.1.2 Apr 12, 2023
0.1.1 Feb 6, 2023
0.1.0 Dec 22, 2022

#68 in Science

MIT license

2.5K SLoC

Crates.io Api Docs Continuous integration Coverage GitHub last commit Crates.io

Symbolic model checker for logic HCTL written in RUST

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.

Model-checking tool

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 none/short/medium/full and defines the amount of information on the output (short is default)
  • 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.

Model formats

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).

HCTL formulae

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.


~120K SLoC