Expressing properties of resource-bounded systems: the Logics RTL* and RTL

Computation systems and logics for modelling such systems have been studied to a great extent in the past decades. This paper introduces resources into the models of systems and discusses the Resource-Bounded Tree Logics RTL and RTL*, based on the well-known Computation Tree Logics CTL and CTL*, for reasoning about computations of such systems. We present initial results on the complexity/decidability of model checking