d your e-mail address to receive free newsletters from SCIRP.
Kwiatkowska, M., Norman, G. and Parker, D. (2011) PRISM 4.0: Verification of Probabilistic Real-Time Systems. Proceedings of the 23rd International Conference on Computer Aided Verification, LNCS 6806, Snowbird, USA, 14-20 July 2011, 585-591.
ABSTRACT: In this paper, verification of real-time pricing systems of electricity is considered using a probabilistic Boolean network (PBN). In real-time pricing systems, electricity conservation is achieved by manipulating the electricity price at each time. A PBN is widely used as a model of complex systems, and is appropriate as a model of real-time pricing systems. Using the PBN-based model, real-time pricing systems can be quantitatively analyzed. In this paper, we propose a verification method of real-time pricing systems using the PBN-based model and the probabilistic model checker PRISM. First, the PBN-based model is derived. Next, the reachability problem, which is one of the typical verification problems, is formulated, and a solution method is derived. Finally, the effectiveness of the proposed method is presented by a numerical example.