Model checking memoryful linear-time logics over one-counter automata