キノシタ ヨシキ   Kinoshita Yoshiki
  木下 佳樹
   所属   神奈川大学  情報学部 計算機科学科
    神奈川大学大学院  理学研究科 理学専攻(情報科学領域)
   職種   教授
言語種別 日本語
発行・発表の年月 2009/04
形態種別 学術雑誌
査読 査読あり
標題 An algebraic semantics of predicate abstraction for PML
執筆形態 共著
掲載誌名 Computer Software (Iwanami shoten)
巻・号・頁 26(2),147-156頁
著者・共著者 Koki Nishizawa and Yoshiki Kinoshita
概要 We give a semantics of abstraction in PML (Pointer Manipulation Language) given by Takahashi et al.. This is an instance of unifying theory for abstraction of reactive systems given by the second author et al., as every model of PML induces a model of Rμ, a modal logic with fixpoints studied by the second author. It gives the proof of the correctness of predicate abstraction used in MLAT.