# HG changeset patch # User kono # Date 979863387 -32400 # Node ID 9b86eb10b61cb4be3b0b7cfd9f943964e98db5a2 # Parent 75a40129f638f4b5ed9384197451aae86744a39f *** empty log message *** diff -r 75a40129f638 -r 9b86eb10b61c infinite.pl --- /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 */ diff -r 75a40129f638 -r 9b86eb10b61c lite.pl --- 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) diff -r 75a40129f638 -r 9b86eb10b61c problems --- 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 ) は、両立しない。