状态机smv 线性时序逻辑(LTL) 分支时序逻辑(CTL)

2023-10-29 18:40
文章标签 逻辑 线性 时序 分支 状态机 ctl smv ltl

本文主要是介绍状态机smv 线性时序逻辑(LTL) 分支时序逻辑(CTL)，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

系统结构 smv_parser,对smv_parser的结果进行分析

突发性wet，比如水泼了

  -> State: 33.7 <-homePresentState = presentruninfan12.timer = 1runinfan27.timer = 2runinfan61.timer = 3runinalarm.timer = 3-> State: 33.8 <-homewater.waterSensor.water = wetfan.switchCap.switch = offruninfan12.timer = 0delayfan12 = 0runinfan27.timer = 1runinfan61.timer = 2runinalarm.timer = 2-> State: 33.9 <-homePresent.presenceSensor.presence = not_presenthomewater.waterSensor.water = dryfan.switchCap.switch = onhomewaterState = wetruninfan27.timer = 0delayfan27 = 0runinfan61.timer = 1runinalarm.timer = 1

对目前状态机的更改问题

实际的运行状态 ⊆ 目前的状态机
1.补全了next
2.加入了对smoke、alarm
如果不加，判断条件就不能是smoke只能是runinfan61.timer=1 & fan.switchCap.switch=on
3.case顺序调换，delay是肯定调后的，状态中runin的调后目前不确定

调换后delayfan修正了，runin虽然没修正但也正常

  -> State: 1.22 <-homePresent.presenceSensor.presence = presenthomewater.waterSensor.water = wetfan.switchCap.switch = offruninfan12.timer = 1runinfan27.timer = 0delayfan27 = 0runinfan61.timer = 2-> State: 1.23 <-homePresent.presenceSensor.presence = not_presenthomewater.waterSensor.water = dryfan.switchCap.switch = onhomePresentState = presenthomewaterState = wetruninfan12.timer = 0delayfan27 = 4runinfan61.timer = 1-> State: 1.24 <-fan.switchCap.switch = offhomePresentState = not_presenthomewaterState = dryruninfan12.timer = 4runinfan27.timer = 4runinfan61.timer = 0delayfan61 = 0

问题：hold / is true

LTL和CTL的选择问题

快是因为复杂度原因
CTL property不能用LTL替换，比如某些情况是子树，包含多个路径
EF AG这种分析包含多个路径的子树的，只能用CTL，如果最简单的ltl逻辑enough for our purpose，只用ltl就行了
在这里插入图片描述

维基上更清楚
https://en.wikipedia.org/wiki/Linear_temporal_logic#Weak_until_and_strong_release

G ((runinfan61.timer = 2 & fan.switchCap.switch = off) -> !( F (runinfan61.timer = 2 & fan.switchCap.switch = on)))

G ((runinfan61.timer = 2 & fan.switchCap.switch = off) -> F (runinfan61.timer = 1 & fan.switchCap.switch = on))，只要找到F不为(runinfan61.timer = 1 & fan.switchCap.switch = on)的就是false，并不能满足我们的需求
!(上式)会出现timer=2并且为on

G,F限制区间问题，read always followed by green or yellow
G(color.red->X(color.green 或 yellow)) ->有当前、未来一步和未来之意？

p->q等价于非p或q
φ ↔ ψ ≡ (φ → ψ) ∧ ( ψ → φ)
->和->F有区别
一个判断当前和后续，一个只判断未后续状态
!一般用于取具体的例子

!G不等于G!
G! (runinfan61.timer=2 & fan.switchCap.switch = off) 全局的每一个状态存在! (runinfan61.timer=2 & fan.switchCap.switch = off)
等价于 !F(runinfan61.timer=2 & fan.switchCap.switch = off)

AutoTap : If @raining while @ rain.off and window.open , then window.close
check_ltlspec -p “G((weather.rain=raining)->!F(window.switch=close))” 基于下一步才变

– Loop starts here
-> State: 1.1 <-
window.switch = open
weather.rain = raining
rain.config = raining
-> State: 1.2 <-
bounded model check就可以避开初始冲突

