logic-rs

This library implements propositional and temporal logic in Rust. The objective is to enable both satisfaction and robustness analysis of formulas using the provided operators. The architecture is intended to be extensible in order to enable users to define custom logical operators for their own use cases.

Basic Usage

This library allows users to define logical formulas which can be evaluated in two different contexts, timed or untimed. An untimed context is a singular valuation is provided to the formula while a timed context is a series of valuations annotated with time steps. Formula elements are separated into two categories. The first category are expressions, which return values when evaluated by themselves. The second category are operators, which operate on expressions or other operators and do not return any value by themselves.

The currently provided expressions are:

• Predicates
• Propositions

The currently provided operators are (* denotes a timed-only operator):

• Not
• And
• Or
• Implies
• Next*
• Always*
• Eventually*

All expressions are defined to operate on valuations represented by hashmaps. A proposition operates on hashmaps with string keys and boolean values, while a proposition operates on hashmaps with string keys and floating point values. A proposition evaluates to true if the variable it refers to is true. A predicate is true if the weighted sum of the variables it refers to is less than its bound value. A bound value may be a constant value or another variable. Propositions and predicates cannot be used together in the same formula because they operate on different valuation types.

let proposition = Proposition::new("a");
let valuation = HashMap::from([
    ("a".to_string(), true)
]);
proposition.satisfied_by(&valuation); //True

let weight_map = HashMap::from([
    ("x".to_string(), 1.0),
    ("y".to_string(), 1.5),
]);
let predicate = Predicate::new(weight_map, Bound::Constant(10.0));
let valuation = HashMap::from([
    ("x".to_string(), 2.0),
    ("y".to_string(), 3.0),
]);
predicate.satisfied_by(&valuation); // 1.0 * 2.0 + 1.5 * 3.0 <= 10.0 => True

Binary and unary operators are constructed in the following manner:

And::new(Proposition::new("a"), Proposition::new("a"));
Not::new(Proposition::new("a"));

Timed operators also have an additional bounded constructor:

Always::new_bounded((0.0, 5.0), Proposition::new("a"));

In order to evaluate timed formulas, a trace must be constructed from an iterator of tuples that contain the time and state value.

let trace = Trace::from_iter([
    (0.0, HashMap::from([("a".to_string(), true)])),
]);

let formula = Always::new(Proposition::new("a"));
formula.satisfied_by(&trace); // True

Predicates and all operators also support the concept of robustness, which is a measure of how close a valuation or trace came to evaluating to false. These semantics can be accessed using the distance method.

let trace = Trace::from_iter([
    (0.0, HashMap::from([("a".to_string(), 9.0)])),
]);

let weights = HashMap::from([("x".to_string(), 1.0)])
let predicate = Predicate::new(weights, Bound::Constant(10.0));
let formula = Always::new(predicate);
formula.distance(&trace); // 1.0

A negative robustness value indicates that the formula was not satisfied, while a positive robustness value indicates that the formula was satisfied.

Acknowledgements

This library is built using the work done in the following papers:

• Fainekos, Georgios E., and George J. Pappas. “Robustness of Temporal Logic Specifications for Continuous-Time Signals.” Theoretical Computer Science, vol. 410, no. 42, Elsevier B.V, 2009, pp. 4262–91, https://doi.org/10.1016/j.tcs.2009.06.021.
• Nickovic, Dejan, and Tomoya Yamaguchi. RTAMT: Online Robustness Monitors from STL. 2020.