WEKO3
インデックスリンク
アイテム
離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時同時相論理式の保存 (設計手法)
http://hdl.handle.net/2297/23624
http://hdl.handle.net/2297/236245ccdf6f2-1056-459f-895b-7edf3f9f6555
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
TE-PR-YAMANE-S-1367.pdf (803.2 kB)
|
|
| Item type | 学術雑誌論文 / Journal Article(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2017-10-03 | |||||
| タイトル | ||||||
| タイトル | 離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時同時相論理式の保存 (設計手法) | |||||
| タイトル | ||||||
| タイトル | Probabilistic Timed Bisimulation Relation and Its Preservation of Probabilistic Timed CTL Formulas of Real-time Systems with Discrete Probability Distributions (Design Methodologies) | |||||
| 言語 | en | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||
| 資源タイプ | journal article | |||||
| 著者 |
山根, 智
× 山根, 智 |
|||||
| 提供者所属 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 金沢大学理工研究域電子情報学系 | |||||
| 書誌情報 |
Transactions of Information Processing Society of Japan = 情報処理学会論文誌 巻 45, 号 5, p. 1367-1375, 発行日 2004-05-15 |
|||||
| ISSN | ||||||
| 収録物識別子タイプ | ISSN | |||||
| 収録物識別子 | 0387-5806 | |||||
| NCID | ||||||
| 収録物識別子タイプ | NCID | |||||
| 収録物識別子 | AN00116647 | |||||
| 出版者 | ||||||
| 出版者 | Information Processing Society of Japan (IPSJ) = 情報処理学会 | |||||
| 抄録 | ||||||
| 内容記述タイプ | Abstract | |||||
| 内容記述 | 近年,世界中で,リアルタイムシステムの仕様記述と検証の研究は大変にさかんである.リアルタイムシステムの仕様記述言語としては,タイミング制約が記述可能な時間オートマトンが定着しており,その検証手法としてもモデル検査手法などが開発されている.とりわけ,最近,リアルタイムシステムの不確かな動作を表現するために,離散確率分布を持つ確率時間オートマトンが開発されており,そのモデル検査手法も開発されている.さらに,最近,我々は確率時間オートマトンの確率時間模倣関係を間発して,段階的詳細化開発へ適用した.本論文では,より一般的な確率時間双模倣関係を新たに定義して,その確率時間双模倣関係にある2つの確率時間オートマトンは確率時間時相論理式の同じ集合を満たすことを示す.この種の双模倣関係は確率時間オートマトンの抽象化を保証するための重要な道具となりうる. Many people have studied formal specification and verification methods of real-time systems all over the world. We generally specify real-time systems using timed automata, and verify them using model-checking. Tiemd automata are augmented with a finite set of clocks. Especialy, recently, probabilistic timed automata and their model-checking have been developed in order to express the relative likelihood of the system exhibiting certain behavior. Moreover, we have developed probabilistic timed simulation relation and applied our proposed methods to stepwise refinement. In this paper, we define general probabilistic timed bisimulation relation, and we show that two probabilistic timed bisimular probabilistic timed automata must satisfy the same set of probabilistic timed CTL formulas. This kind of bisimularity is a valuable tool to guarantee abstractions of probabilistic timed automata. | |||||
| 権利 | ||||||
| 権利情報 | 本文データは情報処理学会の許諾に基づきCiNiiから複製したものである | |||||
| 著者版フラグ | ||||||
| 出版タイプ | VoR | |||||
| 出版タイプResource | http://purl.org/coar/version/c_970fb48d4fbd8a85 | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://www.ipsj.or.jp/ | |||||
| 関連URI | ||||||
| 識別子タイプ | URI | |||||
| 関連識別子 | http://ci.nii.ac.jp/naid/110002712186/en/ | |||||
