An executable temporal logic to express safety properties and its connection with the language Lustre

Abstract:
This paper studies the expressive power of the synchronous data-flow language Lustre as a specification language, and its connection with temporal logic. After a brief overview of Lustre, we define a temporal logic, called SL, which is shown to have exactly the expressive power of regular safety properties. Directly inspired from Boolean Lustre, this logic is executable, in the sense that the accepting automaton of any SL formula can be constructed "on the fly", as the model is read. Then we consider a fragment of SL, called DSL, for the formulas of which the accepting automaton built by the previous technique is deterministic. DSL is shown to have the same expressive power as SL, and to be equivalent to Boolean Lustre.

Reference:

   @INPROCEEDINGS{islip93,
      AUTHOR={N. Halbwachs and J.-C. Fernandez and A. Bouajjanni},
      TITLE={An executable temporal logic to express safety properties 
            and its connection with the language Lustre},
      BOOKTITLE={Sixth International Symp. on Lucid and Intensional
               Programming, ISLIP'93, Quebec},
      MONTH={April },
      YEAR= 1993
   }

Postscript file