Probability meets Non-Probability via Complete IL-Semirings

This thesis aims to provide a path to abstraction between probabilistic systems and non-probabilistic systems in order to put the verification methods for probabilistic systems into practical use. McIver et al have introduced a verification method for probabilistic systems using probabilistic Kleene algebras and their model of probabilistic systems. However it is difficult to put their method in practical use because their model of probabilistic systems still includes probabilistic components. Thus we have to find more abstract semantic domain excluded probabilistic components in order to enable their verification method to be put into practical use. This thesis offers multirelations — extended binary relations — as that abstract domain for probabilistic systems. And we generalize the model of probabilistic systems as probabilistic multirelations, then we consider probabilistic multirelations and non-probabilistic multirelations via an algebra called complete IL-semiring. Giving several Galois connections between them, we begin walking to abstraction for probabilistic systems.理工学研究科博士論文 (理学) ; 学位取得日: 平成24年3月23