ABSTRACT Robotic systems operating in dynamic and uncertain environments increasingly require planners that satisfy complex task sequences whilst adhering to strict temporal constraints. Metric interval temporal logic (MITL) offers a formal and expressive framework for specifying such time‐bounded requirements; however, integrating MITL with reinforcement learning (RL) remains challenging due to stochastic dynamics and partial observability. This paper presents an unified automata‐based RL framework for synthesising policies in both Markov decision processes (MDPs) and partially observable Markov decision processes (POMDPs) under MITL specifications. MITL formulae are translated into timed limit‐deterministic generalised Büchi automata (Timed‐LDGBA) and synchronized with the underlying decision process to construct product timed models suitable for Q‐learning. A simple yet expressive reward structure enforces temporal correctness whilst allowing additional performance objectives. The approach is validated in three simulation studies: a grid‐world formulated as an MDP, a grid‐world formulated as a POMDP and an office‐like service‐robot scenario. Results demonstrate that the proposed framework consistently learns policies that satisfy strict time‐bounded requirements under stochastic transitions, scales to larger state spaces and remains effective in partially observable environments, highlighting its potential for reliable robotic planning in time‐critical and uncertain settings.
Wang et al. (Tue,) studied this question.