Priorian temporal logics of trees I: axiomatizing logics of some classes of non-discrete trees

Abstract We present complete axiomatizations for the Priorian temporal logics of the class of all irreflexive trees, the class of all reflexive trees, as well as various classes of reflexive and irreflexive unbounded and dense trees, including trees with branches isomorphic to the rational numbers, and to the real numbers with both there strict and non-strict orderings. We introduce new model constructions including the refinement of a bidirectional transitive filtration, unfolding, and unrolling. We establish the finite model property for all logics considered and thereby prove their decidability.