フォロー
最後の段落しか読んでなかった
unboundとは。temporal logicも雰囲気しかわからない
> impossible to write an unbound model
->
> guaranteed that every spec is over a finite state space
REPLはそう
感覚では、Eventuallyのような性質はリミットなしには有限ステップでグラフの到達性を調べる問いに変換できそうにない