モナ★MONAのこと - トアル電算室ノ業務日誌★モナMONAのこと MONA （http://www.brics.dk/mona/） は式を有限オートマトンに変換するツール。 検索パターンや時相論理の属性値を持つようなリアクティブシステム（こっちからなんかすると反応が返ってくるようなシステムのこと）やパーズ木（ 解析木-構文分析の結果を図示したもの）の制約を表すようなものを対象としている。 MONAは変換したオートマトンを分析してそれが妥当であるとか、あるいは反例（仮説に反対の論拠として用いられる反事実, 反証のこと）を出力してくれるありがたいツールだ。 MONAには１つあるいは２つのsuccessor関数の弱二次理論（Weak Second-order Theory）を決定手続きを取得する機能を持っている。 １つのsuccessor理論は一般的にはWS1Sと略されているもので、自然数の有限集合を二階量化子で拡張。successor関
