{{ $t("message.ADVERTISEMENT") }}
{{ $t("message.AD_EXPIRE_DATE") }}2024年03月
文献
J-GLOBAL ID:201702243083144714   整理番号:17A0253055

有界モデル検査の高速化を指向した差分論理に基づく時間ペトリネットの論理式表現

Symbolic Representation based on Difference Logic of Time Petri Nets for Efficient Bounded Model Checking
著者 (6件):
資料名:
巻: 116  号: 426(SS2016 36-59)  ページ: 59-64  発行年: 2017年01月19日 
JST資料番号: S0532B  ISSN: 0913-5685  資料種別: 会議録 (C)
記事区分: 原著論文  発行国: 日本 (JPN)  言語: 日本語 (JA)
抄録/ポイント:
抄録/ポイント
文献の概要を数百字程度の日本語でまとめたものです。
部分表示の続きは、JDreamⅢ(有料)でご覧頂けます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。
著者らはこれまでに,SMTソルバを用いて時間ペトリネットの有界モデル検査を行うための手法を開発してきた。SMTソルバは線形制約を扱うことができるため,時間ペトリネットにおける時間制約を線形制約上の不等式によって表現することで,SMTソルバによる有界モデル検査が実現できる。ここで,「x-y∽c」という形式の不等式のみで表現される差分論理(Difference Logic)上の制約に対しては,高速な充足可能性判定アルゴリズムが存在することが知られている。そこで本稿では,時間ペトリネットの時間制約を差分論理によって表現することで,充足可能性判定に基づく有界モデル検査を高速化するための手法を提案する。(著者抄録)
シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

準シソーラス用語:
シソーラス用語/準シソーラス用語
文献のテーマを表すキーワードです。
部分表示の続きはJDreamⅢ(有料)でご覧いただけます。
J-GLOBALでは書誌(タイトル、著者名等)登載から半年以上経過後に表示されますが、医療系文献の場合はMyJ-GLOBALでのログインが必要です。

分類 (1件):
分類
JSTが定めた文献の分類名称とコードです
グラフ理論基礎 
引用文献 (18件):

前のページに戻る