This work was supported by the University of Bialystok grants: BST447 Formalization of temporal logics in a proof-assistant.  Application to System Verification , and BST225 Database of mathematical texts checked by computer.
['Mariusz Giero']
Propositional Linear Temporal Logic with Initial Validity Semantics1