Generating Type Systems for Process Graphs

In: Concurrency Theory : Proceedings of the 10th International Conference, CONCUR 1999. - (Lecture Notes in Computer Science ; 1664)
978-3-540-66425-3 Aufl. , Springer (1999), S. 352-367
Buchaufsatz / Kapitel / Fach: Informatik
We introduce a hypergraph-based process calculus with a generic type system. That is, a type system checking an invariant property of processes can be generated by instantiating the original type system. We demonstrate the key ideas behind the type system, namely that there exists a hypergraph morphism from each process graph into its type, and show how it can be used for the analysis of processes. Our examples are input/output-capabilities, secrecy conditions and avoiding vicious circles occurring in deadlocks. In order to specify the syntax and semantics of the process calculus and the type system, we introduce a method of hypergraph construction using concepts from category theory.