IEICE Trans - Probabilistic Symmetry Reduction for a System with Ring Buffer

Probabilistic Symmetry Reduction for a System with Ring Buffer

Toshifusa SEKIZAWA  Takashi TOYOSHIMA  Koichi TAKAHASHI  Kazuko TAKAHASHI

Publication
IEICE TRANSACTIONS on Information and Systems   Vol.E94-D    No.5    pp.967-975
Publication Date: 2011/05/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E94.D.967
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: System Analysis
Keyword:
probabilistic symmetry reduction,  ring buffer,  model checking,  the Ising model,  AIS,

Full Text: PDF>>

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.