Trace Type: Counterexample
-> State: 1.1 <-
window.switch = open
weather.rain = not_raining
-> State: 1.2 <-
weather.rain = raining
– Loop starts here
-> State: 1.3 <-
weather.rain = not_raining
-> State: 1.4 <-

Trace Type: Counterexample
-> State: 3.1 <-
window.switch = open
weather.rain = not_raining
step = 1
-> State: 3.2 <-
weather.rain = raining
step = 2
-> State: 3.3 <-
window.switch = close
step = 3
– Loop starts here
-> State: 3.4 <-
window.switch = open
-> State: 3.5 <-
window.switch = close
-> State: 3.6 <-
window.switch = open

MODULE mainVARwindow.switch:{open, close, uncertain};weather.rain:{raining,not_raining};ASSIGNinit(weather.rain):=not_raining;--防止第一次,对没有TAP规则的要注意单独处理一下--init(window.switch):=close;next(window.switch):=window.switch;

5种数排列120种

MODULE mainVARwindow.switch:{open, close, uncertain};weather.rain:{raining,not_raining};step:1..3;--rain.config:{raining,not_raining};ASSIGNinit(weather.rain):=not_raining;next(weather.rain):=casestep = 2:raining;TRUE:{raining,not_raining};esac;init(step):=1;next(step):=casestep != 3: step+1;TRUE:step;esac;init(window.switch):=open;next(window.switch):=casestep = 1:open;weather.rain = raining:{open, close, uncertain};TRUE: window.switch;esac unioncasestep = 1:open;weather.rain = not_raining:{open, close, uncertain};TRUE: window.switch;esac;--check_ltlspec -p "G((weather.rain=raining)->!F(window.switch=close))"

MODULE mainVARwindow.switch:{open, close, uncertain};weather.rain:{raining,not_raining};ASSIGNinit(weather.rain):=not_raining;next(weather.rain):=caseTRUE:{raining,not_raining};esac;init(window.switch):=open;next(window.switch):=caseweather.rain = raining:close;TRUE: window.switch;esac;
MODULE mainVARwindow.switch:{open, close, uncertain};window.switch_old:{open, close, uncertain};window.certain:boolean;temperature:0..10;humidity:10..20;flag_open:0..1;flag_close:0..1;ASSIGNinit(temperature) := 5;init(humidity) := 10;init(window.switch) := close;next(window.switch):=casenext(flag_open)=1 & next(flag_close)=1:uncertain;temperature < 5: close;TRUE:window.switch;esac unioncasenext(flag_open)=1 & next(flag_close)=1:uncertain;humidity > 15 : open;TRUE:window.switch;esac;init(window.switch_old) := close;next(window.switch_old) := window.switch;init(flag_open) := 0;next(flag_open):=casetemperature < 5: 1;TRUE:0;esac;init(flag_close) := 0;next(flag_close):=casehumidity > 15: 1;TRUE:0;esac;init(window.certain) := TRUE;next(window.certain):=casenext(flag_open) = 1 & next(flag_close) = 1: FALSE;TRUE:TRUE;esac;-- check_ltlspec -p "G(window.certain=TRUE)"

该路径没有LOOPS
Trace Type: Counterexample-- Loop starts here-> State: 1.1 <-window.switch = closewindow.switch_old = closewindow.certain = TRUEtemperature = 5humidity = 10flag_open = 0flag_close = 0-> State: 1.2 <-temperature = 3humidity = 17-> State: 1.3 <-window.switch = uncertainwindow.certain = FALSEtemperature = 0humidity = 10flag_open = 1flag_close = 1-> State: 1.4 <-window.switch = closewindow.switch_old = uncertainwindow.certain = TRUEtemperature = 7humidity = 13flag_close = 0-> State: 1.5 <-window.switch_old = closetemperature = 5humidity = 10flag_open = 0

