### 10 releases

0.2.2 | Dec 19, 2023 |
---|---|

0.2.0 | Sep 22, 2023 |

0.1.6 | Jul 14, 2023 |

0.1.1 | Feb 6, 2023 |

0.1.0 | Dec 22, 2022 |

#**24** in Science

**56** downloads per month

**MIT**license

200KB

3.5K
SLoC

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

## Prerequisites

To run the model checker, you will need the Rust compiler. We recommend following the instructions on rustlang.org.

If you are not familiar with Rust, there are also Python bindings for most of the important functionality in AEON.py.

## Functionality

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`]`

is a path to a file with BN model in selected format (see below,`MODEL_PATH`

is default)`aeon`

is path to a file with a set of valid HCTL formulae (one per line)`FORMULAE_PATH`

is one of`PRINT_OPTION`

/`no-print`

/`summary`

/`with-progress`

and defines the amount of information on the output (`exhaustive`

is a default mode)`summary`

is one of`MODEL_FORMAT`

/`aeon`

/`bnet`

and defines the input format (`smbl`

is default)`aeon`

For more help, use option

or `-`h

.`-- help`

### Library

This package also offers an API for utilizing the model-checking functionality.
The most relevant high-level functionality can be found in modules

and `analysis`

.
Further, useful functionality and structures regarding parsing (parser, tokenizer, syntactic trees) is in `model_checking`

module.`preprocessing`

## Model formats

The model checker takes BN models in

format as its default input, with many example models present in the `aeon`

directory.
You can also use `benchmark_models`

and `sbml`

models by specifying the format as a CLI option (see above).`bnet`

## 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

file.`benchmark_formulae .txt`

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:

(e.g.`alphanumeric characters and underscores`

)`p_1` - variables:

(e.g.`alphanumeric characters and underscores enclosed``in``"`{}`"`

)`{`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`}``:`

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

#### Wild-card properties

The library also provides functions to model check extended formulae that contain so called "wild-card propositions".
These special propositions are evaluated as an arbitrary (coloured) set given by the user.
This allows the re-use of already pre-computed results in subsequent computations.
In formulae, the syntax of these propositions is

.`%`property_name`%`

#### Dependencies

~7–16MB

~172K SLoC