Embeddings Between State and Action Based Probabilistic Logics
Presenter: Susmoy Das
Session Chair: Clemens Dubslaff
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 discrete time 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 aldl′ and sldl′ 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.