離散確率分布を持つリアルタイムシステムの確率時間双模倣関係と確率時間時相論理式の保存

IPSJ Web Site 20 References

Bibliographic Information

Other Title
  • リサン カクリツ ブンプ オ モツ リアルタイム システム ノ カクリツ ジカンソウモホウ カンケイ ト カクリツ ジカンジソウ ロンリシキ ノ ホゾン
  • Probabilistic Timed Bisimulation Relation and Its Preservation of Probabilistic Timed CTL Formulas of Real-time Systems with Discrete Probability Distributions
  • 設計手法

Search this article

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. Espe-cialy, 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 meth-ods to stepwise refinement. In this paper, we define genral 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.

Journal

References(20)*help

See more

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top