Fri Jan 19 20:59:46 JST 2001 | ?- ex((infinite -> @infinite)). state(1 , not(true&false),@ (true&false)) [][empty]->empty [][more]->true 0.021000000000000796 sec. 1 states 2 subterms 2 state transions verbose,renaming,singleton,length limit 5 valid yes | ?- infinite. unsatisfiable in infinite interval. これは... どういうことなんでしょうね? inifite は基本的に false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable だね。 Fri Jan 19 20:40:37 JST 2001 割りと簡単なアルゴリズムで、satisfiabilityは、チェック できました。これが、正しいかどうかは Moszkowski によるけど... inifnite *skip *((skip&skip)) などに関しては、うまく動くようですね。 vailidity checker が欲しい所だけど... どういうものがvalidなのかは、 良くわからない。もちろん、否定が unsatisfiable ならば、valid なの だが。 でも、この方法だと、 satisfiable in ω-interval implies falsifiable in finite interval ってことになるらしい。 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 ) は、両立しない。 <>empty = finite & empty = ~(true & false) & empty ~(true & false ) はなにを示しているかと言うと... いつでも「終れる」ということ。infinite は、「終れない」 ω区間には、empty exit は存在できない。正確には、 ... [ no-empty loop ] .... ということ。そういうsub 区間があれば良い。 [](more) は? もちろん、これは、Lite では、false. ~(finite & ~more) ~(~(true & false) & ~more)) ~(~(true & false) & empty)) これが ω区間で true になるためには... []のinifinite versionは? http://research.commpaq.com/SRC/esc/ Fri Jan 19 01:20:54 JST 2001 ω区間は、必ず、(s_n...s_m)* を含む。decidableならば、そうだ。 が、それは、証明が必要がだけど。 逆に、(s_n...s_m)* を含めば、そこをずーっと繰り返すことにより、 ω区間を実装できる。だから、そういうループを見つければ、 ω区間上で satisfiable だということができる。 その区間上で、∨empty のようなexitが許されるのか? たぶん、 許されない。ということは、やはり、false loop を見つければ 良いと言うことか。 そのアルゴリズムは? ω区間では、empty で抜け出ることができない。-> <>empty がfalse どうも正しそうだな。 えーと、何か、安全なアルゴリズムがありそうだけど... 簡単なのは、すべてのループをdepth first で探すことだな。 とすると、finitarity をチェックするのは結構面倒になる。 finitarity とはなに? ループには必ずtrue exitがある infiniteness とは、 exit のないループがある []<>(p) = <>[](p) は、どうなるんだろう? <>(p) = finite & p ~(finite & ~(finite & p)) = finite & ~(finite & ~p) ですか。 Fri Jan 19 00:33:43 JST 2001 えーと、 [](false) がsatisfiableになることはない。 ~(true & ~ false) ~(true & true) だから。 true & ~true は、許される。しかし、 ~true & ~true は許されない。これ自体は、今のverifier でも、そうなる。 tableau expansion 自体は同じだと考えて良いのか? 特に異なる inference rule があるわけではないらしい。 だとすれば、必要なコードは、false loop detector だけか? exe/diag の代りに、infinite_exe,infinite_diag を作るのだろうか。 infinite_exe は、ループを表示しなければならない。必ず、 そのようなループが存在するのだろうか? とすると、infinite interval は、prefix のようなものになる。実は、prefix がinfinite interval そのもの? prefix(finite,....) みたいなものだね。これは、どっかで見たことが... Thu Jan 18 22:42:24 JST 2001 | ?- ex(((true&false)->(<>(empty)))). は、valid になってしまう。実際には、infinite->not(<>(empty)). Thu Jan 18 21:04:13 JST 2001 まず、chop.pl の中の、X & false をfalseに変換しているのを 抜く必要がある。 Thu Jan 18 19:59:33 JST 2001 in POPL01 LICS00 の infinite を入れるように Lite を拡張することが できるのか? 単純な拡張にはならない。 infinite =def (true & false ) だから。これは、今の実装では unsatisfiable。 P&Q で、Q が単純にfalseだからといって、諦められない。今は、node は、 empty,false empty,true more,false more,some_other というように特徴付けられている。これで足りるのか? Eventurality check が必要無いと良いんだけど。 Rabin automaton ってなんだ? Buchi と同じなんじゃないの? true & false は、 empy -> false more -> true & false に展開される。今は、empty だけを見て、validity/satisfiability を 調べている。しかし、これを、 「ある特定のfalse exit ループをsatisfiableだとみなす」 ことにより、infinite interval を導入することができる。 問題は、どのような false exit ループが satisfiable だという こと? というよりは、これで unsatisfiable になる formulaって 何? more -> false のたぐいだけか? finite empy -> true more -> true & true は、どうなる? ~infinite empy -> true more -> ~(true & false) となる。なので、これは finite に等しい。 infinite は、false loop を表していると考える。 全ての式Pを、finite -> P で、チェックすれば、finite LITL になる。 (ならなければいけない) って、ことは、false loop をdetectすれば良いだけか? これは、 結構易しいが、計算量的には、ちょっと大変かな。 finitely valid, satisfiable, unsatisfiable... inifinitly valid, satisfiable... infinitely satisfiable とは、 flase loop が存在すること valid は、 false loop 以外は、empty false であること(?) えーと、それだと、inifinitly satisiable な式は、finitly unsatisfiable だけど、それでいいの? だとすると、valid な式はなくなってしまうね。 これは、ちょっとうれしくないであろう。ということは、 infinitely valid は、 false loop 以外は、empty ture であること(?) を含むと考えるのが正しい。だとすると、 |= finitie /\ finite ってことになるね。それは、ちょっとうれしくないか。 うーむ、Moszkowski は、どういう選択をしたんだろう? Wed Nov 22 16:27:45 JST 1995 rstd 側で limit を扱うことにする。 rename_list でlimitを指定することになる。singleton のlimit をはずさないといけないだろう。over(r,N)が外にでないのが ちょっと情報不足だな。 itlstd が idempotent になってなーい!!! しくしく。 itlstd(X,Y,_),bdt2itl(Y,Z),itlstd(Z,Y1,_) でY=Y1になる はずなのだが... itlstd2 では、singleton remove, renaming は行なわないで、limit over だけを取り扱う。これによってdetailed trace が可能となる。これに、 従来のitlstdをかければ、もとに戻るはずだ。が、どうも失敗している らしい。 Tue Nov 21 18:33:19 JST 1995 renaming の trace は original limit で行なう。 detailed trace は no limit で行なう。 itl/5 は2度呼ばれるが、まあ、良とするか。 rstd 側でlimitの置き換えをすればだいぶましなんだが... renmaing で、over limit を取り扱う方が統一的か。 Wed Nov 15 12:58:28 JST 1995 over(r,N) が true/false に置き換わっていて、unifyするか? いずれにせよ、ちょっと気まずい。どの変数が置き換わるかは、 renaming を trace すれば分かるが... この置き換えをrstd側で行なって、original/restrictedの両方を とっておく。そして、どの変数が置き換わったか分かるようにする。 (renaming informationに入れておく) でも、この情報もどうせ lazyに生成するんだよね? なんか変だ。 あるいは、detailed traceの方では置換えしない? true/false に 置き換えても同じstateで実現できるはず。だが、unify はしないと いけない。 いずれにせよ、lazy state generation では、 full trace, restricted trace の両方をおこなう。このためには、over の置き換えをrstd で行なった 方が良いだろう。 うーむ、でも、そうすると、itlstd がnon-deterministic になって しまう。それは、いまいちだ。 Tue Nov 14 19:56:26 JST 1995 Detailed trace の時は Fromula と state number と両方持ち歩かないと だめだ。 ということは、diag routine を書き直さないとダメか。ndcomp は あきらめるか? Mon Nov 13 22:33:34 JST 1995 trace するときにrenaming は、いらないんじゃない? detailed traceをどうせ使うとすれば... そうすれば、 choice も考えなくても良い。 Sun Nov 12 23:37:36 JST 1995 ^r のtrace stateは決まっている duplicated は rename inforamtion を使ってtrace できる。 detailed expansion して、unify する。具体的には、 BDDにそって分解する。これによって、true_false がr^nの treeに展開されるはず。されなければ、別のものを探す。 true_falseのchoiceによって値が異なるわけだけど...? choice は、一つのBDDに関して一つしかでない。(leafにしかない から) ということは、複数のchoice は、 異なる & の empty でしか起きない。なんらかのidentityを残した方がいいんだけど。 ま、結果的に同じstateにいって、すべての条件が尽くされるなら、 構わないか。detailed expansion はすべてを含んでいるのだから、 構わないはず。 まずは、renaming のカタをつけよう。 もっと選択的に^rをトレースした方が良くない? singleton ^r をなんらかのtermにマップできなものか? Sat Nov 11 09:55:41 JST 1995 2path singleton removal がようやっとできた。 ただし、どうも、order sensitive なんだよな。over が@<,@>に よってでる時とでない時がある。 sbdt_split, sbdt_ife によってremoval/renameによるorderを修正しない といけなかった。やむをえないところか? しかしsingleton removalを書いたら、もとの方も良くなってしまった。 どうも、bdt routineには問題があったみたい。true & true を除く ようにしたのが効いたとも思えないんだが.... sbdt_opt のせいか? state numberがでなくなるbugを直した あとは、trace の問題だな。r^nの実行がちゃんとトレースできると いいんだけど。 Thu Nov 9 12:03:32 JST 1995 P & Q を、sb(P_BDD & Q_BDD) という形で持っているけど.. sb(P_BDD,PN) sb(Q_BDD,QN) PN & QN という方が良くない? ほとんど同じだとは思うけど.... ?(PN & QN,true,false) となるのか.... うーん。 Qの展開を一回に抑えられない? ? を未展開のマークに 使えないか? Wed Nov 8 20:31:23 JST 1995 はやり一旦BDDに落して2pathで処理することとする。 first path: singleton varble の detect (regular variableがない場合は、そのままstd_check singleton removal で消えることはない) regular variable が無ければ、これで終了 rename list を計算 second path path: singleton variable があった場合、 t/fのtree を parallel traverse t/f または、[tf]/tf の組合せをtfに置き換える 複数のsingleton variableを順不同に処理して良い regular variable があるかどうかは、singleton removval の 結果に依存するので、1path で厳密に取り除くことはできない。 が、2nd path では確実に取り除くことが出来る。 ぶぶ、2nd pathは全然処理が違う!! sbdt と共用はできない Tue Nov 7 15:45:07 JST 1995 chop のレベルで分ければ、まあ、良い。問題は、そのあと。と、 考えると、BDDに変換するレベルで対応する方が望ましいかも知れない。 もちろん、今のままでもsafeなんだけど、落ちているものが多い。 それは結果的に状態を増やしていることになる。 一つの方法は、 p(^r) => ?(^r,pt,pf) とする。 (pt,pf; tf), (pt;pf) と変形する。と、こんな具合。これは重いなぁ。 (~ ^r), ^r がボトムアップではfにならない。ま、そういうことなんだよな。 Tue Nov 7 10:38:59 JST 1995 どうも、singleton removal だと、[a](^r = length(2)), f(^r) のようなものは完璧にトレースできるらしい。 [a](^r = length(2)), *(^r) もOk だった。 でも、さすがに文法記述は発散する。 結局、どういう制限なのかなぁ? diag 時に、full trace できたかどうかを チェックするか... どうも、シングルトンチェックが甘いな。もっと、ちゃんとチェックする ためには? Mon Nov 6 15:57:46 JST 1995 [p_0,p_1,...,p_n] は、 p_0,p_1,...,p_n -> true ~ p_0,~ p_1,...,~ p_n -> false else -> true_false という形でBDD(MTBDD)になる。3値論理 ^r -> true_false true_false -> empty? choice ? true : fals : true_false t,tf -> tf t;tf -> t tt;tf -> tf f,tf -> f f;tf -> tf tt,tf -> tf (あれ、cross termは?) 確かにこれでうまくいきます。はい。* ^r も完璧。 問題は、実行をtraceできるかどうかだな。 Mon Nov 6 08:50:01 JST 1995 singleton の効果は有限か? BDDの中でsingleton duplicate を許すとすると、これは止まるのか? selection(uniq set of subterm) という形になるはず。だから、とまるはず。subtermは有限。singleton には、 R名による区別さえ必要無い。 ^r -> ^([false,true]) ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n]) という展開になる? 再sortは必要。 一般的に、^(r,[p_0,p_1...p_n]) という形で収束しないの? r が一つだったら... ネストしたらout。でもnestはあっても固定だから。 が、これでcomputationをトレースできるのか? いや、特別な展開が必要。 あと、determinization しないとね。(どうやって?) ^([p_0,p_1...p_n]) -> ^([px_0,px_1...px_n]) の際に、px_0 には next のみが入る。そうすれば良い。 itl(p_0,more,..) での出力はnext,true,false。Ok。 Sun Nov 5 21:34:33 JST 1995 しかし、なんと * ^R は非常に大きな状態を生成する。 ^R と true & ^R の干渉が大きな状態を生成してしまう。(らしい) これを抑えるには? 一つはlength で頭を抑えることだな。 ああ、でも、やっぱり大きいか。あんまり、うまくない。 length(10) でも結構巨大か.. proj でも同じような問題はあったのだけど... ^r の permuation の対称性を何とかしない限りだめだね。 しかし、順序は変えちゃダメなんでしょう? うーむ。 でもさ、モデル自身は小さいんだが.... うーむ。 いや、この場合は singleton removal が効くみたい。そうか。 これはsingleton の処理が正しくないからじゃない? singleton の効果は有限か? f(r^1,....r^n) -> exists だとすれば有限。だけど、固定してはだめ。 r^s ? length(1) : r^s ? length(2) : .... となりうる? Wed Nov 1 21:12:04 JST 1995 例題ねー... しかし、<>^R が使えないとなると.... あ、でも、* ^R は使える。 Mon Oct 16 16:05:31 JST 1995 LITL で、closure, proj 抜きだとpolynominal orderの方法がある!? ~(....&....(...&... ~(...&....))) という形で、これにvariable patternを埋め込んでいけば良い。これだと marking だから state space database はいらない。 tableau expansion でも、生成される状態は同じ数だから結果的にpolynominal になっていたのかも.... たしかに、quantifier, closure, proj を入れると verification は難しくなっていた。 いや、でも、empty interval があると、そうもいかないか? ~(....&....(...&... ~(...&....))) の任意のchopをand,emptyに変える操作がいる。これは exponential。 p & p & p & p & p p & p & p & p,empty , p chomp (non-empty interval chop) だったら、大丈夫。 でも、closure, proj をいれるならおんなじか。 Mon Oct 9 19:51:27 BST 1995 proj では、r^n の n を階層化する。r^0 は、すべての階層で共有される。 他のlengthは共有されないとみるのが正しいのだろう。length(1) proj Q だと、r^1^1 = r^0^1 だよね? P proj Q で、Q part のnext part は、 proj の中にencupsulated されているので、term はいじる必要はない。が、 condition はいじる必要がある。ただし、renaming を original clock level と同じにすると limit が効きすぎるだろう。しかし、ここを複雑に するのは、どうかなぁ。term level も階層化すれば、問題はない。 (r^n)^n とか... 結局、singleton removal は、うまくいかないね。これがうまくいけば、だい ぶ範囲が広まるのだが.... せめて、eventuality と同じぐらいまでにできな いの? あ、そうか、r^s をmarking と見ればいいわけね。しかし、結構、めん どくさいといえばめんどくさい。 Time constant regular variable renaming なしならば、割と自明。 r^0 ... r^limit をunifyすれば良い。renaming ありだと、もう少し複雑になる。r^n を state と見るのが簡単。いずれにせよ、かなり制限された感じだね。 renaming の、もっと気の聞いたalgorithmがあれば... Mon Oct 9 05:48:38 BST 1995 ^r -> true/false では、[a](^r=length(2)) が unsatisfiable. over(r) では、true/false に置き換えている。^r -> +r/-r でも、 [a](^r=length(2))はだめ。これにさらに工夫がいる。 でも、それはこっちの方がましだということだろう。でも、どれくらい ましなの? local でないぐらいか? singleton を ^(r,s) で置き換えても、[a](^r=lenth(2)) は、> length(4) でfail する。なんで? Sat Oct 7 17:20:17 BST 1995 singleton removal を r^s で行なうと、limit を一つ伸ばす効果が あるらしい。したがってlimitまでいくような場合は状態が増える。 r^s の選択を独立に行なうような方法で、ちゃんとできるのか? できないような気もする。 Sat Oct 7 10:08:57 BST 1995 (1) 番号を詰める (番号limitあり) は、やってみたけど、^r には効果があるんだけど、他のはほとんど 関係ないなぁ。[a](^r...) みたいなものにはきかないのだろう。 Fri Oct 6 09:46:45 JST 1995 (1) 番号を詰める (番号limitあり) (2) singleton removal この二つでかなりいくはず。(2)どうにかなんないの? (3) 番号を構造化する low resolution? Edge driven な logic にできるか? Thu Oct 5 18:27:29 JST 1995 うーむ。length limit は、うまくいくが、それ以外の制限がいまいち うまくいかないね。 rename して ^r の数を制限する方法だと、over に変換されるものが あまりにアドホックに決まってしまう。 r^n の n に、何か term を持って来れないの? total order を持って来るか... 効果あるの? さぁ... Sun Sep 24 01:14:36 JST 1995 だから、 ^r = false にすると、 [a](^r=legth(2)) -> [a](false=legth(2)) [a](false=legth(1)) [a](false=legth(0)) = unsatisfiable になるからだめなの。うんうん。 true = length(2) も false = length(2) も、両方ともunsatisfiable。どちらかというと、 (length(2);not(length(2))) & true となるのが正しい。 (length(2) & true) ; (not(length(2)) & true) は? これは Ok なはず。 だったら、expansion する前にsingletonをチェックして、singleton に対しては quantifiy してしまうってのは? うーむ... じゃあ、なんで ^r -> ^r;not(^r) ではだめなのか? これは、終りを共有するものをいっしょにしているから。 ^r on n+1 |--| T |-| F || F |-| T || F || F とする ^r on n |---| |--| |-| || が新しいもの。これらは、独立。ふんふん。 Tue Sep 19 23:53:19 JST 1995 どうも変だな。 down(r^0) と true;false とはどこが違うんだ? state(1 , not(true& ?(^r,not(@ @empty),@ @empty)&true)) [a](^r = length(2)) [empty,down(r,0),up(r)]->false [empty,not(down(r,0)),up(r)]->empty [empty,down(r,0),not(up(r))]->empty [empty,not(down(r,0)),not(up(r))]->empty [more,down(r,0),up(r),ev(r^0)]->false [more,not(down(r,0)),up(r),ev(r^0)]->2 not(true& ?(^r,not(@ @empty),@ @empty)&true); [a](^r = length(2)); not(not(@empty)&true),not(@empty&true) [i](length(1)),not(length(1)&true) [more,down(r,0),not(up(r)),ev(r^0)]->3 not(true& ?(^r,not(@ @empty),@ @empty)&true); [a](^r = length(2)); not(@empty&true) not(length(1)&true) [more,not(down(r,0)),not(up(r)),ev(r^0)]->3 やっぱり違う。true だと、length(1)でtrue length(2)でfalseという 技が出来ない。この選択はこの場所で独立に選択しなくてはならない。 (ええ?だけど、true;false なんだから... だったらtrueか?) +r, -r の方がましか? Sat Sep 16 11:44:25 JST 1995 singleton ^r を true, false に置き換えると、[]true,[]false の意味に なってしまう。実際は、true/false なのに。だから、singleton removal はうまくない。 t0: ^r = length(2) t1: r^0 = length(1) empty/not(r^0) t2: r^0 = mpty(1) empty/r^0 Quantifierに置き換える? だったら残しておいた方がまし? 何かoperatorを作る? some -> true/false quantified true? <>false かな? not([](true)) = not(not(true & not true))). でも、これだといつかはfalseになってしまう。operatorにすると、deterministic でなくなるか。それはまずい。negationが。 Fri Sep 15 11:26:13 JST 1995 singleton check をitl時にすることはできない? Wed Sep 13 18:24:24 JST 1995 結局、RITLは CFG を含んでいるのだから、Regular Subset を決めることは できない。 ^r のdepthを制限すれば、ある程度はできる。しかし、これでは fairnessにはならないね。 depth 以外の制限は? 状態数の制限が望ましい。 singleton の remove でかなりのことが出来ると言えば、そうなのだが。 singleton remove のタイミング? itlの時に detect? itlstd の時に detect? remove の仕方 eventually(^r,N) eventually(not(^r,N)) を挿入する。ということは、itldecomp の show の直前で 行えば良い。 しかし、これだと正確な状態出力ではない。ではないが原理的にトレース できる部分をはしょっているだけ。mark を付けるのでは同じになってしまう。 やはりremoveしたい。 ^rの出現頻度を押さえることで、logicになるか? 例えば2つとか? * consistent にならない==safeでない(標準形を工夫すれば...) * でなくても良いという考え方もある。characterriseできる? いずれにせよ、singleton removal でどこまでいくかだな。 Sun Jul 23 10:16:02 JST 1995 * ^r -> +r, -r depth によって独立に選択 * +r も r^depth により選択 これだと、[a](^r),<>(not(^r))がsatisfiable * ^r -> +r, -r depth によって独立に選択しない と、[a](^r=length(2))がunsatisfiable うーむ、うまくいかん。 Sat Jul 22 12:52:11 JST 1995 * depthの違いはchopの処理で行なう * ^rのemptyと、+r, -rのemptyは独立 * ^rのmoreと、+r, -rの関係 +r, -r は、異なるdepthでT/Fの時に生じる 既に +r がある時は、それに合流して良い +r/\-r となることはない。それはfalse。 |-------| +r |---------| -r ^r +r とする not(^r)があったら-rとする これでいいか? tailを共有するrである not(^r),と^rの扱いは対称 ^r/-rの組合せは? +r, -r が解消される場合 * +r or -r がempryになるとき -r はemptyにならない +rが残って害があるか? -rがなければ関係ない 状態は増えるけど。 Fri Jul 14 18:31:19 JST 1995 異なる chop で、異なるrの番号を付ける。 その番号毎に up(^r), down(r,n) を行なう これによって、すべての組合せが一応得られる。 番号は状態には付加しない。(いいのか?) 同じinterval上では、 r, not(r) があり得る... これは... 気まずいか。 ^r -> +^r, -^r とする? すると... +up, -up がある? まあ、試してみよう。(やっぱりだめだった...) Thu Jul 13 14:05:06 JST 1995 r^n の数を減らす => 等価でユニークな表現 singleton r^n は消せる doubleton r^nどうしを融合したい。 新しいrをr^nに相対的に定義する (それはできるのだが... +r/-r) のは、うまくいったのだが、足りないものがある。状態数が 足りない。 * 必要な状態数のみを区別する * 同じ結果を生じる変数は区別しない 自分自身と同じかどうか / 違うということを覚えないといけない 同じだったら関係ない What happen in next case? ([a](^r)) not(r^5) & true, r^5 & true, ^r & true, not(^r) & true ---|-----| r^5 ---|----| r r^5が落ちれば一つ減る。減らなければr^6で一つ増える。しかし、 この場合は増えてはいけない。r^5 と ^r 自身は関係が無い。 が、結果は同じという関係がある。( うがー、わからないよう.... ) st6: not(r^5) & true, r^5 & true, ^r & true, not(^r) & true up(^r),down(r^5),down(^r) @not(r^5)&t, t, t, @not(r^6)&t up(^r),down(r^5),not(down(^r)) @not(r^5)&t, t, @(r^6)&t, t up(^r),not(down(r^5)),down(^r) t, @not(r^5)&t, t, @not(r^6)&t up(^r),not(down(r^5)),not(down(^r)) t, @not(r^5)&t, @(r^6)&t, t Mon Jul 10 20:01:46 JST 1995 f(^r) => contratint_1(^r) & continuation_1(^r) g(^r) => contratint_2(^r) & continuation_2(^r) r(r^n)&c(r^n) がnを除いて等しい時、 r^n => r^n' がいえる。 けど、別に等しい必然性もない。(たしかに...) r^nはquantifyして良い。ということは、同じなら消して良いということ? ということか。cross term は? exists(^r, empty(^r)? ...) r0: { +r(const, continu), -r(const, continu) } r1: { +r(const, continu), -r(const, continu) } いつかは +r(empty,continu) +r(true,continu) のどちらかにいく。いや、いかない。emptyなら問題無い。trueが問題(?) +r(fixpoint,contiu) という形になる。これがたくさん存在するということになる。 +/-r^n(fixpoint_k,continu_k_i) というわけだ。この場合のr^nの重なりが解消できれば問題は解決。 うまくいかないね... で、同じものは消して良い。順序をそろえないと消しにくい。 違うrでも同じカッコなら消して良い。(reular variableは、実質は 一つ, ^r => r,^common にするか? それはちょっと違う) この場合は消しても干渉のパターンが変わらない。干渉パターン ごとにマッチングをとるから。(有限の組合せなのか?) 消すのはterm levelでおこなう? c(r^n, i_n...) & ... c(r^n, i_n...) というtermしかr^nに関してはでてこない。消せるんだったら、他の 方法はいい加減でも大丈夫。 f(r^n)とf(r^n'1)の関係 |------|-| |----|-| r^n, r^n' 自身は独立 r^1(r,c) r^2(r,c) empty(r^1),empty(r^2),empty(r) => c cross term empty(r^1),more(r^2), empty(r) => c,(more(r),r^1(@(r),c)) more(r^1),more(r^2), more(r) => more(r),r^1(@(r),c),r^2(@(r),c) == r^1(c);c,more(r),r^1(@(r),c);more(r),r^1(@(r),c),r^2(@(r),c) 他のr^nと干渉する方法が変わってしまう... Sun Jul 9 15:32:43 JST 1995 r^1 & true; r^2 & true; r^3 & true 一つにまとめられない? f(+/- r^n) (必ずtopにある/一度展開されているから) |-------------|-----------| down(r^n) => true/false 性質 f(+/- r^n) down(r^n) => f((+/-true ,empty)) not(down(r^n)) => f(+/- r^n) parallel termがある時は無くなるまで展開する r^n, *length(3) などは? これは無視して良い r^n, *length(3) & true が問題 => evenrually true + *length(3) だから、nが複数あっても、f((+/-true ,empty))が同じなら同じでよい(?) f(+/- r^n) => true & down(r^n),f(+/-true,empty) => down(r^n) = eventually(f(+/-true,empty)) ということは、やっぱりdown(r^n)を外に出せるということ? r^n & true なら eventually(true) not(r^n) & true なら? ふむ。そして eventually(f) の f にはr^nは入らない。これは いけるかも知れない。 chopの処理の時に、eventuality listをbdtの形で外に出せば良い。 eventuality が満たされた時がr^nが成立した時。(これも 前考えたな...) ^r & .... という形だけ? (^r, g) & f => ev(f),(g & f) ちょっと違う... (^r & f),(g & f) とは少し異なるよ。not がうまくないはず。 not(ev(f)); not(g & f) (?) そうか... ev(f)が満たされれば、^rは落ちて良い。(落ちれる) 落ちなくてもいい。 前もってevenruality formにITLを書き換えるのは? f(r) => g(eventualy(h)) 本当にdiceidableなのか? 整数方程式が書けるとすれば... Fri Jul 7 18:51:32 JST 1995 true & ^r & true => r^1 & true; r^2 & true; r^3 & true となる。ということは、ひとつのintervalだけを見て吸収することは出来ない。 t1 t2 up(r) down(r^1) r&true |-------------|-------------------- not(r&true) |----------------|not(down(r^1)---- |---|up(r)----|not(down(r^2)------- r^1 は競合するr^1がある時しか関係しない。したがって単独に 出てくるr^1は現在時点で fin(r^1) => true fin(not(r^1)) => false を決めて良い。これだけで、true & ^r & true は収束する。 が、それだけで収束するか? たぶん、しない。 (1) 複数の始点を持つ状態を一つにまとめられればできる。+r, -r はそういう 方法だった。が一つにはならない。有限な組合せになる。 (2) 収束するとすれば、共有されたr^nの組が有限な場合である。これは、finiteness の条件に相当する。前もって共有される可能性のあるtermを生成できるか? ( たぶんできる) 前もって複数出て来た(違うsytactical interval上の)^rに番号を付けて 識別しておく。競合は、異なる番号上でしか起きない? [](<>(^r)) = not(ture & not(true & ^r)) のような場合は? そうか。同じ番号上の共有は+r, -rで構わない。 (true or false だから) [](<>(^r)) <-> [](<>(^r)) のような場合は? Fri Jun 30 20:08:47 JST 1995 f(r^1,r^2,r^3) & true, g(r^1,r^2,r^3) & true f(r^1,r^2,r^3)とg(r^1,r^2,r^3)を見ながらr^nの数を減らさないといけない。 r^n は、emptyの時しか影響しない。moreの時はtrueと同じ。 ^r のみが新しいr^nを増やす。これをいかに吸収するかを調べれば良い? f(r^cur,r^1,r^2,r^3) & true, => r^cur ? +f(r^1,r^2,r^3) : -f(r^1,r^2,r^3) & true g(r^cur,r^1,r^2,r^3) & true => r^cur ? +g(r^1,r^2,r^3) : -g(r^1,r^2,r^3) & true Fri Jun 30 10:48:46 JST 1995 各stateに、regular variableのmapを割り当てる。方法がいまいち わからない。^rの生成された状態を識別することが必要。 ^r(s) をやってみる。昔もやった。 true & ^r が爆発する r^1 ; r^2; r^3; ... ; true & ^r これが r^1 true & ^r となれば良い。 r^1 .... r^2 は新しいr^nになる。(相互関係は?) ^r どうしの制約を保持した もっとも少ないr^nを選択すれば良い。(この変換はsafe & compete?) 相互関係を保存しないなら^rをすべて共通にすれば良い。が、 それはうまくいかない。 r^1 , not(r^2) -> r^1, not(r^1) -> false のような場合があるから。 r^1 , not(r^2) -> r^1 か? 他の変数が入る場合は? r^1 .. r^n に依存するtermの変換を 計算する。= BDT の leaf の数。それを表現できる最小のr^nを 作る。 そうすれば、temporal operatorのネストは変わらないのだから、 全体は有限になるはず。 これでなんでfullでなくてregularになるの? ^r がcontext dependent でないから。 r^1 , not(r^2) -> r^1 は、context dependent では できない。(なるほど...) Wed May 24 20:32:34 JST 1995 ^rは、やはり、 ^r -> +r, -r の変換でなんとかするべき。こうして生成したモデルは、正しいRITLを 含んでいる。あとは整合性のチェックをすれば良い。 (1) local consstency check => regular variable (2) global consistency check => regular constant どういうようにcheckするの? ん.... 昔のbdcomp.pl をbddlibで書き換える。 characteristic function f(q) f(q) = more,fx_q(sbn,sbx,P);empty,fn_q(P) f(p&q) = f(q) & q Tue May 2 17:49:35 JST 1995 BDDLIBを組み合わせたが、やっぱり Prolog <-> BDD の変換が入るだけ 遅くなるだけだった。bdtstd.pl は綺麗になるのだが。 前作ったBDDの方式も遅くなるだけだった。(BDT/*) それは、 BDD の leaf をnext leafに展開 BDDの再構成 next leafを2-3 treeに登録 新しいnext leaf をさらに展開 というのがすごく遅かったから。 Charcteristic Function を作り上げる方法は、今一だ。でもBDDLIBなら うまくいくかもしれない。 Subtermを前もって、すべて、 condition, next というBDDに展開しておいたら? Quantifierなどは、Subtermの中に状態が現れてしまう。だから、 前もって、中を展開しておく。 そうすれば、あとの処理は、BDDのみでできるはずだ。(しかし、CF法と 結果は同じ?) Wed Mar 29 17:22:43 JST 1995 regular(r,....r....) という形を使う ( QPTL <-> RITL だから... ) Quantifierを直接使うのは? st(0) = exists(c, c->st(1),not(c)->st(2)) さぁ... begin(r,formuala) -> T/F end(r,formula) -> T/F 異なるうformulaが実は同じだった。-> いつか regular(r, f) という同じ形になる。 regular(r,f(r)) empty(f(r)) -> r=true,empty not(empty(f(r))) -> r=false,empty regular(r,f(r)) more(f(r)) -> r=true,regular(r,fx(r)) not(more(f(r))) -> r=false,regular(r,fx(r)) したがって生成されるモデルは冗長。 chop が来た時に r をreset しないといけない。 (だよね...) だったら、regular(r,f(r))はいらない? どうやって? r を前もって宣言するってのは? PDA との関係は? Thu Dec 15 20:21:58 JST 1994 Modelとの対応 t0 -[+-]-> t1 -[+-]-> t2 -[+-]-> t3 |---------|-----------| r0 r1 r2 |-----------|-----------| r0' r1' r2' r0 は常に要素0から始める。 から始める。 r0 -[-]-> r1 で集合の要素にシフトする。 r0 -[+]-> r1 で次の時間のものと違うFAであることを表す。 Mon Nov 28 19:27:37 JST 1994 RITLステートをITL formulaのbool代数で表す。bool代数はBDDで表現する。 もともとITL formula自身がsubtermの集合だから、二重のbool代数になる。 したがって、double exponential algorithmとなる。 r/not(r) flip では、すべての組合せは生じるが、すべての組合せの 連結は表現できない。したがって、生じたすべての組合せをとって おけば良い。 集合の作り方 r/not(r) flip で生じたLITLを集合として持つ (implementationは?) r の例 [1] r -(+r)-> r, r -(-r)-> not(r) {r,not(r)} [2] r -> {r,not(r)} -> {r,not(r)} (終り) t & r の例 (detailは異なる。emptyの場合があるから) [1] t & r -(+r)-> r\/t & r, t & r -(-r)-> not(r)\/t & r {r\/t&r, not(r)\/t&r} [2] {r\/t&r, not(r)\/t&r} -> {r;t&r, not(r);t&r} (終り) [a](r=length(2))の例 [1] [a](r=length(2)) -(+r)- > r =length(1)/\[a](r=length(2)) -(-r)- > not(r)=length(1)/\[a](r=length(2)) {r =length(1)/\[a](r=length(2)), not(r)=length(1)/\[a](r=length(2))} [2] {r =length(1)/\[a](r=length(2)), not(r)=length(1)/\[a](r=length(2))} => { r =length(0)/\ r =length(1)/\[a](r=length(2)), F r =length(0)/\ ~r =length(1)/\[a](r=length(2)), ~r =length(0)/\ r =length(1)/\[a](r=length(2)), ~r =length(0)/\ ~r =length(1)/\[a](r=length(2))} F [3] => [2] へ or [1]'へ (r=length(1)がtrueの場合) もっとコンパクトになるんじゃない? (これだとfinitenessは明解だけど) ITL(r)は、rをr/not(r)に任意に置換したもののsubset。どれとどれが一致するかを 覚えれば良いのでは? => 開始時点が等しいものが一致。 Indexを付けるのはダメ。=> モデルが有限にならない。(うーむ、わからない) ITL(r) => 展開 => subset モデルの解釈 bool代数は、rのassignmentが与えられると解決する。しかし、一つの ノードが別な解釈を共有することもあり得る。 Term間は任意に遷移するのか? そうではなくて、同時に遷移する。 異なる開始時点を持つrは、同時に異なる遷移を廻る すべて可能な遷移があるわけではなく、いくつかはFとなり禁止となる => r に対する制約 実行できる? bool節の一つのinstanceを適当に実行すれば良い Rに単一のautomatonを割り振ることは可能か? [a](R = r) where r is automaton constant 時間を遡ってモデルを作る これによって、state minimizationも同時に走らせることができる Minimizationのテストプログラムを作って見ること Thu Nov 24 14:54:00 JST 1994 LTTL = LITL < RE LITL* = RE RITL = RE RITL(= 2nd order LITL) RITL is decidable LTTL = LITL on compact time Even(p)は、LITLでもだめ。 (p.)* ができない (abac)* -> (a[bc])* LITL -> LTTL converter LITL/LTTLは、やっぱり群を構成する []a & []b & []a a...ab...ba...a -> a until (b until []a) だからconversionできる? a & b & aは a, <>(b, <>a) か... うう、できそうな気がする... P & Q -> start(P),(run(P) until lttl(Q)) に変形する run(P)にはquantifierが入るのか? 入らない? events continue |----------|..........| |-> <>(events) |-> [](continue) <>events, <>(continue until Q)) というようにcompileする。ふむ。 l(P) & Q l(P) = LTTL formula of P <>(P) -> <>(P,<>(l(Q))) [](P) -> P until l(Q) RITL decidability Reverse Specification R -> +(R) -(R) on Start Time empty(R) は hidden だけど、+R/-R に関しては同期する ここがまだ良く分からない。 Modelを直接構成しない。filtrationの意味でも...大きすぎるから。 その代わり、Model constraintを構成する。 Generating C / In-kernel implementation Wed Oct 5 15:30:19 JST 1994 Regular variable. ^r -> more(^r), @( ^r) not(more(^r)),@(not(^r)) ^r -> empty(^r), empty not(empty(^r), not(empty) This gives ^r constraints, and produce finite state. Meaning of regular variable. Mij(^r) = f(Mi(more(^r),empty(^r)),Mi+1j(^r)) ^r's automaton is depend on clock, and fin time is controled in finite state machine's way. Mij(^r) is f(Mi(p)...Mj(p)). ^r = lenght(3) & ^r = length(2) is statisfiable. Is this different from interval variable? Yes. But How? If we need all regular variable act the same automaton, exists(^c) [a](^r= ^c),... where ^c is a time stable automaton. It is ok to show:, M |= not(^r),(^r & true) Problem. [a](^r=lenth(2)) , lenth(4) is unsatisfiable empty(^r),(empty =^r) => ^r (true) empty(^r),(len(1)=^r) => not(^r) (false) ((empty = ^r)&true), ((length(1) = ^r)&true) but this is satisfiable.... ?-? Let's think about, exists_automatic(R) f(R) = g automatic unification = boolean unification? Sat Jun 12 10:41:24 JST 1993 dvcomp uses subterm tree for decomposition and ndcomp uses chop normal form. Since development result is not the same, lazy generation of state is not allowed. sb's and itl_state's hash and sharing is important. Time to write C version? Sun Jun 6 14:15:42 JST 1993 Now module system is supported. tgen/0 generates Tokio program and kiss/0 generates KISS format for SIS. ex(300,X),ex(true proj ~X) becomes very large. Terminates? ex(300,(X,Y)),ex(true proj (X;Y)) is still very large, but ex(300,(X,Y)),ex(true proj X) is Ok. old/bdcomp does not check sbterm early. This is the reason why this method is slow. expansion ; subterm check is bad expansion with subterm check will be ok. How about permutation? Declare permutation from the begining. |- permute V on F <-> F How about anti-symmetry? |- odd-permute V on F <-> ~ F |- even-permute V on F <-> ~ F Mon Nov 9 15:18:49 JST 1992 prefix operator is wrong. length(2),prefix((length(3),fin(false))) must be false. Mon Sep 21 20:16:39 JST 1992 I'm very sorry to send you rather large example. But it is a little dificult to extract simple example. To compile and load, | ?- [bddi]. In next example, fixpoint predicates find a subtle counter example of ITL formula. (p&&p&&p&&p&&p&& ~p&&p)->[](<>p) is tested by | ?- ex(10,X),fixpoint(X). First, this formula is translated into a finite state automaton. Like this. +----------+ E,PL -------| Logic |---> E,PL | | Sn +------| |--->+ Sx | | | | | +----------+ | | +----------+ | +-<----| Latch |----+ +----------+ In this case, Sn/Sx pairs are vector of ITL subterm. "Logic" is defined in boolean constraint on Sn/Sx. In fixpoint/10, fixpoint(F,Fix,Fix1,E,P,PL,Sn,Sx,S,N), F current possible state (boolean constraint of Sn) Fix disjunction of visit state Fix1 previous visit state, if it is eqaul to Fix, everything is done. E,P,PL Input/Output value of variable in state diagram Sn state variable Sx next state variable S for display subterm state. N depth count fixpoint(_,Fix,Fix1,_E,_P,_PL,_Sn,_Sx,_S,_N):- bool:taut(Fix=:=Fix1,1),!,write('end'),nl. fixpoint(F0,_,Fix,E,P,PL,Sn,Sx,S,N):- quantify(Sn,F0,F0S),bool:sat(F00=:=F0S), % take all possible state display_state(E,E*F00,P,PL,S,_,Sn), % find counter example quantify([E|PL], ~E*F00,F0P), % for all possible I/O bool:sat(F0Q=:=F0P), copy_term([E,Sx,F0Q],[0,Sn,F1]), % replace Sn/Sx bool:sat(Fix1=:=Fix+F1), % for termination write_state_number(N,N1,'depth:'),!, fixpoint(F1,Fix,Fix1,E,P,PL,Sn,Sx,S,N1). So this traces all possible execution in finite state automaton. | ?- ex(10,X),fixpoint(X). depth:0 % it becomes slower and slower... depth:1 depth:2 depth:3 depth:4 depth:5 depth:6 depth:7 empty,[t(p,0)],[...] % find one counter example |: % a return is required depth:8 end X = ((p&&p&&p&&p&&p&& ~p&&p)->[](<>p)) ? yes | ?- I think I need something like setarg in boolean constraint. Sun Sep 20 18:10:30 JST 1992 Why not add exclusive status as a primitive? states([a,b,c,d,e,f]) -> [](( ~(( a,b)), ... ) 2^n ... Wow! It generates status(a)-> ... ; status(b)-> ... status(f)-> .. ; status([])-> ... generate n+1. Tue Sep 15 13:04:43 JST 1992 結局、Regular variable state を共有しないと収束しないし、 共有できるかどうかの判断は大域的だから、この方法では できないらしい。 Tue Sep 15 11:36:36 JST 1992 Regular variable must be non-deterministic. ^r [more,up(r),down(r)] is not false If we don't care about down, we cannot distinguish ^r& ^r ,not( ^r ) up(r) down(1) ~down(1) | | | |----------------|-------| up(r) down(2) Mon Sep 14 14:07:52 JST 1992 (^r & ^r),not(^r) itl:0 [empty,up(r),down(r,0)] -> false itl:0 [more,up(r),down(r,0)] -> false itl:0 [more,up(r),~down(r,0)] -> (stay(r,now)&^r),not(stay(r,now)) now=1 stay(^r,0) (stay(r,now)&^r),not(stay(r,now)) itl:1 [empty]->false itl:1 [more,down(r,1),up(r),down(r)]->false itl:1 [more,~down(r,1)]-> (stay(r,now)&^r),not(stay(r,now)) now = 1 2 itl:1 [more,down(r,1),~down(r,0)]]-> stay(r,1);(stay(r,now)&^r),not(stay(r,now)) 3 stay(2,1) stay(r,1);(stay(r,3)&^r),not(stay(r,3)) itl:3 [empty,down(1)]->empty itl:3 [empty,~down(1)]->false itl:3 [more,down(r,1)]->true itl:3 [more,~down(r,1)]-> stay(r,2);(stay(r,4)&^r),not(stay(r,4)) = 3 itl:3 [more,down(r,1),~down(r,0)]]-> stay(r,1);(stay(r,3)&^r),not(stay(r,3)) 3 stay(2,1),stay(4,3) Mon Sep 14 00:25:08 JST 1992 ^r で生成されるautomatonは、^rを普通の変数と見て生成するtableauの subsetである。従って、tableauのnodeを指し示すことで ^r のモデルを 作ることが出来る。しかし、うまくいかない... (^r & true),not(^r) のモデルはないから そこで、stay(r,N)を使う (up(r),emtpy & true & down(r),empty) ではだめ。 ^r & ^r -> ^r になってしまうから。 するとモデル構築が収束しない --> これは Full ITL だから しかしRITLのモデルは有限だから stay(r,N)のかなりの部分は 相互に等しい。等しいかどうかをどう判断するかが問題。 Deterministic Pathが等しければ同じstateと判断するのでは足りない Loopが作れないから。 むしろすべて等しいのがDefaultで、必要な時だけ分離するのが望ましい Mon Jan 1 11:05:38 JST 1990 ^r & ^r itl:0 [empty,up(r),down(r)] -> empty itl:0 [more,up(r),down(r)] -> false itl:0 [more,up(r),~down(r)] -> stay(r,[true])&^r 1 stay(r,[]) -> down,empty stay(r,[]) -> ~down,more stay(r,[])&^r itl:1 [empty,down(r,[]),down(r,[true]),up(r)] itl:1 [more,down(r,[true]),up(r),down(r,[])]->false itl:1 [more,~down(r,[true])]-> stay(r,[true,true])&^r 2 itl:1 [more,down(r,[true]),up(r),down(r,[])]->false itl:1 [more,down(r,[true]),up(r),~down(r,[])]->stay(r,[true]) 3 -> false itl:1 [more,down(r,[true]),~up(r)])]->false stay(r,[]) -> down,empty stay(r,[true]) -> down,up(r),empty stay(r,[true]) -> more, ~down, stay(r,[true,true]) stay(r,[true]) ?why not stay(r,[true]) -> more, down, up(r), stay(r,[true]) -> false stay(r,[true,true]) -> down,up(r),empty itl:2 [empty,down(r,[]),down(r,[true,true]),up(r)] itl:2 [more,down(r,[true,true]),up(r),down(r,[])]->false itl:2 [more,~down(r,[true,true])]-> stay(r,[true,true,true])&^r 4 itl:2 [more,down(r,[true,true]),up(r),down(r,[])]->false itl:2 [more,down(r,[true,true]),up(r),~down(r,[])]->stay(r,[true]) 3 -> false itl:2 [more,down(r,[true,true]),~up(r)])]->false stay(r,[true,true]) -> down,up(r),empty stay(r,[true,true]) -> more, ~down, stay(r,[true,true,true]) stay(r,[true,true]) ?why stay(r,[true,true]) -> more, down. Sat Sep 12 18:05:26 JST 1992 How about contiion-history list? (p->^r),@((q->^r),@empty) itl:0 [more,p,up(r),~down(r,[])] -> stay(r,[p]),(q->^r,@empty) 1 itl:0 [more,~p]-> true stay(r,[]) p ->stay([p]),~down ~p->true stay(r,[p]),q->^r,@empty itl:1 [more,p,q,up(r),~down(r,[p]),~down(r,[])] -> empty,stay(r,[(p,q),p]),stay(r,[p]),stay(r,[q]) 2 itl:1 [more,~p,q,up(r),~down(r,[p]),~down(r,[])] -> empty,stay(r,[(~p,q),p]),stay(r,[q]) 3 itl:1 [more,~q] -> empty,stay(r,[~q,p]) 4 stay(r,[]) q ->stay(r,[q]),~down ~q ->true stay(r,[p]) q ->stay(r,[(p,q),p]),~down q ->stay(r,[(~p,q),p]),~down ~q->true empty,stay(r,[(p,q),p]),stay(r,[p]),stay(r,[q]) itl:2 [empty,q] -> false itl:2 [empty,~q,down(r,1),down(r,0)] -> true stay(r,[(p,q),p]) ->down stay(r,[p]) ~q->down stay(r,[q]) ~q->down stay(r,[(p,q),p]) ~q->down empty,stay(r,[(~p,q),p]),stay(r,[q]) itl:3 [empty,down(r,1),down(r,0)] -> true stay(r,[(p,q),p]) ->down stay(r,[q]) ->down empty,stay(r,[~q,p]) itl:3 [empty,down(r,1)] -> true stay(r,[~q,p]) ->: down Fri Sep 11 16:13:48 JST 1992 Parallel Regular variable construction itl:0 [up(r),~down(r,0)] -> ... stay(r,0).... 1 -> stay(r,N1) [up(r),~down(r,0)] -> ... stay(r,0).... 2 -> stay(r,N2) ^r:0 [up(r),~down(r,0)] -> ... stay(r,N1).... 1 [up(r),~down(r,0)] -> ... stay(r,N2).... 2 equivalence list stay(r,i) = stay(r,j) if stay(r,4) -f-> stay(r,i) stay(r,4) -g-> stay(r,j), f->g stay(r,n) .... itl:n -> [x0,x1,x2...xk] Tue Sep 8 22:13:51 JST 1992 true & ^r [empty,up(r),down(r)]->true [more,up(r),down(r)]->(stay(r,1);true & ^r) [more,up(r),~down(r)]->(stay(r,1);true & ^r) = 3 [more,~up(r)]->(true & ^r) How to prevent stay(r,N) multiplier? state(3) = (stay(r,1);true & ^r) [empty,down(r,1)]->empty [empty,down(r,3),up(r),not(down(r,1))]->empty [empty,not(down(r,3)),up(r),not(down(r,1))]->false [empty,down(r,3),not(up(r)),not(down(r,1))]->false [empty,not(down(r,3)),not(up(r)),not(down(r,1))]->false [more,up(r)]->(stay(r,1);stay(r,3);true & ^r) [more,not(up(r))]->3 Why stay(3) = stay(1)? .... Finitarity? state(1 , ^r& ^r,not(^r)) [empty,down(r,1),up(r)]->false [empty,not(down(r,1)),up(r)]->false [empty,down(r,1),not(up(r))]->false [empty,not(down(r,1)),not(up(r))]->false [more,down(r,1),up(r)]->3 (stay(r,1);stay(r,1)& ^r),not(stay(r,1)) [more,not(down(r,1)),up(r)]->4 stay(r,1)& ^r,not(stay(r,1)) [more,down(r,1),not(up(r))]->false [more,not(down(r,1)),not(up(r))]->false state(3 , (stay(r,1);stay(r,1)& ^r),not(stay(r,1))) [empty,down(r,1)]->false [empty,not(down(r,1))]->false [more,up(r),down(r,1)]->3 [more,not(up(r)),down(r,1)]->3 [more,not(down(r,1))]->3 state(4 , stay(r,1)& ^r,not(stay(r,1))) [empty,down(r,4),up(r),down(r,1)]->false [empty,not(down(r,4)),up(r),down(r,1)]->false [empty,down(r,4),not(up(r)),down(r,1)]->false [empty,not(down(r,4)),not(up(r)),down(r,1)]->false [empty,not(down(r,1))]->false [more,up(r),down(r,1)]->3 [more,not(up(r)),down(r,1)]->4 [more,not(down(r,1))]->4 1.4510000000000002 sec. Tue Jun 30 17:01:37 JST 1992 Quantifier does not works well. ?-fixpoint(even(p)=evenp(p)). Projection looks like difficult. Tue Jun 30 08:58:27 JST 1992 fixpoint((a,(more = (more & more)))) terminates. why? fixpoint(more = (more & more)) causes loop. why? It looks like SICSuts's bug. Some how I avoid that. Sun Mar 01 01:01:57 1992 BST Yes, I almost finish BDD version. Quantification is very subtle in SICStus. ?-bool:sat(_A=:= B*C),bool:sat(_A=:=A),bool:sat(E =:= ~B*A^A). ?-bool:sat(_A=:= B*C),bool:sat(A=:=_A),bool:sat(E =:= ~B*A^A). give us different result. ?-fixpoint(p-> [](<>(p)) causes quantifier failure. exists(p,..) is now working, but closure is not. Mon Feb 10 20:06:36 1992 BST ?-fixpoint(p,X). subterm(p,N,_,[p(N)],[]) p =:= N ?-tableau(N,F1,[],[]) F1 = exists(p,F*R)/replace(S,S') N=p, F1=nil? copy_term([],[],N],[[],[],F]), no constrain on N/F ?-bool:sat(F1=:=(N+F)). ?-bool:taut(N=:=F1,1) N=:=(N+F) x Wed Nov 06 21:56:57 1991 BST Dense time modification. more <-> more & more discrete time: more -> empty->false;more->true true -> empty->true; more->true more&more -> empty->false;more->true&more true&more -> empty->false; <---- This makes difference more->true dense time: more&more* > empty->false;more->more* more* -> empty->true ;more->more* more -> empty->false;more->true true -> empty->true; more->true more&more -> empty->false;more->true true -> empty->true; more->true Tue Jun 25 07:21:11 1991 BST 2nd order local variable is also easily implemented. Notation? regurlar Tue Jun 25 07:06:28 1991 BST For verification, Information hiding is bad. Necessary information muse be accessed by everyone for reliability. Only useless information is allow to hide. If some information does not change world, it is useless. Higer abstraction makes many information useless, which can be hide. Tue Jun 25 06:52:32 1991 BST Closure is easily implemented. Single varible quantifier is also easy. These are effectively equivalent in expressiveness. But nested quantifier is very different. Its decomposition is same as sigle variable case, but to make a standard form, it requires P-space. Quantifier impelentation of bdtstd/itlstd will be difficult. Derivation tree generation method is much suitable for quantifier. But is it worth implement? It is better to find out another abstraction mechanism, such as multi-linear projection. The important this is not what IS existing, but how it DOES exists. Quantifier lacks synchronization type. Tue Jun 21 21:08:31 BST 1991 Problem on Theorem prover 1) it does not handle eventuality |= true & empty ( compact interval ) |= finite -> (true & empty) <- eventuality axiom ( open interval ) introducing topology? and differencial? d/dt f(x,t) is related to scheduling? very close to .... 2) dense time what's wrong? 3) 3-stages: itlstd, decomposition, checking are redundant each other. -> derivation tree construction ( do this first ) (bdcomp.pl must work faster) 4) extensions infinite interval interval variable projection framing multi-linear scheduler other standard form interactive proof/protocol design rational length operator 5) overupping interval (minus length) Tue Jun 18 16:45:35 BST 1991 true & q -> NDST e0, e1 q->true m0, e1 q->@true m0, m1 ->@(true & q) else false DST [e0,q] -> true [m0,q] -> @true ;@(true & q) [e0,~q] -> false [m0,~q] -> @false;@(true & q) ~(true & q) -> NDST e0, e1 q->false m0, e1 q->@false m0, m1 ->@~(true & q) else true DST [e0,q] -> false [m0,q] -> ~(@true ;@(true & q)) [e0,~q] -> true [m0,~q] -> ~(@false;@(true & q)) Tue Jun 18 15:49:21 BST 1991 % % London 23:38 36.52 Newyork 18:38 Tokyo 07:38 % p & q -> |-----|-----| 1 0 ifEmpty(p) 1->p ifNotEmpty(p) ~1->p P & Q -> 0 P,Q ~0, 1 beg(P),Q ~0,~1 Pn, @(Px,Q) p & q -> NDST 0 p,q->true ~0, 1 p,q->@true ~0,~1 p->@(true & q) else false DST [p,q] -> [0]true +[~0,1]@true +[~0,~1]@(true & q) <- sometime? [p,~q] -> [0]false+[~0,1]@false+[~0,~1]@(true & q) [~p] -> []false a path must contain true eventuality ~(p & q) -> NDST 0 p,q->false ~0, 1 p,q->@false ~0,~1 p->@~(true & q) else true DST [p,q] -> [0]false+[~0,1]@false+[~0,~1]@~(true & q) <- never? [p,~q] -> [0]true +[~0,1]@true +[~0,~1]@~(true & q) [~p] -> []true a path must not contain false eventuality iのは式の中の&の数に等しい empty 0 true ~0 false ~empty 0 false ~0 true fin(p) [p] -> [0]true +[~0]@fin(p) [~p] -> [0]false+[~0]@fin(p) keep(p) [p] -> [0]true+[~0]@keep(p) [~p] -> [0]true+[~0]false p & q & r -> NDST 2, 1, 0 p,q,r->true 2, 1,~0 p,q,r->@true 2,~1,~0 p,q->@(true & r) ~2,~1,~0 p->@(true & q & r) DST [~p] -> []false [p,~q] -> [ 0]false +[ 2, 1,~0]@false +[ 2,~1,~0]@(true & r) +[~2,~1,~0]@(true & q & r) [p,q,~r] -> [ 0]false +[ 2, 1,~0]@false +[ 2,~1,~0]@(true & r) +[~2,~1,~0]@(true & q & r) [p,q,r] -> [ 0]true +[ 2, 1,~0]@true +[ 2,~1,~0]@(true & r) +[~2,~1,~0]@(true & q & r) ~(p & q & r) -> NDST 2, 1, 0 p,q,r->false 2, 1,~0 p,q,r->@false 2,~1,~0 p,q->@~(true & r) ~2,~1,~0 p->@~(true & q & r) DST [~p] -> []true [p,~q] -> [ 0]true +[ 2, 1,~0]@true +[ 2,~1,~0]@~(true & r) +[~2,~1,~0]@~(true & q & r) [p,q,~r] -> [ 0]true +[ 2, 1,~0]@true +[ 2,~1,~0]@~(true & r) +[~2,~1,~0]@~(true & q & r) [p,q,r] -> [ 0]false +[ 2, 1,~0]@false +[ 2,~1,~0]@~(true & r) +[~2,~1,~0]@~(true & q & r) Thu Jun 13 12:00:39 BST 1991 Empty Queue should be incoporated into Cond part. Only true/false remains in Em_j part. S = \Sum_j Cond_j -> ( \Sum_i empty_i->Em_{i,j} -> More_j ) ~S = \Sum_j Cond_j -> ( \Sum_i empty_i->Em_{i,j} -> ~More_j ) Thu Jun 13 11:32:44 BST 1991 S = \Sum Cond_j -> ( empty->Em_j ; ~empty->More_j ) ~S = \Sum Cond_j -> ( empty->~Em_j ; ~empty->~More_j ) since empty is invisible, ; means non deterministic choice More_j = Keep \and @ More => troubled on negation Cond_j -> ( empty->Em_j + (Keep_j \and @ More_j) ) => Cond_j + Keep_j -> ( empty->Em_j + ~empty->@ More_j ) Cond_j + ~Keep_j -> ( empty->Em_j + ~empty->false ) Example empty -> true -> (empty->true + ~empty->false) ~empty -> true -> (empty->false+ ~empty->true) fin(p) -> true -> (empty->p+ ~empty->@fin(p)) keep(p) -> p -> (empty->true + ~empty->@keep(p)) + ~p -> (empty->true + ~empty->false) Wed Jun 12 16:05:31 BST 1991 ITL->DST converter using BDT varialbe order p & q ~p -> [] p,q -> [e0, (t & q)] e0 = (t & q) p,~q -> [~e0,(t & q)] t & q (contains both ~e0, e0) ~q -> [~e0,(t & q)] q -> [e0,t,(t & q)] t -> [e1,(~e1,t)] e1 = (t) ITL model checker Wed May 22 15:37:30 BST 1991 The problem is negation of state digram is time consuming task. To make a symmetrical treatment of negation on state digram, exclusion normal form is good. P == (ab -> empty) + ((~a)b -> false) + (a(~b)+~a~b -> @next) ~P == (ab -> false) + ((~a)b -> empty) + (a(~b)+~a~b -> @~next) True-Set + False-Set + Next-Set It requires 2^numver(variables on expression) terms. (Sad..) P,Q -> PQ P;Q -> PQ + ~PQ + P~Q Tue May 21 19:16:12 BST 1991 Extenstion of state diagram is necessary. true & p = <>p s0 -empty-> p s0 -e(true)-> s0 s0 -e(p)-> true ~(true & ~p) = #p s0 -empty-> p s0 -a(~p)-> false s0 -e(true)-> s1(~true & ~p) ~(p & ~q) = #p s0 -empty-> ~p;q s0 -a(p)-> s1(~(true & ~q)) s1 -a(~q)-> false p & q s0 -empty-> p,q s0 -p-> s1(true&q) s1 -e(true)-> s1 s1 -e(q)-> true = s1 -a(~q)-> false Tue May 21 15:08:51 BST 1991 The point is the concurrent development of negation form. |- ~(On Some interval, P) <-> |- For all interval, ~P <-> |\- On Some interval, P |- ~~P <-> |-P |-P,|\-Q => |-P0,@Pnext , |\-Q0,@Qnext => |\-Q0,@Qnext |-(P0,~Q0),@Pnext |-(P0,Q0),@(Pnext,~Qnext) example |- ~(q & ~p) => |\- q,~p,empty |- empty,~(q,~p) |\- empty(q),~p,~empty => |- q,p |- ~q |\- q,@(q & ~p) => |- ~q |- q, @~(true & ~p) Anther problem is Empty/More state. An interval can be empty/~empty ~(empty,P) -> ~empty;~P this is funny |- ~(empty,P) <-> |\- empty,P ~P,~(empty,P),empty is Ok This means false transision has separate Empty flag empty,(P&Q) -> empty,P,Q Global variables maps local variable state diagram -> {true, false} How to calculate it comformity? Thu May 16 12:54:27 BST 1991 Decomposition Rule for Model Checking ~ , ; & @ Failure Set Success Set ?-de(Proposition,Now,Next). de((P,Q),(NP,NQ),(XP,XQ),F) :- de(P,NP,XP,F),de(Q,NQ,XQ,F). de((P;Q),Now,Next,F) :- de(P,Now,Next,F). de((P;Q),Now,Next,F) :- de(Q,Now,Next,F). de(~P,Now,Next,(FN,FX)) :- de(P,FN,FX,(Now,Next)). de(@P,true,P,(FN,FX)) :- de(P,FN,FX,(Now,Next)). % weak? de((P&Q),(PN,Now),Next,F) :- % empty case de(P,PN,true,PF),de(Q,Now,Next). de((P&Q),Now,Next,F) :- % non empty case de(P,PN,true,PF),de(Q,Now,Next). Now is allways classical/local. Using Binary Decision Tree on Interval Variable P = true & P [t]P = ~~P = ~(true & ~P) while i do j = i-> j&(while i do j) ; empty so everything is & and ~ and ; and ,. Formula = { Interval Variable, Local Variable, connectives } P = set of BDT on Interval Variables P /\ P ~P There is only a finite number of interval variables. Clausal Form: P :- x ; y ; P. P :- empty. P x /\ it is better to make BDT primitives... variablesBDT compBDT andBDT orBDT negBDT hashBDT Mon May 20 14:24:59 BST 1991 ITL decomposition Rule for Model Checker choices interval is finite / infinite interval is open / close interval is empty / non-empty ITL finite/close and has empty p,q p;q ~p p&q local variable non local variable ~(true & ~p) s0 Success: nil Failure: true & ~p decompositon( Formula , Local State, Next Intervals ) Formula -> (Local-0, empty); (Local-1, ~empty) & Next Intervals ( with eventuality ) ~empty contains eventuality (OK?) local variable p -> p,empty ; (p,~empty & true) P & Q -> (empty,P,Q); ( empty,P & ~empty,Q ); ( ~empty, P & Q ) local part should have standard form