平成 23 年東北地区高等専門学校専攻科研究発表交流会 講演番号 T11－C03 モデル検査器 NuSMV を用いたオントロジーの検証 ○阿部 雄貴 小林 秀幸 高橋 薫 仙台高等専門学校 １．はじめに オントロジーの記述は人手で行うこ とが大半であり，その中には構文的矛盾や意味的な間 違い，一貫性が保たれていない記述が含まれている可 能性がある．そのため，記述したオントロジーの内容 を検証する必要がある．文献[1]ではオントロジーを形 式化したグラフで表現し，素である関係と補集合の関 係に着目し，構文に関する検証を行っている．しかし 意味的矛盾に関する検証は難しい． 本稿では，ソフトウェアや組み込みシステムの検証 において有効なモデル検査の手法をオントロジーの検 証に応用し，構文的な矛盾や意味的矛盾を含んだオン トロジーの検証を行う．モデル検査ツールとしては NuSMV[2]を用いる． 検証内容：男が誰かの姉（妹）として記述されている この検証式を満たさない場合，反例（図２）が出力 され，この反例を解析することにより，修正を行うこ とができる． ４．おわりに 本稿ではモデル検査器 NuSMV を用 いてオントロジーの検証を行うための変換や検証方法 について述べた．モデル検査器を用いたことにより， 出力された反例を矛盾の手掛かりとすることができた． 今後はオントロジーを NuSMV へ入力し，検証をサポ ートする検証ツールを実装する予定である． オントロジ- rdfs:subClassOf Human Woman rdf:type Alice rdfs:subClassOf Man hasBrother, hasSister rdf:type hasSister Bob 状態遷移モデル owl:Thing, empty, hasSubClass, S, -, -, - Human, empty, hasSubClass, O, -, -, Man, empty, hasSubClass, O, -, -, - Human, empty, hasSubClass, S, -, -, - Woman, empty, hasSubClass, O, -, -, - ・・・ ３．検証例 本節では意味的矛盾を含んだオントロ ジーを例に検証を行う．図１に矛盾を含んだオントロ ジーと，前節で述べた規則に従い，変換した状態遷移 モデルを示す．この例では，Man クラスのインスタン スが「姉（妹）である」と記述されているため，矛盾 が生じている．次に，この状態遷移モデルと以下の検 証内容を表現した検証式を NuSMV へ入力し，検証を 行う．検証式は CTL 時相論理式を用いて表現する． EX (so=o & c=Man & p=hasSister)) ・・・ ２．オントロジーの状態遷移モデル 本節では，オ ントロジーを NuSMV で扱うための検証用のモデル， 状態遷移モデルについて述べる．NuSMV で扱うモデ ルはラベル無し状態遷移系であり，単純な対応付けで は元のオントロジーが持つ関連性を損なうことが考え られる．また検証内容に対する反例の出力を用いるこ とでオントロジーの誤りに対する修正の手掛かりを得 ることができるため，これらを考慮し状態遷移モデル へと変換を行う必要がある． 状態遷移モデルでは，オントロジーのトリプルを主 語と目的語を表す 2 つの状態に分け表現する．クラス とインスタンスを別々の変数で表すことにより，それ ぞれの関係性に対し検証を行うことができる．また， オントロジーではクラス演算や値に関する制約を記述 することができるため，クラス演算等を表現するため にクラス演算子に関する変数や制約条件を表す変数な どを加え，状態遷移モデルへ変換を行う． 検証式： AG !(so=s & i !=empty & 図 1 矛盾を含んだオントロジーと状態遷移モデル 図 2 反例の出力 【参考文献】 [1] S. C. Lam, D. Sleeman and W. Vasconcelos, “Graph-Based Ontology Checking”, Proceedings KCAP05 Workshop on Ontology Management: Searching, Selection, Ranking and Segmentation, pp. 33-40, 2005. [2] A. Cimatti, et. al., “NuSMV: A New Symbolic Model Verifier ”, LNCS, Vol.1633, pp.495–499,1999.
© Copyright 2024 ExpyDoc
