Resumo: We study temporal properties over infinite binary redblue trees in the setting of constructive type theory. We consider several familiar pathbased properties, typical to lineartime and branchingtime temporal logics like LTL and CTL*, and the corresponding treebased properties, in the spirit of the modal mucalculus. We conduct a systematic study of the relationships of the pathbased and treebased versions of "eventually redness", "eventually always blueness" and mixed inductivecoinductive "almost always blueness". We relate these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).
We have fully formalized our development with the Coq proof assistant.
(Joint work with Marc Bezem and Tarmo Uustalu)
