Probabilistic Symmetry Reduction for a System with Ring Buffer

Toshifusa SEKIZAWA; Takashi TOYOSHIMA; Koichi TAKAHASHI; Kazuko TAKAHASHI

doi:10.1587/transinf.E94.D.967

Probabilistic Symmetry Reduction for a System with Ring Buffer

Toshifusa SEKIZAWA, Takashi TOYOSHIMA, Koichi TAKAHASHI, Kazuko TAKAHASHI

Full Text Views

0

Cite this

Summary :

Probabilistic model checking is an emerging technology for analyzing systems which exhibit stochastic behaviors. The verification of a larger system using probabilistic model checking faces the same state explosion problem as ordinary model checking. Probabilistic symmetry reduction is a technique to tackle this problem. In this paper, we study probabilistic symmetry reduction for a system with a ring buffer which can describe various applications. A key of probabilistic symmetry reduction is identifying symmetry of states with respect to the structure of the target system. We introduce two functions; Shift_δ and Reverse to clarify such symmetry. Using these functions, we also present pseudo code to construct a quotient model. Then, we show two practical case studies; the one-dimensional Ising model and the Automatic Identification System (AIS). Behaviors of them were verified, but suffered from the state explosion problem. Through the case studies, we show that probabilistic symmetry reduction takes advantage of reducing the size of state space.

Publication: IEICE TRANSACTIONS on Information Vol.E94-D No.5 pp.967-975

Publication Date: 2011/05/01

Publicized

Online ISSN: 1745-1361

DOI: 10.1587/transinf.E94.D.967

Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)

Category: System Analysis

Cite this

Copy

Toshifusa SEKIZAWA, Takashi TOYOSHIMA, Koichi TAKAHASHI, Kazuko TAKAHASHI, "Probabilistic Symmetry Reduction for a System with Ring Buffer" in IEICE TRANSACTIONS on Information, vol. E94-D, no. 5, pp. 967-975, May 2011, doi: 10.1587/transinf.E94.D.967.
Abstract: Probabilistic model checking is an emerging technology for analyzing systems which exhibit stochastic behaviors. The verification of a larger system using probabilistic model checking faces the same state explosion problem as ordinary model checking. Probabilistic symmetry reduction is a technique to tackle this problem. In this paper, we study probabilistic symmetry reduction for a system with a ring buffer which can describe various applications. A key of probabilistic symmetry reduction is identifying symmetry of states with respect to the structure of the target system. We introduce two functions; Shift_δ and Reverse to clarify such symmetry. Using these functions, we also present pseudo code to construct a quotient model. Then, we show two practical case studies; the one-dimensional Ising model and the Automatic Identification System (AIS). Behaviors of them were verified, but suffered from the state explosion problem. Through the case studies, we show that probabilistic symmetry reduction takes advantage of reducing the size of state space.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E94.D.967/_p

Copy

@ARTICLE{e94-d_5_967,
author={Toshifusa SEKIZAWA, Takashi TOYOSHIMA, Koichi TAKAHASHI, Kazuko TAKAHASHI, },
journal={IEICE TRANSACTIONS on Information},
title={Probabilistic Symmetry Reduction for a System with Ring Buffer},
year={2011},
volume={E94-D},
number={5},
pages={967-975},
abstract={Probabilistic model checking is an emerging technology for analyzing systems which exhibit stochastic behaviors. The verification of a larger system using probabilistic model checking faces the same state explosion problem as ordinary model checking. Probabilistic symmetry reduction is a technique to tackle this problem. In this paper, we study probabilistic symmetry reduction for a system with a ring buffer which can describe various applications. A key of probabilistic symmetry reduction is identifying symmetry of states with respect to the structure of the target system. We introduce two functions; Shift_δ and Reverse to clarify such symmetry. Using these functions, we also present pseudo code to construct a quotient model. Then, we show two practical case studies; the one-dimensional Ising model and the Automatic Identification System (AIS). Behaviors of them were verified, but suffered from the state explosion problem. Through the case studies, we show that probabilistic symmetry reduction takes advantage of reducing the size of state space.},
keywords={},
doi={10.1587/transinf.E94.D.967},
ISSN={1745-1361},
month={May},}

Copy

TY - JOUR
TI - Probabilistic Symmetry Reduction for a System with Ring Buffer
T2 - IEICE TRANSACTIONS on Information
SP - 967
EP - 975
AU - Toshifusa SEKIZAWA
AU - Takashi TOYOSHIMA
AU - Koichi TAKAHASHI
AU - Kazuko TAKAHASHI
PY - 2011
DO - 10.1587/transinf.E94.D.967
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E94-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2011
AB - Probabilistic model checking is an emerging technology for analyzing systems which exhibit stochastic behaviors. The verification of a larger system using probabilistic model checking faces the same state explosion problem as ordinary model checking. Probabilistic symmetry reduction is a technique to tackle this problem. In this paper, we study probabilistic symmetry reduction for a system with a ring buffer which can describe various applications. A key of probabilistic symmetry reduction is identifying symmetry of states with respect to the structure of the target system. We introduce two functions; Shift_δ and Reverse to clarify such symmetry. Using these functions, we also present pseudo code to construct a quotient model. Then, we show two practical case studies; the one-dimensional Ising model and the Automatic Identification System (AIS). Behaviors of them were verified, but suffered from the state explosion problem. Through the case studies, we show that probabilistic symmetry reduction takes advantage of reducing the size of state space.
ER -