Buchi Automatonあれこれ 思いつき次第追記していきます Emptiness checking Buchi Automatonが受理する言語が空でない 初期状態から到達可能かつサイクル上にある終状態が存在する. 効率的なアルゴリズム オートマトンを有向グラフとみなし強連結成分に分け…

Tree automata 今回は(one way) tree automataの話です. ざっくり直感的な説明をするなら、木構造をした入力テープ上を走査(ただし今回はone wayなので逆走したりはしない)して、そこに書かれたアルファベットを入力として読んでいき状態遷移するようなオー…

Propositional Dynamic Logic of Looping and Converse 注意 : 本記事は記事の体をなさぬ自分用メモです。したがってわかりやすさ等について一切の配慮をしておりません。内容を整理し記事の体をなすようになれば「記事の体をなさぬメモ」タグを外します。 I…

論理とか文法とかあれこれの表現力のメモ[未整理] regular language < linear language < context free

クリプキフレーム Kripke frame そう言えばクリプキフレームの話を書いていなかった事を思い出したり(クリプキフレームの話なんて素敵なpdf (http://www.is.titech.ac.jp/~kashima/manuscript/03Sept.pdf )がネット上に溢れているので、わざわざ書くようなこ…

2-way 決定性有限オートマトン[2DFA] 直感的な説明をすると, 入力文字列を2方向に走査できるオートマトン。通常のオートマトンでは, キャラクタを受け取るとそのキャラクタと, 現在の状態から次の状態を決定する。その流れは2DFAでも同様に行われるが, 2DFA…

Visibly Pushdown Automaton (VPA) nested wordをアクセプトするオートマトンをnested wordオートマトンという。VPAはnested wordオートマトンと等価な普通の(nested wordでない)語を受理するオートマトン。 nested wordオートマトンと関係がありそうだなあ……

Nested word 直感的には、XMLのような構造や、callイベントやretイベントを持つトレースをイメージすると良いかと. 定義 アルファベット上の長さのnested wordは組として定義される。ここで、は長さの上の語で、は長さのマッチング関係である。 マッチング関…

動的命題論理(PDL)について調べていて分かりやすい日本語文献があったので、シェアしておきます。 ci.nii.ac.jp

当ブログ最初の記事ですが, 初っ端から論文紹介です。 (挨拶記事だけ書いてブログに飽きるというジンクスを回避したい…) 以降も,こんな感じで面白いなと思った論文や記事の紹介,解説をしていく感じになると思います(続けば) ざっくり説明するので,しっかり理…