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

Graphical abstract

References

[1] Benveniste A , Caspi P , Edwards S A , Halbwachs N , Le Guernic P , de Simone R . The synchronous languages 12 years later. Proceedings of the IEEE, 2003, 91( 1): 64– 83

[2] Harel D Kozen D Tiuryn J. Dynamic Logic. MIT Press, 2000

[3] Harel D. First-Order Dynamic Logic. Berlin: Springer, 1979

[4] Platzer A. A temporal dynamic logic for verifying hybrid system invariants. In: Proceedings of International Symposium on Logical Foundations of Computer Science. 2007, 457– 471

[5] Berry G. The constructive semantics of pure Esterel draft version 3. See Citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.2076.website, 1999

Acknowledgements

This work was partially supported by the Youth Project of National Natural Science Foundation of China (62102329), the Project of Natural Science Foundation of Chongqing (cstc2021jcyj-bsh0204), the Capacity Development Grant of Southwest University (SWU116007), and the Key Projects of National Natural Science Foundation of China (61732019, 62032019).

Supporting Information

The supporting information is available online at journal.hep.cn and link.springer.com.

RIGHTS & PERMISSIONS

2022 Higher Education Press