最後の段落しか読んでなかった
unboundとは。temporal logicも雰囲気しかわからない
> impossible to write an unbound model
->
> guaranteed that every spec is over a finite state space
REPLはそう
感覚では、Eventuallyのような性質はリミットなしには有限ステップでグラフの到達性を調べる問いに変換できそうにない
最後の段落しか読んでなかった
unboundとは。temporal logicも雰囲気しかわからない
> impossible to write an unbound model
->
> guaranteed that every spec is over a finite state space
REPLはそう
感覚では、Eventuallyのような性質はリミットなしには有限ステップでグラフの到達性を調べる問いに変換できそうにない
$15するのか
Using lightweight modeling to understand chord
https://dl.acm.org/doi/10.1145/2185376.2185383