Abstract

We build on the established work on modal transition systems and probabilistic specifications to sketch a framework in which system descriptions, abstraction, and finite-state model checking all have a uniform presentation across various levels of qualitative and quantitative views together with mediating abstraction and concretization maps. We prove safety results for abstractions within and across such views for the ``forall fragment'' of the modal mu-calculus and show that they allow for some compositional reasoning with respect to a process algebra `a la CCS.