## 定義 状態機械(state machine)とは、集合上の二項関係(遷移関係, transition relation)と、その集合の中で指定される開始状態(start state)からなる、段階的プロセス(step-by-step process)の抽象モデルである。集合の要素は「状態」と呼ばれ、遷移関係のグラフ表現(状態遷移グラフ, state graph)における矢印1本を遷移と呼び、状態qから状態rへの遷移をq→rと書く。各状態からの遷移先が高々1つの機械を決定性(deterministic)、複数ありうる機械を非決定性(nondeterministic)と呼ぶ。デジタル回路や文字列パターンマッチングは有限状態数の機械でモデル化されることが多く、継続的な計算過程は無限状態数の機械になりやすい。**実行(execution)**は開始状態から始まり、連続する状態対がすべて遷移関係を満たすような(有限または無限の)状態列であり、実行に現れる状態を到達可能(reachable)と呼ぶ。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.4.1, §5.4.3) 状態機械は帰納法([[帰納法]])を「段階的プロセスの各ステップで性質が保たれること」の証明に特化させた形式であり、Floydの不変条件原理([[不変条件]])と一体で用いられる。プログラム(高速べき乗算のようなレジスタ操作の列)・デジタル回路・確率過程など、離散的なステップの繰り返しで進行するあらゆる対象を状態機械としてモデル化できる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.4) ## 横断的知見 - 本conceptに現時点で紐づくソースは第5章のみであり、複数ソースの突き合わせによる知見はまだ蓄積されていない。他のソース(形式手法・モデル検査・プログラム検証系の論文や書籍)が取り込まれ次第、本節を育てる。 ## 未解決の問い - 状態機械の到達可能性判定・不変条件の自動発見は、モデル検査(model checking)やSAT/SMTベースの検証手法とどう関係するか。本章はFloydによる手作業の不変条件発見しか扱っていない。 - 非決定性状態機械(Die Hard の水差し問題のように複数の遷移先を持つ機械)の到達可能性は、決定性機械の場合と比べて証明の難度・構造がどう変わるか。 - 状態機械の「状態」を無限集合(例: レジスタ値の組)に取る場合と有限集合に取る場合とで、不変条件の発見しやすさにどのような違いが生じるか。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] - 概念: [[帰納法]] —— 状態機械の不変条件原理は帰納法を段階的プロセス向けに再定式化したもの。/ [[不変条件]] —— 状態機械上で保たれる性質を扱う姉妹concept。 ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 5.