Embeddings Between State and Action Based Probabilistic Logics

This paper defines embeddings between state-based and action-based probabilistic logics which can be used to support probabilistic model checking. First, we propose the syntax and semantics of an action-based Probabilistic Computation Tree Logic (APCTL) and an action-based PCTL* (APCTL*) interpreted over action-labeled discretetime Markov chains (ADTMCs). We show that both these logics are strictly more expressive than the probabilistic variant of Hennessy-Milner logic (prHML). Next, we define an embedding aldl which can be used to construct an APCTL* formula from a PCTL* formula and an embedding sldl from APCTL* formula to PCTL* formula. Similarly, we define the embeddings ale and sldr from PCTL to APCTL and APCTL to PCTL, respectively. Finally, we prove that our logical embeddings combined with the model embeddings enable one to minimize, analyze and verify probabilistic models in one domain using state-of-the-art tools and techniques developed for the other domain.