論理式肥大に伴う活性のモデル検査の非効率化の改善

Material type: 文書・図像類

Author: 緒方, 和博

Publisher: -

Publication date: 2014-04-23

Material Format: Digital

Capacity, size, etc.: -

NDC: -

View All

Notes on use

Note (General)：: 公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。この論理式はBuchiオートマトンへ変換される。この変換は論理式の大きさに対しべき乗の計算と空間を必要とするため、公平性が大きくなるとBuchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。本研究で...

Search by Bookstore

Holdings of Libraries in Japan

This page shows libraries in Japan other than the National Diet Library that hold the material.

List of Cooperating Institutions and Databases

Please contact your local library for information on how to use materials or whether it is possible to request materials from the holding libraries.

other

JAIST Repository
Digital
You can check the holdings of institutions and databases with which 学術機関リポジトリデータベース（IRDB）（機関リポジトリ） is linked at the site of 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）.
JAIST Repository

Search by Bookstore

Bibliographic Record

You can check the details of this material, its authority (keywords that refer to materials on the same subject, author's name, etc.), etc.

Digital

Material Type: 文書・図像類
Title: 論理式肥大に伴う活性のモデル検査の非効率化の改善
Author/Editor: 緒方, 和博
Author Heading: 緒方, 和博
Publication Date: 2014-04-23
Publication Date (W3CDTF): 2014-04-23
Alternative Title: Improvement of liveness model checking performance degraded by obese formulas
Periodical title: 科学研究費助成事業研究成果報告書
Pages: 1-4
Text Language Code: jpn
Subject Heading: モデル検査
活性
公平性
準公平性
分割統治
公平性の理解
反例
Maude
Target Audience: 一般
Note (General): 公平性のもとでの活性のモデル検査対象の論理式は"公平性 ⇒ 活性"の形をとる。この論理式はBuchiオートマトンへ変換される。この変換は論理式の大きさに対しべき乗の計算と空間を必要とするため、公平性が大きくなるとBuchiオートマトンへの変換が実質不可能になり、モデル検査自体もできなくなる。本研究では、"公平性 ⇒ 準公平性"を満たし、公平性より小さな論理式である準公平性を探し、"準公平性 ⇒ 活性"をモデル検査することで公平性のもとでのモデル検査を可能とする方法を提案する。すなわち、"公平性 ⇒ 活性"の代わりに、"公平性⇒ 準公平性" と"準公平性 ⇒ 活性"をモデル検査することである。 : Model checking a liveness property lprop under a fairness assumption fair, the formula is in the form "fair => lprop". The formula is transformed into a Buchi automaton. The transformation requires an exponential time and space of the size of the formula. If the formula becomes large, it becomes (almost) impossible to transform the formula into a Buchi automaton and then to model check the formula. The research proposes a way of making the model checking feasible by model checking "fair => qfair" and "qfair => lprop" for some formula qfair such that the size of qfair is (much) smaller than that of fair.
研究種目：基盤研究(C)
研究期間：2011～2013
課題番号：23500041
研究者番号：30272991
研究分野：計算機科学
科研費の分科・細目：ソフトウェア
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/12176
Format (IMT): application/pdf
Source: https://dspace.jaist.ac.jp/dspace/bitstream/10119/12176/1/23500041seika.pdf
https://dspace.jaist.ac.jp/dspace/bitstream/10119/12176/1/23500041seika.pdf
Access Restrictions: 限定公開
Data Provider (Database): 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
https://irdb.nii.ac.jp
Original Data Provider (Database): 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