A Structured Temporal Logic Language:XYZ/SE

In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZsystem,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is thebasis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate forproving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that everyXYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a generalcompositional verification method in the XYZ system concerning the sequential case.