检查等效的CTL公式 [英] Check equivalent CTL formulas

问题描述

我正在做CTL练习，我正在尝试检查以下公式是否等效.但是我不确定我做得对吗.

I'm doing an CTL exercise, I'm trying to check if the following formulas are equivalent or not. But I'm not sure if I'm doing right.

EF (p or q) = EF(p) or EF(q) ? 
AF(p or q) = AF(p) or AF(q) ? 
A(p U ( A(q U r) )) = A(A(p U q) U r) ? 

合适的公式:等效

第二个公式:等效

第三个公式:等效

对吗? 如果错了，可以给我Kripke模型中的一个反例吗?

Is it right? If are wrong could you give me one of possible counter-examples in Kripke model?

谢谢.

推荐答案

我将尝试使用此处定义的CTL语义:有关CTL的维基百科.

I'll try to use the semantics of CTL defined here: Wikipedia about CTL.

(I) 为了证明EF (p or q) = EF(p) or EF(q):

(M, s1) |= EF (p or q)*

<=> (Def. of EF)

There is s1->s2->... such that there is an i >= 1 such that (M, s_i) |= (p or q)

<=> (Def. of or)

There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p OR ((M, s_i) |= q)

<=> (Equivalence rules for predicate logic)


(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= p)
 OR 
(There is s1->s2->... such that is an i >= 1 such that ((M, s_i) |= q)

<=> (Def. of EF)

EF(p) or EF(q)

所以等价有效.

(II)

AF(p or q) = AF(p) or AF(q)

假定具有三个状态S0，S1，S2的Kripke结构，令S0为初始状态. 在S0中，p nor q都不成立，在S1中仅p持有，在S2中仅q持有.

Assume a Kripke structure with three states S0, S1, S2, let S0 be the initial state. In S0 neither p nor q holds, in S1 only p holds, in S2 only q holds.

转换是:

S0 -> S1
S0 -> S2
S1 -> S1
S2 -> S2

S1形成一个SCC，S2形成一个SCC. AF(p或q)适用于此Kripke结构，因为(p或q)适用于S0以外的所有状态，最终每个序列都到达S1或S2. AF(p)或AF(q)呢? AF(p)不成立，因为存在序列S0 S2 S2 S2 ...，其中没有p出现. AF(q)不成立，因为存在序列S0 S1 S1 S1 ...，其中没有q出现.

S1 forms an SCC, and S2 forms an SCC. AF(p or q) holds for this Kripke structure, since (p or q) holds for ALL states except S0, and eventuelly every sequence reaches S1 or S2. What about AF(p) or AF(q)? AF(p) does NOT hold, since there is the sequence S0 S2 S2 S2 ... where no p appears. AF(q) does not hold, since there is the sequence S0 S1 S1 S1 ... where no q appears.

对于(III):请用上面的技巧进行验证:

For (III): Have fun proving it, maybe with the techniques used above :)

这篇关于检查等效的CTL公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！