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

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

クリプキフレーム 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は組として定義される。ここで、は長さの上の語で、は長さのマッチング関係である。 マッチング関…