On the Use of Model and Logical Embeddings for Model Checking of Probabilistic Systems

Logics for probabilistic process algebraic models are either not very expressive or cannot be intuitively used for specifying interesting performance and reliability properties due to the presence of fixed-point operators. Moreover, the model checking machinery for these logics is very limited and is not as efficient as their state-based counterparts. Recently, new probabilistic logics and a formal framework of embeddings has been proposed which enables one to seamlessly move between state and action-based probabilistic logics. Similarly, this framework also bridges the gap between these two modeling communities by relating the state and action-based probabilistic models. We focus on implementing this framework and studying the effect of applying it on several interesting case studies from the process algebraic domain. Our results show that it enables one to efficiently verify probabilistic process algebraic models using tools and methods developed in the state-based setting. Additionally, it also enables analyzing and model checking interesting reward-based properties.