This paper proposes a formal selection framework of multiple navigation behaviors for a service robot. In our approach, modeling, analysis, and performance evaluation are carried out based on the Generalized Stochastic Petri Nets (GSPN). By adopting probabilistic approach, our framework helps the robot to select the most desirable navigation behavior in run time according to environmental conditions. Moreover, after a mission, the robot evaluates prior navigation performance from accumulated data, and uses the results for the improvement of future operations. Also, GSPN has several advantages over classic automata or direct use of Markov Process. The basic ideas of the framework were introduced in our previous work . Thus, this paper focuses on experimental verification by implementing the framework into the guide robot Jinny. We conduct the experiments about real guidance tasks with visitors in the National Science Museum of Korea. The results show that the proposed strategy is useful to select an appropriate navigation behavior in a dynamic space.