A dynamic logic for verification of synchronous models based on theorem proving

摘要

1Introduction Synchronous models,a modelling paradigm proposed along with the development of synchronous programming languages[1]in,the 198os,are well-adapted for modelling and specifying reactive systemsa.type of systems that consecutively interact with their environment at a particular environment-determined rate.In a synchronous model,system behaviours are interpreted as a sequence of reactions.