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