cpslab-asu / banquo

Offline signal temporal logic monitor written in Rust

Banquo

This repository contains the crates that make up the banquo temporal logic monitoring library. For more information, please refer to the README in the banquo crate or the documentation on docs.rs.

Structure

The banquo library is divided into multiple feature crates so that users can avoid including any functionality that they are not interested in. The banquo-core crate provides the Predicate and temporal operator definitions using the Formula trait. The banquo-hybrid_distance crate provides the HybridPredicate definition for analyzing systems that can be represented as hybrid automata. The banquo-parser crate provides the functionality to parse formulas from text.

banquo's Issues

Support Parameterized Formulas

Implement support for parameterized formulas.

A parameterized formula represents numeric values symbolically so that they can be replaced at runtime without re-writing the entire formula. Support for this functionality enables interesting use cases like parameter mining which searches for the most restrictive values of a formula that do not produce a falsification.

A parameterized formula may look like the following example: []{$a, $b} (x <= $c /\ <>{$d, $e} (y <= $f)). In this case, each variable prefixed by a dollar sign is substituted using a name => value mapping to produce a concrete formula that can be evaluated using a trace.

Create Python Bindings

Python is a widely-used language and providing to use this monitoring library will help increase the number of users. In addition, supporting python can enable this library to be shipped as a monitoring back-end for the psy-taliro toolbox.