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.

Diplomarbeit.dvi.gz (approx. 95 kByte)
Diplomarbeit.ps.gz (approx. 310 kByte)

This page was last updated on 25th April 2001.