1 unstable release

Uses new Rust 2021

0.1.0 Sep 17, 2022

#19 in #logic

MIT/Apache

56KB
1.5K SLoC

telo - Specifying temporal properties in Rust

With telo, you can specify temporal properties using linear-time temporal logic (LTL). Those specifications can be transformed into monitoring automata, which can detect violations of safety specifications during runtime.

How-to: Runtime monitoring

use telo::{*, predicate::*, monitor::*};

// Step 1: define predicates
const LIMIT: i32 = 123;

let mut builder = Predicates::builder();
let above_limit = builder.new_predicate(ClosurePredicate::new(
    |val: &i32| *val >= LIMIT,
     "value is above LIMIT",
));
let predicates = builder.build();

// Step 2: define temporal specification
let property = Property::never(Property::atomic(above_limit));

// Step 3: transform to monitoring automaton
let automaton = property.to_monitoring_automaton(&predicates);

// Step 4: runtime monitoring
let mut monitor = Monitor::new(predicates, automaton);
for value in 0..LIMIT {
  assert!(monitor.next_state(&value));
}
assert!(!monitor.next_state(&LIMIT)); // the property is violated

From LTL to minimal and deterministic safety automata

  • LTL over an arbitrary domain using self-defined predicates
  • Translation to LTL in negation normal form
  • Translation to alternating-time Büchi automaton
  • Translation to non-deterministic Büchi automaton (via Miyano-Hayashi construction)
  • Re-interpretation as non-deterministic safety automaton
  • Determinize and minimize safety automaton

License

Licensed under either of

at your option.

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Dependencies

~3MB
~68K SLoC