MODULE mainVARwindow.switch:{open, close, uncertain};window.switch_old:{open, close, uncertain};window.certain:boolean;temperature:0..10;t1:0..10;humidity:10..20;h1:10..20;flag_open:0..1;flag_close:0..1;step:1..3;ASSIGNinit(temperature) := 5;next(temperature):=casestep = 1: 3;TRUE:0..10;esac;init(humidity) := 10;next(humidity):=casestep = 1: 17;TRUE:10..20;esac;--等于配置初始值init(t1) := 5;--第一次变化之后保持不变，防止生成过多无效空间next(t1):=casestep = 1: 1..10;TRUE:t1;esac;    init(h1) := 15;  next(h1):=casestep = 1: 10..19;TRUE:h1;esac;   init(step):=1;next(step):=casestep != 3: step+1;TRUE:step;esac;init(window.switch) := close;next(window.switch):=casenext(flag_open)=1 & next(flag_close)=1:uncertain;temperature < t1: close;TRUE:window.switch;esac unioncasenext(flag_open)=1 & next(flag_close)=1:uncertain;humidity > h1: open;TRUE:window.switch;esac;init(window.switch_old) := close;next(window.switch_old) := window.switch;init(flag_open) := 0;next(flag_open):=casetemperature < t1: 1;TRUE:0;esac;init(flag_close) := 0;next(flag_close):=casehumidity > h1: 1;TRUE:0;esac;init(window.certain) := TRUE;next(window.certain):=casenext(flag_open) = 1 & next(flag_close) = 1: FALSE;TRUE:TRUE;esac;-- check_ltlspec -p "G(window.certain=TRUE)"

Trace Type: Counterexample-> State: 1.1 <-window.switch = closewindow.switch_old = closewindow.certain = TRUEtemperature = 5t1 = 5humidity = 10h1 = 15flag_open = 0flag_close = 0step = 1-> State: 1.2 <-temperature = 3t1 = 1humidity = 17h1 = 11step = 2-- Loop starts here-> State: 1.3 <-temperature = 0humidity = 10flag_close = 1step = 3-> State: 1.4 <-temperature = 1humidity = 12flag_open = 1flag_close = 0-> State: 1.5 <-temperature = 0humidity = 10flag_open = 0flag_close = 1

在这里插入图片描述
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述
反例
在这里插入图片描述

一、线性时序逻辑(LTL)

在这里插入图片描述

X,U是temporal operator，不指precise time
W(weak until) (ψ U φ) ∨ G ψ 多了个G ψ
F sometimes
FG infinitely often
Realse ψ R φ。φ保持为真，直到ψ变为真（包括为真的地方）。如果ψ不会为真，则φ一直为真

the syntax of LTL
之前都是看the first letter就行
X可以看the rest of word
X(X(p2))
X(p1Up2) 在下一状态，p1Up1 = true?和p1Up2的区别是起始位置不同
X(X(p1UX(p2)))

p1 until p2 ，找到p2为true的第一个地方，在那个地方前p1 is true
在这里插入图片描述
1

true每个点都满足意味着没约束，true U p1 在某个p1为true的地方
true U ¬p1 在某个p1为flase的地方
¬(true U ¬p1)意味着无法找到某个p1为flase的地方，everywhere p1 is true

∅1→∅2 如果∅1，那么∅2
在这里插入图片描述
i can’t(¬) reach F(¬∅) sometime
G§:p is True in every state

在这里插入图片描述

每处F(∅)为true
在这里插入图片描述

在这里插入图片描述

LTL本身的定义和在状态机中的体现

在这里插入图片描述
AP-INF是所有可能，property ∅是AP-INF的一个子集，Words(∅):AP-INF中满足∅的words

在这里插入图片描述
一个是对符号的拆分一个是satisfy ∅，对复杂的直接把∅替换为一坨
在这里插入图片描述
words(∅) = σ

在这里插入图片描述
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述

狼羊过河问题

planning problem:find a path to the goal state
在这里插入图片描述
在这里插入图片描述
check !∅，如果有反例是满足∅的

