{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:09Z","timestamp":1781238909466,"version":"3.54.1"},"publisher-location":"Cham","reference-count":66,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031986840","type":"print"},{"value":"9783031986857","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,23]],"date-time":"2025-07-23T00:00:00Z","timestamp":1753228800000},"content-version":"vor","delay-in-days":203,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Linear Temporal Logic (LTL) is used widely in verification, planning, and more. Unfortunately, users often struggle to learn it. To improve their learning, they need drill, instruction, and adaptation to their strengths and weaknesses. Furthermore, this should fit into whatever learning process they are already part of (such as a course).\n<\/jats:p>\n          <jats:p>In response, we have built a <jats:italic>misconception-based<\/jats:italic> automated tutoring system. It assumes learners have a basic understanding of logic, and focuses on their understanding of LTL operators. Crucially, it takes advantage of multiple years of research (by our team, with collaborators) into misconceptions about LTL amongst both novices and experts.<\/jats:p>\n          <jats:p>The tutor generates questions using these known learner misconceptions; this enables the tutor to determine which concepts learners are strong and weak on. When learners get a question wrong, they are offered immediate feedback in terms of the concrete error they made. If they consistently demonstrate similar errors, the tool offers them feedback in terms of more general misconceptions, and tailors subsequent question sets to exercise those misconceptions.\n<\/jats:p>\n          <jats:p>The tool is hosted for free on-line, is available open source for self-hosting, and offers instructor-friendly features.<\/jats:p>","DOI":"10.1007\/978-3-031-98685-7_9","type":"book-chapter","created":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T03:31:39Z","timestamp":1753155099000},"page":"185-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Misconception-Driven Adaptive Tutor for\u00a0Linear Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7936-8147","authenticated-orcid":false,"given":"Siddhartha","family":"Prasad","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7078-9287","authenticated-orcid":false,"given":"Ben","family":"Greenman","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9377-9943","authenticated-orcid":false,"given":"Tim","family":"Nelson","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5184-1975","authenticated-orcid":false,"given":"Shriram","family":"Krishnamurthi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,23]]},"reference":[{"key":"9_CR1","doi-asserted-by":"crossref","unstructured":"Van\u00a0der Aalst, W.M., de\u00a0Beer, H.T., van Dongen, B.F.: Process mining and verification of properties: an approach based on temporal logic. In: On the Move to Meaningful Internet Systems 2005: CoopIS, DOA, and ODBASE: OTM Confederated International Conferences, CoopIS, DOA, and ODBASE 2005, Agia Napa, Cyprus, October 31-November 4, 2005, Proceedings, Part I, pp. 130\u2013147. Springer (2005)","DOI":"10.1007\/11575771_11"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Acree, A., Budd, T., Demillo, R., Lipton, R., Sayward, F.: Mutation analysis. Technical report. ADA076575, Georgia Inst. of Tech. Atlanta School of Information and Computer Science (1979). https:\/\/apps.dtic.mil\/sti\/citations\/ADA076575","DOI":"10.21236\/ADA076575"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Alur, R., Bansal, S., Bastani, O., Jothimurugan, K.: A framework for transforming specifications in reinforcement learning. In: Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, pp. 604\u2013624. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_29","DOI":"10.1007\/978-3-031-22337-2_29"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Amram, G., Bansal, S., Fried, D., Tabajara, L.M., Vardi, M.Y., Weiss, G.: Adapting behaviors via reactive synthesis. In: CAV, pp. 870\u2013893. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_41","DOI":"10.1007\/978-3-030-81685-8_41"},{"issue":"2","key":"9_CR5","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1207\/s15327809jls0402_2","volume":"4","author":"JR Anderson","year":"1995","unstructured":"Anderson, J.R., Corbett, A.T., Koedinger, K.R., Pelletier, R.: Cognitive tutors: lessons learned. J. Learn. Sci. 4(2), 167\u2013207 (1995)","journal-title":"J. Learn. Sci."},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Antoniotti, M., Mishra, B.: Discrete events models + temporal logic = supervisory controller: automatic synthesis of locomotion controllers. In: ICRA, pp. 1441\u20131446. IEEE (1995). https:\/\/doi.org\/10.1109\/ROBOT.1995.525480","DOI":"10.1109\/ROBOT.1995.525480"},{"key":"9_CR7","unstructured":"Araki, B., Li, X., Vodrahalli, K., DeCastro, J.A., Fry, M.J., Rus, D.: The logical options framework. In: ICML, vol.\u00a0139, pp. 307\u2013317. PMLR (2021). http:\/\/proceedings.mlr.press\/v139\/araki21a.html"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Babiak, T., K\u0159et\u00ednsk\u1ef3, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: Fast and more deterministic. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 95\u2013109. Springer (2012)","DOI":"10.1007\/978-3-642-28756-5_8"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y., Wells, A.: Model checking strategies from synthesis over finite traces. In: ATVA, pp. 227\u2013247. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_11","DOI":"10.1007\/978-3-031-45329-8_11"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Benny, A., Chandran, S., Kalayappan, R., Phawade, R., Kurur, P.P.: faRM-LTL: a domain-specific architecture for flexible and accelerated runtime monitoring of LTL properties. In: International Conference on Runtime Verification, pp. 109\u2013127. Springer (2024)","DOI":"10.1007\/978-3-031-74234-7_7"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Bhatia, A., Kavraki, L.E., Vardi, M.Y.: Sampling-based motion planning with temporal goals. In: ICRA, pp. 2689\u20132696. IEEE (2010). https:\/\/doi.org\/10.1109\/ROBOT.2010.5509503","DOI":"10.1109\/ROBOT.2010.5509503"},{"issue":"3","key":"9_CR12","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Brunel, J., Chemouil, D., Cunha, A., Macedo, N.: The Electrum analyzer: model checking relational first-order temporal specifications. In: ASE, pp. 884\u2013887. ACM (2018)","DOI":"10.1145\/3238147.3240475"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Ciccio, C.D., Montali, M.: Declarative process specifications: Reasoning, discovery, monitoring. In: Process Mining Handbook, Lecture Notes in Business Information Processing, vol.\u00a0448, pp. 108\u2013152. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-08848-3_4","DOI":"10.1007\/978-3-031-08848-3_4"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Cosler, M., Hahn, C., Mendoza, D., Schmitt, F., Trippel, C.: nl2spec: interactively translating unstructured natural language to temporal logics with large language models. In: CAV, pp. 383\u2013396. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18","DOI":"10.1007\/978-3-031-37703-7_18"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Cui, L., Rothkopf, R., Santolucito, M.: Towards reactive synthesis as a programming paradigm (2024). https:\/\/doi.org\/10.1184\/R1\/25587741.v1, https:\/\/kilthub.cmu.edu\/articles\/conference_contribution\/Towards_Reactive_Synthesis_as_a_Programming_Paradigm\/25587741","DOI":"10.1184\/R1\/25587741.v1"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., De\u00a0Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring business metaconstraints based on LTL and LDL for finite traces. In: BPM, pp. 1\u201317. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-10172-9_1","DOI":"10.1007\/978-3-319-10172-9_1"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Maggi, F.M., Marrella, A., Patrizi, F.: On the disruptive effectiveness of automated planning for LTLf-based trace alignment. In: Artificial Intelligence, pp.\u00a01\u20137. AAAI (2017). https:\/\/doi.org\/10.1609\/aaai.v31i1.11020","DOI":"10.1609\/aaai.v31i1.11020"},{"key":"9_CR19","unstructured":"Dortmund, T.U.: Logic WiSe 2022 (2022). https:\/\/iltis.cs.tu-dortmund.de\/Logic-WiSe2022-external\/en\/#chapterB1"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A.: Manipulating LTL formulas using Spot 1.0. In: Proceedings of the 11th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201913), pp. 442\u2013445. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_31","DOI":"10.1007\/978-3-319-02444-8_31"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: what\u2019s new? In: Proceedings of the 34th International Conference on Computer Aided Verification (CAV\u201922), Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"9_CR22","unstructured":"Dwyer, M.B.: Patterns for LTL translation (2025). https:\/\/matthewbdwyer.github.io\/psp\/patterns\/ltl.html. Accessed 08 Jan 2025"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), pp. 411\u2013420 (1999). https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: ICRA, pp. 2020\u20132025. IEEE (2005). https:\/\/doi.org\/10.1109\/ROBOT.2005.1570410","DOI":"10.1109\/ROBOT.2005.1570410"},{"issue":"13","key":"9_CR25","doi-asserted-by":"publisher","first-page":"16428","DOI":"10.1609\/aaai.v37i13.27068","volume":"37","author":"F Fuggitti","year":"2023","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL \u2013 a Python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. AAAI Conf. Artif. Intell. 37(13), 16428\u201316430 (2023). https:\/\/doi.org\/10.1609\/aaai.v37i13.27068","journal-title":"AAAI Conf. Artif. Intell."},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Geck, G., Ljulin, A., Peter, S., Schmidt, J., Vehlken, F., Zeume, T.: Introduction to ILTIS: an interactive, web-based system for teaching logic. In: ITiCSE, pp. 141\u2013146. ACM (2018). https:\/\/doi.org\/10.1145\/3197091.3197095","DOI":"10.1145\/3197091.3197095"},{"key":"9_CR27","unstructured":"Geck, G., et al.: ILTIS: teaching logic in the Web. CoRR abs\/2105.05763 (2021)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Greenman, B., et al.: Misconceptions in finite-trace and infinite-trace linear temporal logic. In: International Symposium on Formal Methods. pp. 579\u2013599. Springer (2024)","DOI":"10.1007\/978-3-031-71162-6_30"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Greenman, B., et al.: Artifact for misconceptions in finite-trace and infinite-trace linear temporal logic (2024). https:\/\/doi.org\/10.5281\/zenodo.12770102","DOI":"10.5281\/zenodo.12770102"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Greenman, B., Saarinen, S., Nelson, T., Krishnamurthi, S.: Accepted artifact for little tricky logic: misconceptions in the understanding of LTL (2022). https:\/\/doi.org\/10.5281\/zenodo.6988909","DOI":"10.5281\/zenodo.6988909"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Greenman, B., Saarinen, S., Nelson, T., Krishnamurthi, S.: Little tricky logic: misconceptions in the understanding of LTL. Programming 7(2), 7:1\u20137:37 (2023). https:\/\/doi.org\/10.22152\/programming-journal.org\/2023\/7\/7","DOI":"10.22152\/programming-journal.org\/2023\/7\/7"},{"issue":"2","key":"9_CR32","doi-asserted-by":"publisher","first-page":"3687","DOI":"10.1109\/LRA.2021.3064220","volume":"6","author":"D Gundana","year":"2021","unstructured":"Gundana, D., Kress-Gazit, H.: Event-based signal temporal logic synthesis for single and multi-robot tasks. IEEE Robot. Autom. Lett. 6(2), 3687\u20133694 (2021). https:\/\/doi.org\/10.1109\/LRA.2021.3064220","journal-title":"IEEE Robot. Autom. Lett."},{"issue":"3","key":"9_CR33","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1119\/1.2343497","volume":"30","author":"D Hestenes","year":"1992","unstructured":"Hestenes, D., Wells, M., Swackhamer, G.: Force concept inventory. Phys. Teach. 30(3), 141\u2013158 (1992). https:\/\/doi.org\/10.1119\/1.2343497","journal-title":"Phys. Teach."},{"issue":"7","key":"9_CR34","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1177\/0278364920913922","volume":"39","author":"Y Kantaros","year":"2020","unstructured":"Kantaros, Y., Zavlanos, M.M.: STyLuS$$ ^{*}$$: a temporal logic optimal control synthesis algorithm for large-scale multi-robot systems. Int. J. Robot. Res. 39(7), 812\u2013836 (2020). https:\/\/doi.org\/10.1177\/0278364920913922","journal-title":"Int. J. Robot. Res."},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Lahijanian, M., Almagor, S., Fried, D., Kavraki, L., Vardi, M.: This time the robot settles for a cost: a quantitative approach to temporal logic planning with partial satisfaction. In: AAAI, pp. 3664\u20133671. AAAI Press (2015). https:\/\/shaull.github.io\/pub\/LAFKV15.pdf","DOI":"10.1609\/aaai.v29i1.9670"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Li, R., Gurushankar, K., Heule, M.J., Rozier, K.Y.: What\u2019s in a name? linear temporal logic literally represents time lines. In: 2023 IEEE Working Conference on Software Visualization (VISSOFT), pp. 73\u201383. IEEE (2023)","DOI":"10.1109\/VISSOFT60811.2023.00018"},{"issue":"5","key":"9_CR37","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1111\/jcal.12365","volume":"35","author":"J Lodder","year":"2019","unstructured":"Lodder, J., Heeren, B., Jeuring, J.: A comparison of elaborated and restricted feedback in LogEx, a tool for teaching rewriting logical formulae. J. Comput. Assist. Learn. 35(5), 620\u2013632 (2019)","journal-title":"J. Comput. Assist. Learn."},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Lodder, J., Heeren, B., Jeuring, J.: Providing hints, next steps and feedback in a tutoring system for structural induction. arXiv preprint arXiv:2002.12552 (2020)","DOI":"10.4204\/EPTCS.313.2"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s40593-020-00222-2","volume":"31","author":"J Lodder","year":"2021","unstructured":"Lodder, J., Heeren, B., Jeuring, J., Neijenhuis, W.: Generation and use of hints and feedback in a Hilbert-style axiomatic proof tutor. Int. J. Artif. Intell. Educ. 31, 99\u2013133 (2021)","journal-title":"Int. J. Artif. Intell. Educ."},{"key":"9_CR40","doi-asserted-by":"publisher","unstructured":"Loizou, S.G., Kyriakopoulos, K.J.: Automatic synthesis of multi-agent motion tasks based on LTL specifications. In: CDC, pp. 153\u2013158. IEEE (2004). https:\/\/doi.org\/10.1109\/CDC.2004.1428622","DOI":"10.1109\/CDC.2004.1428622"},{"issue":"OOPSLA1","key":"9_CR41","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1145\/3649823","volume":"8","author":"KC Lu","year":"2024","unstructured":"Lu, K.C., Krishnamurthi, S.: Identifying and correcting programming language behavior misconceptions. Proc. ACM Program. Lang. 8(OOPSLA1), 334\u2013361 (2024)","journal-title":"Proc. ACM Program. Lang."},{"issue":"1","key":"9_CR42","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/TSE.2013.44","volume":"40","author":"L Madeyski","year":"2013","unstructured":"Madeyski, L., Orzeszyna, W., Torkar, R., Jozala, M.: Overcoming the equivalent mutant problem: a systematic literature review and a comparative experiment of second order mutation. IEEE Trans. Software Eng. 40(1), 23\u201342 (2013)","journal-title":"IEEE Trans. Software Eng."},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Maggi, F.M., Montali, M., Westergaard, M., Van Der Aalst, W.M.: Monitoring business constraints with linear temporal logic: an approach based on colored automata. In: Business Process Management: 9th International Conference, BPM 2011, Clermont-Ferrand, France, August 30-September 2, 2011. Proceedings 9. pp. 132\u2013147. Springer (2011)","DOI":"10.1007\/978-3-642-23059-2_13"},{"issue":"1","key":"9_CR44","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. TOPLAS 6(1), 68\u201393 (1984). https:\/\/doi.org\/10.1145\/357233.357237","journal-title":"TOPLAS"},{"issue":"OOPSLA1","key":"9_CR45","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/3649833","volume":"8","author":"T Nelson","year":"2024","unstructured":"Nelson, T., et al.: Forge: a tool and language for teaching formal methods. Proc. ACM Program. Lang. 8(OOPSLA1), 613\u2013641 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"9_CR46","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, L., Wickstr\u00f6m, O.: Quickstrom: property-based acceptance testing with LTL specifications. In: PLDI, pp. 1025\u20131038. ACM (2022). https:\/\/doi.org\/10.1145\/3519939.3523728","DOI":"10.1145\/3519939.3523728"},{"issue":"2","key":"9_CR47","doi-asserted-by":"publisher","first-page":"127","DOI":"10.3102\/0162373713507480","volume":"36","author":"JF Pane","year":"2014","unstructured":"Pane, J.F., Griffin, B.A., McCaffrey, D.F., Karam, R.: Effectiveness of cognitive tutor algebra I at scale. Educ. Eval. Policy Anal. 36(2), 127\u2013144 (2014)","journal-title":"Educ. Eval. Policy Anal."},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190. ACM (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"issue":"2","key":"9_CR49","first-page":"211","volume":"66","author":"GJ Posner","year":"1982","unstructured":"Posner, G.J., Strike, K.A., Hewson, P.W., Gertzog, W.A.: Accommodation of a scientific conception: toward a theory of conceptual change. Sci. Educ. 66(2), 211\u2013227 (1982)","journal-title":"Sci. Educ."},{"key":"9_CR50","doi-asserted-by":"publisher","unstructured":"Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: Conceptual mutation testing for student programming misconceptions. Art Sci. Eng. Program. 8(2) (2023). https:\/\/doi.org\/10.22152\/programming-journal.org\/2024\/8\/7","DOI":"10.22152\/programming-journal.org\/2024\/8\/7"},{"key":"9_CR51","unstructured":"Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: Hosting the LTL Tutor (2024). https:\/\/github.com\/brownplt\/LTLTutor\/wiki\/Hosting-the-LTL-Tutor"},{"key":"9_CR52","unstructured":"Prasad, S., Greenman, B., Nelson, T., Krishnamurthi, S.: LTL tutor (2024). https:\/\/github.com\/brownplt\/ltltutor"},{"key":"9_CR53","doi-asserted-by":"crossref","unstructured":"Rojas, J.M., White, T.D., Clegg, B.S., Fraser, G.: Code defenders: crowdsourcing effective tests and subtle mutants with a mutation testing game. In: 2017 IEEE\/ACM 39th International Conference on Software Engineering (ICSE), pp. 677\u2013688. IEEE (2017)","DOI":"10.1109\/ICSE.2017.68"},{"issue":"2","key":"9_CR54","doi-asserted-by":"publisher","first-page":"957","DOI":"10.1007\/s10648-021-09656-z","volume":"34","author":"NL Schroeder","year":"2022","unstructured":"Schroeder, N.L., Kucera, A.C.: Refutation text facilitates learning: a meta-analysis of between-subjects experiments. Educ. Psychol. Rev. 34(2), 957\u2013987 (2022)","journal-title":"Educ. Psychol. Rev."},{"key":"9_CR55","unstructured":"Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task specifications from demonstrations. In: NeurIPS, pp. 3808\u20133817 (2018)"},{"issue":"4","key":"9_CR56","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1093\/jigpal\/jzm026","volume":"15","author":"W Sieg","year":"2007","unstructured":"Sieg, W.: The AProS project: strategic thinking & computational logic. Logic J. IGPL 15(4), 359\u2013368 (2007)","journal-title":"Logic J. IGPL"},{"key":"9_CR57","doi-asserted-by":"publisher","unstructured":"Smith, R., Avrunin, G., Clarke, L., Osterweil, L.: PROPEL: an approach supporting property elucidation. In: Proceedings of the 24th International Conference on Software Engineering. ICSE 2002, pp. 11\u201321 (2002). https:\/\/doi.org\/10.1109\/ICSE.2002.1007952","DOI":"10.1109\/ICSE.2002.1007952"},{"key":"9_CR58","doi-asserted-by":"publisher","unstructured":"Tabajara, L.M., Vardi, M.Y.: LTLf synthesis under partial observability: from theory to practice. In: GandALF, pp. 1\u201317. Open Publishing Association (2020). https:\/\/doi.org\/10.4204\/eptcs.326.1","DOI":"10.4204\/eptcs.326.1"},{"key":"9_CR59","doi-asserted-by":"publisher","unstructured":"Tracy\u00a0II, T., Tabajara, L.M., Vardi, M., Skadron, K.: Runtime verification on FPGAs with LTLf specifications. In: FMCAD, pp. 36\u201346. IEEE Computer Society (2020). https:\/\/doi.org\/10.34727\/2020\/isbn.978-3-85448-042-6_10","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_10"},{"key":"9_CR60","doi-asserted-by":"publisher","unstructured":"Umili, E., Capobianco, R., De\u00a0Giacomo, G.: Grounding LTLf specifications in images. In: KR, pp. 45\u201363. ACM (2023). https:\/\/doi.org\/10.24963\/kr.2023\/65","DOI":"10.24963\/kr.2023\/65"},{"issue":"3","key":"9_CR61","doi-asserted-by":"publisher","first-page":"227","DOI":"10.3233\/IRG-2006-16(3)02","volume":"16","author":"K VanLehn","year":"2006","unstructured":"VanLehn, K.: The behavior of tutoring systems. Int. J. Artif. Intell. Educ. 16(3), 227\u2013265 (2006)","journal-title":"Int. J. Artif. Intell. Educ."},{"key":"9_CR62","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: 1st Symposium in Logic in Computer Science (LICS). IEEE Computer Society (1986)"},{"key":"9_CR63","unstructured":"Wang, Y., Figueroa, N., Li, S., Shah, A., Shah, J.: Temporal logic imitation: learning plan-satisficing motion policies from demonstrations. In: Conference on Robot Learning, CoRL, pp. 94\u2013105. PMLR (2022). https:\/\/proceedings.mlr.press\/v205\/wang23a.html"},{"key":"9_CR64","unstructured":"Wickstr\u00f6m, O.: LTL visualizer (2023). https:\/\/github.com\/quickstrom\/ltl-visualizer"},{"key":"9_CR65","doi-asserted-by":"publisher","unstructured":"Wongpiromsarn, T., Ulusoy, A., Belta, C., Frazzoli, E., Rus, D.: Incremental temporal logic synthesis of control policies for robots interacting with dynamic agents. In: IROS, pp. 229\u2013236. IEEE (2012). https:\/\/doi.org\/10.1109\/IROS.2012.6385575","DOI":"10.1109\/IROS.2012.6385575"},{"key":"9_CR66","doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLf synthesis. In: IJCAI, pp. 1362\u20131369 (2017). https:\/\/doi.org\/10.24963\/ijcai.2017\/189","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98685-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T17:23:07Z","timestamp":1757265787000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98685-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986840","9783031986857"],"references-count":66,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98685-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"23 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"All authors declare that they have no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}