Issues in Type Checking
Usages of channels:must be explicitly specified by programmers
Reliability of usages:can be automatically checked(by a co-inductive method)
Time tag ordering:can be automatically inferred(by generation & satisfaction of constraints)