Autonomous robots are becoming increasingly popular and such systems has led to complex design and analysis which brings the necessity of validation and verification. In particular, symbolic robot motion planning based on formal methods is verifiably correct. It is the process of specifying and planning robot tasks in a discrete space, then carrying them out in a continuous space in a manner that preserves the discrete-level task specifications. Despite progress in symbolic motion planning, many challenges remain, including addressing scalability for multi-robot systems and improving solutions by incorporating human intelligence in an adaptive fashion. On the other hand, extant works in human-robot interaction (HRI) often lack quantitative models and real-time analytical approaches. Here, we summarize our recent works on symbolic robot motion planning with human-in-the-loop as a step toward addressing these challenges. We specially focus on human trust in autonomous robots and embed trust analysis into the symbolic robot motion planning.