changeset 6:9b86eb10b61c

*** empty log message ***
author kono
date Fri, 19 Jan 2001 09:16:27 +0900
parents 75a40129f638
children bd06de5e669a
files infinite.pl lite.pl problems
diffstat 3 files changed, 126 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/infinite.pl	Fri Jan 19 09:16:27 2001 +0900
@@ -0,0 +1,62 @@
+/*
+ Copyright (C) 2001, Shinji Kono, University of the Ryukyus
+
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license, but changing it is not allowed.  You can also
+ use this wording to make the terms for other programs.
+
+ send your comments to kono@ie.u-ryukyu.ac.jp
+ $Header$
+
+ Infinite satisfiability/validity checker
+
+A set of non-empty-exit looping states represents infinite
+interval in ITL. The loop can contains deterministic state
+choice. This should correspond Rabin/Strreet Automaton
+that is non-deterministic Buchi automaton.
+
+The algorith works in depth first way.
+
+ */
+
+:-dynamic found_infinite/0.
+
+infinite:-
+    retract_all(found_infinite),
+    infinite(L),
+    write_infinite_seq(L).
+infinite:-
+    found_infinite,!.
+infinite:-
+    write('unsatisfiable in infinite interval.'),nl.
+
+write_infinite_seq(L) :-
+    write('satisfiable in infinite interval: '),
+    write(L),nl.
+
+retract_all(X) :-
+    retract(X),fail.
+retract_all(_).
+
+infinite([S|L]) :-
+    links(_,S),
+    more_only(S),   % search more only node
+    more_only_loop(S,S,L,[]),
+    assert(found_infinite).
+infinite([]) :-
+    found_infinite.
+
+more_only(S) :- 
+    state(S,[empty|_],true),!,fail.
+more_only(S) :- number(S).
+
+more_only_loop(S,S0,L,L1) :-
+    links(N,S),
+    more_only_loop1(N,S0,L,L1).
+
+more_only_loop1(S,S,L,L) :-!.
+more_only_loop1(N,S,[N|L],L1) :-
+    more_only(N),
+    more_only_loop(N,S,L,L1).
+
+/* end */
--- a/lite.pl	Fri Jan 19 04:25:07 2001 +0900
+++ b/lite.pl	Fri Jan 19 09:16:27 2001 +0900
@@ -4,6 +4,7 @@
 	ex/1,  			% ex(ITL)   verification predicate
 	ex/2,			% ex(No,Example)
 	diag/1,diag/0, 		% find counter example
+	infinite/1,infinite/0, 	% omega interval satisfiability
 	exe/1, exe/0,		% find sample execution
 	verbose/1, 		% verbose mode (default on)
 	renaming/1, 		% 2var renaming mode (default on)
--- a/problems	Fri Jan 19 04:25:07 2001 +0900
+++ b/problems	Fri Jan 19 09:16:27 2001 +0900
@@ -1,4 +1,66 @@
-
+Fri Jan 19 07:48:59 JST 2001
+
+Streett     ∩_i []<>L_i ⊃ <>[]U _i
+Rabin     ~(∩_i []<>L_i ⊃ <>[]U _i)
+
+という構造を持っている。これは、
+    ある無限回繰り返す所 L から先は、いつか、ずーっと U を通るようになる
+のと、その否定という構造になっている。これを、
+    labeled tree の、ある所から先は、ずーっと「あるマークがついている」ループ
+で表す。
+
+で、そのアルゴリズムだけど...
+
+depth first に「出口の無いノード」を探す。そこをマークする。そこから、
+ノードを覚えながら、出口の無いノードを手繰る。ループが出て来たら検出
+完了。最後までいったら、マークに戻り、次の出口の無いノードを探す。
+これをdepth first search が終るまで繰り返す。したがって、計算量は、
+ノード数N  に対して、最悪 N^2/2 ( N+(N-1)+(N-2)...1 ) である。それほど
+悪くは無いか。
+
+Fri Jan 19 04:27:42 JST 2001
+
+えーと、LICS のpaper は、やたら複雑だが、要は、ω-automatonの
+否定の問題だよね。だから、false loop detection が、ちゃんと、
+ITL の否定の定義に一致していることさえ見れば良い。
+
+finite interval では、既に一致しているわけだから、(true  & false )
+のsatisfiabilityの定義を無理して一致させる必要は無い。一致しなければ、
+異なるaxiomatiazation を見つけたことになる。だから、false loop 
+detection が negetation consistent ならば、たぶん、一致するんだろう。
+
+結局は、Rabin automatonのacceptabilityをチェックすることになるんだろう。
+ってことは、non deterministic buchi automaton を扱うってことか。
+
+   Rabin <-> Streett  complimentary
+
+(true & false)に関しては、<>[](not_empty) だよな。
+   infinite  -> <>[](more)
+
+ってことは... やっぱり、false_loop detection でいいんじゃないかなぁ。
+
+えーと、
+	すべてのterminating loop で、empty->true がない => infinite
+だから、ω区間で充足ってのは、
+	terminating loop に empty->trueがないものがある
+だから、ω区間で恒真ってのは、
+	terminating loop に empty->trueがない
+
+となる。その否定を取ると、true/false が逆転する。(のか?)
+
+しかし、terminating loop でなくても、ω区間を実現することはできる。
+	infinite & P -> infinite
+だから。この場合も充足っていうんだろうな。この場合は、どうせ P
+は、tableau で無視されるので問題無い。
+
+って、ことは、terminating loop だけを見ればよろしい。
+
+execution example は、
+    s s s s s s (s s s s s s)*
+という形を取る。なので、必ず最小モデルの性質を持つ。
+実際には、* の中は、非決定的で良い。
+
+
 Fri Jan 19 02:18:39 JST 2001
 
 <>empty と infinite = (true & false ) は、両立しない。