MODULE main
VARman:boolean;goat:boolean;wolf:boolean;cabbage:boolean;carry:{g,w,c,0};
ASSIGNinit(man) := FALSE;init(goat) := FALSE;init(wolf) := FALSE;init(cabbage) := FALSE;init(carry) := 0;--man要么在左边要么在右边next(man) := {TRUE,FALSE};--man和其它同值则可以搬运，且一次可以搬运的选项是非确定性(non-deterministic),esac union 提供了next value的non-deterministic choice-- carry并不是实际的，只是提供了一种选项（choose to do），因为可以呆在原地不变next(carry) :=  caseman = goat:g;-- 确保condition exhaustedTRUE:carry;esac unioncaseman = wolf:w;TRUE:carry;esac unioncaseman = cabbage:c;TRUE:carry;esac union 0;next(goat):= 	case-- 如果goat被carry，那么反置值表示达到另一岸--next(carry) = g:!goat;-- carry = goat但man可能呆在同一岸，随着人的位置而变化next(carry) = g:next(man);TRUE:goat;esacnext(wolf):=next(cabbage):=nextLTLSPEC
!( ((goat = cabbage | goat = wolf)->man = goat) U (man & cabbage & goat & wolf) )

nusmv test.smv

trace相关的p94 - 100

4个变量和转化为可达性问题（全0到全1）

在这里插入图片描述

二、分支时序逻辑(CTL)

每个node可以是{p1}{p2}{p1,p2}，如switch=ff & present = off

LTL讨论path的property
CTL讨论tree的property，一个状态机可以表示为一颗树，初始状态是根节点

E

红点并不是node，而是该node有对应的ap
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述

在这里插入图片描述

A

在这里插入图片描述
在这里插入图片描述
在这里插入图片描述

在这里插入图片描述
两个符号E代表Exist，Exist a path 满足∅，A代表all path满足∅，E(F(A(G(∅))))，某个子树满足A(∅)

E mix with A

在这里插入图片描述

在这里插入图片描述
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述
在这里插入图片描述

CTL*

state formulae
path formulae
在这里插入图片描述

LTL CTL* CTL的关系

如果系统满足LTL，则对应的树满足A(∅)，LTL属于CTL的一部分
CTL property不能用LTL替换，比如某些情况是子树，包含多个路径
LTL不能用CTL实现，CTL也不能用LTL实现
在这里插入图片描述
如果最简单的ltl逻辑enough for our purpose，只用ltl就行了

CTL是CTL*限制后的

LTL CTL*的转换

如果G (runinfan61.timer=2 & fan.switchCap.switch = off)，如果等于初始0，找到反例并不能说明冲突存在
–LTLSPEC G! (runinfan61.timer=2 & fan.switchCap.switch = off)
如果找到反例则说明这种情况存在

这篇关于状态机smv 线性时序逻辑(LTL) 分支时序逻辑(CTL)的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！


http://www.chinasem.cn/article/302597。

相关文章

线性因子模型 - 独立分量分析（ICA）篇

线性因子模型 - 独立分量分析（ICA）篇

序言 线性因子模型是数据分析与机器学习中的一类重要模型，它们通过引入潜变量（ latent variables \text{latent variables} latent variables）来更好地表征数据。其中，独立分量分析（ ICA \text{ICA} ICA）作为线性因子模型的一种，以其独特的视角和广泛的应用领域而备受关注。 ICA \text{ICA} ICA旨在将观察到的复杂信号
阅读更多...
✨机器学习笔记（二）—— 线性回归、代价函数、梯度下降

✨机器学习笔记（二）—— 线性回归、代价函数、梯度下降

1️⃣线性回归（linear regression） f w , b ( x ) = w x + b f_{w,b}(x) = wx + b fw,b​(x)=wx+b 🎈A linear regression model predicting house prices： 如图是机器学习通过监督学习运用线性回归模型来预测房价的例子，当房屋大小为1250 f e e t 2 feet^
阅读更多...
【高等代数笔记】线性空间（一到四）

【高等代数笔记】线性空间（一到四）

