As reinforcement learning methods increasingly amass accomplishments, theneed for comprehending their solutions becomes more crucial. Most explainablereinforcement learning (XRL) methods generate a static explanation depictingtheir developers' intuition of what should be explained and how. In contrast,literature from the social sciences proposes that meaningful explanations arestructured as a dialog between the explainer and the explainee, suggesting amore active role for the user and her communication with the agent. In thispaper, we present ASQ-IT -- an interactive tool that presents video clips ofthe agent acting in its environment based on queries given by the user thatdescribe temporal properties of behaviors of interest. Our approach is based onformal methods: queries in ASQ-IT's user interface map to a fragment of LinearTemporal Logic over finite traces (LTLf), which we developed, and our algorithmfor query processing is based on automata theory. User studies show thatend-users can understand and formulate queries in ASQ-IT, and that using ASQ-ITassists users in identifying faulty agent behaviors.