WP1: Exploiting Modularity and Compositionality CAP WP1 consists of four workpackages. WP1.T1: Assume-Guarantee Reasoning [THU] WP1.T2: Linear-Time Properties [ISCAS] WP1.T3: Compositional Verification Methods for Probabilistic Hybrid Systems [RWTH] WP1.T4: Minimization for Markov Automata [SAU]