Misconceptions In Finite-Trace and Infinite-Trace Linear Temporal Logic

We now also have an automated tutor that puts this material to work to help students directly. Over the past three years and with a multi-national group of collaborators, we have been digging deeper into misconceptions in LTL (Linear Temporal Logic) and studying misconceptions in LTLf, a promising variant of LTL restricted to finite traces. Why LTL and LTLf? Because beyond their traditional uses in verification and now robot synthesis, they support even more applications, from image processing to web-page t