どうも
"From PSL to NBA: a Modular Symbolic Encoding"
によると。
LTLはTableau法にてautomatonになるけども、PSLはLTLを拡張している
からABA(Alternating Buchi Automata:universal and existential branchingが特徴)になるんだけども。
これをNBA(Non-deterministic Buchi Automata:existential branchingが特徴)に変換するという
そういう論文だった。
まだまだ勉強が必要なことがわかった。
