6.6 Case Study: Verified Model Checking ケーススタディとしてComputation Tree Logic(CTL)を使ったモデル検査を取り上げます。モデル検査の基礎は集合論であり、これをHOLを使って見てみます。まずpropositional dynamic logic(PDL)と呼ばれる単純な様相…