x******t
发帖数: 6 | 1 a, b中间可以插入别的字母，比如 a c d b d a b, 但删去非a,b的字符后
串形如(ab)*
不太清楚LTL跟正则表达式之间的关系……求教~ |
s*x
发帖数: 3328 | 2 不行，表达不出来这种一个间隔一个的pattern
【在 x******t 的大作中提到】
: a, b中间可以插入别的字母，比如 a c d b d a b, 但删去非a,b的字符后
: 串形如(ab)*
: 不太清楚LTL跟正则表达式之间的关系……求教~
|
x******t
发帖数: 6 | 3 smallx同学...没想到在这里也能发现你的身影，呵呵
【在 s*x 的大作中提到】
: 不行，表达不出来这种一个间隔一个的pattern
|
x******t
发帖数: 6 | 4 response(a, b):= G(a => F(b))
precedence(a, b):= F(b) => (!b U a)
always_between(a,b):= G( b => X (precedence(a, b) )
(ab)* := precedence(a,b) && response(a,b) && always_between(b,a) && always_
between(a,b)
这样写错在哪里呢……
【在 s*x 的大作中提到】
: 不行，表达不出来这种一个间隔一个的pattern
|
s*x
发帖数: 3328 | 5 嘿嘿
【在 x******t 的大作中提到】
: smallx同学...没想到在这里也能发现你的身影，呵呵
|
s*x
发帖数: 3328 | 6 (aab)* 也满足吧，类似的(abb)*，甚至随便一个abbabaabbaababbabaababbaabbabaab.
..都可以满足。你说的四个条件都满足。
【在 x******t 的大作中提到】
: response(a, b):= G(a => F(b))
: precedence(a, b):= F(b) => (!b U a)
: always_between(a,b):= G( b => X (precedence(a, b) )
: (ab)* := precedence(a,b) && response(a,b) && always_between(b,a) && always_
: between(a,b)
: 这样写错在哪里呢……
|
x******t
发帖数: 6 | 7 (abb)*不满足always_between(a,b)啊~
根据always_between，因为第二个字符是b，所以从第三个位置开始的b(abb)*应满足
precedence(a,b)。
显然F(b)成立，根据precedence，b(abb)*应满足!b U a，但第一个字符是b，所以不满
足……
(aab)*的推理类似。
abbabaabbaababbabaababbaabbabaab.
【在 s*x 的大作中提到】
: (aab)* 也满足吧，类似的(abb)*，甚至随便一个abbabaabbaababbabaababbaabbabaab.
: ..都可以满足。你说的四个条件都满足。
|
s*x
发帖数: 3328 | 8 oh~~好久没用，你说的有道理，这么看来LTL确实和正则语言有点关系。
【在 x******t 的大作中提到】
: (abb)*不满足always_between(a,b)啊~
: 根据always_between，因为第二个字符是b，所以从第三个位置开始的b(abb)*应满足
: precedence(a,b)。
: 显然F(b)成立，根据precedence，b(abb)*应满足!b U a，但第一个字符是b，所以不满
: 足……
: (aab)*的推理类似。
:
: abbabaabbaababbabaababbaabbabaab.
|
s*x
发帖数: 3328 | 9 LTL表达式表达的应该都可以用正则表达式表达，考虑LTL的等价FM的等价正则表达式就
可以了，反过来，应该可以有LTL表达不了的正则语言。
【在 s*x 的大作中提到】
: oh~~好久没用，你说的有道理，这么看来LTL确实和正则语言有点关系。
|
x******t
发帖数: 6 | 10 查了篇文章Loop-Free Alternating Finite Automata，清楚了。
LTL的表达能力与star-free regular expression相同。所谓的“star-free的regexp语
言”虽然不含有*，却包含negation和intersection，因此它可以表达某些无限长的串。
【在 s*x 的大作中提到】
: LTL表达式表达的应该都可以用正则表达式表达，考虑LTL的等价FM的等价正则表达式就
: 可以了，反过来，应该可以有LTL表达不了的正则语言。
|
