Chapter 2　Backgrounds

To make this book self-contained，we introduce some preliminaries in this chapter，including introductions on operational semantics，proof techniques，and truly concurrent process algebra［7］，which is based on truly concurrent operational semantics.