Clovis Eberhart (NII, Japon), A Compositional Approach to Verification Models

Abstract

We present a compositional approach to graph-like verification models (e.g., parity games, Markov decision processes, or Petri nets) based on "open" structures. Such open structures are graphs with potentially dangling edges called "open ends", and which form interfaces along which open structures can be composed. We thus define a syntactic category of interfaces and open structures between them. We then define a semantic category representic relevant information about the structure (e.g., a category of probabilistic rewards). Finding an interpretation functor from the syntactic category to the semantic one shows that these structures' sematics can be computed compositionally.