logic-rs

此库在Rust中实现了命题逻辑和时序逻辑。目标是使用提供的运算符实现对公式的满足性和鲁棒性分析。该架构旨在可扩展，以便用户可以为他们的用例定义自定义逻辑运算符。

基本用法

此库允许用户定义逻辑公式，这些公式可以在两种不同的环境中进行评估，即定时或不定时。不定时环境向公式提供单一的估值，而定时环境是带有时步注释的估值序列。公式元素分为两个类别。第一类是表达式，当单独评估时返回值。第二类是运算符，它们在表达式或其他运算符上操作，本身不返回任何值。

目前提供的表达式有

• 谓词
• 命题

目前提供的运算符有 (* 表示仅定时运算符)

• 非
• 与
• 或
• 蕴含
• 下一个*
• 总是*
• 最终*

所有表达式都定义为在由哈希表表示的估值上操作。命题在具有字符串键和布尔值的哈希表上操作，而命题在具有字符串键和浮点值的哈希表上操作。如果所引用的变量为真，则命题评估为真。如果所引用的变量的加权总和小于其界限值，则谓词为真。界限值可能是一个常量值或另一个变量。由于命题和谓词在估值类型上操作不同，因此它们 不能 在同一公式中使用。

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

二元和一元运算符按以下方式构建

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

定时运算符还有一个额外的界限构造函数

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

为了评估定时公式，必须从包含时间和状态值的元组的迭代器构建一个跟踪。

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

谓词和所有运算符还支持鲁棒性的概念，这是衡量估值或跟踪接近评估为假的程度。可以使用 distance 方法访问这些语义。

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

负鲁棒性值表示公式未满足，而正鲁棒性值表示公式已满足。

致谢

此库基于以下论文的工作构建

• 法因科斯，乔治·E，和乔治·J·帕帕斯。“连续时间信号的时序逻辑规范鲁棒性。”理论计算机科学，第410卷，第42期，Elsevier B.V，2009年，第4262-91页，https://doi.org/10.1016/j.tcs.2009.06.021。
• 尼科维奇，德扬，和山口智也。“RTAMT：从STL在线鲁棒性监控。”2020年。