Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 mm1
Verification 3
Subject:
LTL, Büchi Automata
Litterature:
JK: 2.1, 2.2, 2.5-2.9 (you may
choose only to skim 2.8)
Excercises.
Exercise 1
Construct Büchi
automata accepting precisely the set of infinite computations satisfying
the formulas Gp (invariantly p), Fp (eventually
p)
and (G ((p) -> (F(q))) as well as their complement. Here p
and q are atomic propositions.
Exercise 2
Prove or disprove the equivalence of the formulas
(Fp) U (Fq) and F(p U q)
Prove or disprove equivalence of the formulas
G(p=>Xp) and G(p=>Gp)