3.4.3 时序逻辑在协议描述中的应用