Personal tools
You are here: Home Events Abstract Archives 1999 System Description, Abstraction, and Verification: A Uniform Treatment of Quality and Quantity

System Description, Abstraction, and Verification: A Uniform Treatment of Quality and Quantity

Michael Huth Department of Computing and Information Sciences Kansas State University 4pm Tuesday 27 July 1999 Room 2511, JCMB, King's Buildings

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.

Document Actions