3. 线性空间 令 K n : = { ( a 1 , a 2 , . . . , a n ) ∣ a i ∈ K , i = 1 , 2 , . . . , n } \textbf{K}^{n}:=\{(a_{1},a_{2},...,a_{n})|a_{i}\in\textbf{K},i=1,2,...,n\} Kn:={(a1​,a2​,...,an​)∣ai​∈K,i=1,2,...,n
阅读更多...
逻辑表达式，最小项

逻辑表达式，最小项

目录 得到此图的逻辑电路 1.画出它的真值表 2.根据真值表写出逻辑式 3.画逻辑图 逻辑函数的表示 逻辑表达式 最小项 定义 基本性质 最小项编号 最小项表达式   得到此图的逻辑电路 1.画出它的真值表 这是同或的逻辑式。 2.根据真值表写出逻辑式   3.画逻辑图   有两种画法，1是根据运算优先级非>与>或得到，第二种是采
阅读更多...
UMI复现代码运行逻辑全流程（一）——eval_real.py（尚在更新）

UMI复现代码运行逻辑全流程（一）——eval_real.py（尚在更新）

一、文件夹功能解析 全文件夹如下 其中，核心文件作用为： diffusion_policy：扩散策略核心文件夹，包含了众多模型及基础库 example：标定及配置文件 scripts/scripts_real：测试脚本文件，区别在于前者倾向于单体运行，后者为整体运行 scripts_slam_pipeline：orb_slam3运行全部文件 umi：核心交互文件夹，作用在于构建真
阅读更多...
带头结点的线性链表的基本操作

带头结点的线性链表的基本操作

持续了好久，终于有了这篇博客，链表的操作需要借助图像模型进行反复学习，这里尽可能的整理并记录下自己的思考，以备后面复习，和大家分享。需要说明的是，我们从实际应用角度出发重新定义了线性表。 一. 定义 从上一篇文章可以看到，由于链表在空间的合理利用上和插入、删除时不需要移动等优点，因此在很多场合下，它是线性表的首选存储结构。然而，它也存在某些实现的缺点，如求线性表的长度时不如顺序存储结构的
阅读更多...
浙大数据结构：02-线性结构4 Pop Sequence

浙大数据结构：02-线性结构4 Pop Sequence

这道题我们采用数组来模拟堆栈和队列。 简单说一下大致思路，我们用栈来存1234.....，队列来存输入的一组数据，栈与队列进行匹配，相同就pop 机翻 1、条件准备 stk是栈，que是队列。 tt指向的是栈中下标，front指向队头，rear指向队尾。 初始化栈顶为0，队头为0，队尾为-1 #include<iostream>using namespace std;#defi
阅读更多...
深度学习与大模型第3课：线性回归模型的构建与训练

深度学习与大模型第3课：线性回归模型的构建与训练

文章目录 使用Python实现线性回归：从基础到scikit-learn1. 环境准备2. 数据准备和可视化3. 使用numpy实现线性回归4. 使用模型进行预测5. 可视化预测结果6. 使用scikit-learn实现线性回归7. 梯度下降法8. 随机梯度下降和小批量梯度下降9. 比较不同的梯度下降方法总结 使用Python实现线性回归：从基础到scikit-learn 线性
阅读更多...
C#中的各种画刷， PathGradientBrush、线性渐变（LinearGradientBrush）和径向渐变的区别

C#中的各种画刷， PathGradientBrush、线性渐变（LinearGradientBrush）和径向渐变的区别

在C#中，画刷（Brush）是用来填充图形（如形状或文本）内部区域的对象。在.NET框架中，画刷是System.Drawing命名空间的一部分，通常用于GDI+绘图操作。以下是一些常用的画刷类型： SolidBrush：用于创建单色填充的画刷。HatchBrush：用于创建具有图案填充的画刷。TextureBrush：用于创建具有图像纹理填充的画刷。LinearGradientBrush：用于创
阅读更多...
(感知机-Perceptron)—有监督学习方法、非概率模型、判别模型、线性模型、参数化模型、批量学习、核方法

(感知机-Perceptron)—有监督学习方法、非概率模型、判别模型、线性模型、参数化模型、批量学习、核方法

定义 假设输入空间（特征空间）是 χ \chi χ ⊆ R n \subseteq R^n ⊆Rn,输出空间是y = { + 1 , − 1 } =\{+1,-1 \} ={+1,−1} 。输入 x ∈ χ x \in \chi x∈χ表示实例的特征向量，对应于输入空间（特征空间）的点；输出 y ∈ y \in y∈y表示实例的类别。由输入空间到输出空间的如下函数： f ( x ) = s
阅读更多...

Copyright China编程 23002807@qq.com

沪ICP备2023033072号-2