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

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

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

let mut builder = Predicates::builder(); let abovelimit = builder.newpredicate(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.tomonitoringautomaton(&predicates);

// Step 4: runtime monitoring let mut monitor = Monitor::new(predicates, automaton); for value in 0..LIMIT { assert!(monitor.nextstate(&value)); } assert!(!monitor.nextstate(&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.