Model Checking with Abstraction

This Master thesis investigates the notion of process abstraction in a category theoretical framework. Using a mu-calculus (notation: L_m), invariance of certain properties under simulation is given. The results [Loiseaux et. al. 95] of preservation and reflection of properties from \Box L_m and \Diamond L_m, respectively, are shown in that context. Ideas about a categorical representation of processes with internal actions are produced, as well.

My Master thesis (Diplomarbeit) is available in German, only.


This page was last updated on 25th April 2001.