研究者情報 | 神奈川大学

タケヤマ　マコト Takeyama Makoto 武山　誠所属神奈川大学理学部情報科学科神奈川大学大学院理学研究科理学専攻（情報科学領域）職種教授
言語種別	日本語
発行・発表の年月	2005
形態種別	学術雑誌
査読	査読あり
標題	Verificaion Transition System Reduction via PVS
執筆形態	共著
掲載誌名	コンピュータソフトウェア,Vol.22,No.3
掲載区分	国内
巻・号・頁	22(3),134-145頁
著者・共著者	Osamu Takaki, Makoto Takeyama, Hirosih Watanabe
概要	We formally verify the correctness of Transition System Reduction (TSR), an algorithm used in model-checkers for temporal logics. Formalizing TSR as a function, we formulate and prove its correctness within the proof assistant PVS. We show how to use a well-ordering on a certain set in a termination proof for the loop-based TSR algorithm. We further detail TSR's partial-correctness proof. The formal framework for these proofs is a part ofour research for a rigorousverfication environment for reactive systems.