# CbC

プログラムをcode とdata に分けて記述され、軽量継続によって繋がれる。 そのため、状態遷移記述になる 状態遷移記述にはタブロー展開が有効

# タブロー展開と線形時相論理

# CbCでのタブロー展開は

プログラムの可能な実行の組み合わせを全て調べる 状態の探索は深さ有線探索(Depth First Search) プログラムの実行によって生成される状態は木構造で記述される 同じ状態は共有される->Partial Order Reduction（半順序簡約)

# partial Order Reduciton

並列システムのモデルの１つ 大まかに並列なプロセスを忠実にモデルにする化する方法とインターリビングモデルがある インターリビングは

• 並列実行されるイベントは任意の順序で現れる

• 並列なプロセスを線形順序の実行系列として表現する。

さらにこのインターリビングモデルの中で、同一の並列プロセスを表している実行系列を簡約するこ事を Partial order Reduciton（半順序簡約)という

# 線形時相論理（LtL)とは

そもそも時相論理とは時間と真偽の組み合わせのこと。 例えば、「私はそのうちお腹がすく」 これは今は」お腹が空いている」は偽であるが、時間経過があると真になるということ 線形時相論理はこの時間経過の状態を増やしたものである 何らかの状態であったなら、時間経過によって真になるといったもの（状態を証明だと様相という） 例えば「requestがあればいずれは受理する」（G(requested⊃F acknowledged)といったもの

*　タブロー展開で状態(様相)を洗い出し、それらを繋ぎ合わせて線形時相論理に基づいて記述する事で検証を行う。

# 参考にしたページ

線形時相論理。 http://www.cs.tsukuba.ac.jp/~mizutani/under_grad/programtheory/2014/2014-09.pdf partial order reduction http://hagi.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/jpf/por.pdf