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

• Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

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.