{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,14]],"date-time":"2026-06-14T06:00:48Z","timestamp":1781416848121,"version":"3.54.1"},"publisher-location":"Cham","reference-count":71,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"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><jats:p>With the growing use of temporal logics in areas ranging from robot planning to runtime verification, it is critical that users have a clear understanding of what a specification means. Toward this end, we have been developing\u00a0a catalog of semantic errors and a suite of test instruments targeting various user-groups. The catalog is of interest to educators, to logic designers, to formula authors, and to tool builders, e.g., to identify mistakes. The test instruments are suitable for classroom teaching or self-study.<\/jats:p><jats:p>This paper reports on five sets of survey data collected over a three-year span. We study misconceptions about finite-trace <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {ltl}_{f}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mstyle>\n                      <mml:mi>L<\/mml:mi>\n                      <mml:mi>T<\/mml:mi>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mi>f<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> in\u00a0three <jats:sc>ltl<\/jats:sc>-aware audiences, and misconceptions about standard <jats:sc>ltl<\/jats:sc> in novices. We find several mistakes, even among experts. In addition, the\u00a0data supports several categories of errors in both <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsc {ltl}_{f}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mstyle>\n                      <mml:mi>L<\/mml:mi>\n                      <mml:mi>T<\/mml:mi>\n                      <mml:mi>L<\/mml:mi>\n                    <\/mml:mstyle>\n                    <mml:mi>f<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and <jats:sc>ltl<\/jats:sc> that\u00a0have not been identified in prior work. These findings, based on data from actual users, offer insights into what <jats:italic>specific ways<\/jats:italic> temporal logics\u00a0are tricky and provide a groundwork for future interventions.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_30","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"579-599","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Misconceptions in\u00a0Finite-Trace and\u00a0Infinite-Trace Linear Temporal Logic"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7078-9287","authenticated-orcid":false,"given":"Ben","family":"Greenman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7936-8147","authenticated-orcid":false,"given":"Siddhartha","family":"Prasad","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5475-2978","authenticated-orcid":false,"given":"Antonio","family":"Di Stasio","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5922-8750","authenticated-orcid":false,"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9680-7658","authenticated-orcid":false,"given":"Giuseppe","family":"De Giacomo","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8021-3430","authenticated-orcid":false,"given":"Marco","family":"Montali","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-0002-4823-8937","authenticated-orcid":false,"given":"Milda","family":"Zizyte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"issue":"4","key":"30_CR1","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1145\/1189136.1189182","volume":"38","author":"VL Almstrum","year":"2006","unstructured":"Almstrum, V.L., et al.: Concept inventories in computer science for the topic discrete mathematics. ACM SIGCSE Bull. 38(4), 132\u2013145 (2006). https:\/\/doi.org\/10.1145\/1189136.1189182","journal-title":"ACM SIGCSE Bull."},{"key":"30_CR2","unstructured":"Alur, R., Bansal, S., Bastani, O., Jothimurugan, K.: A framework for transforming specifications in reinforcement learning. CoRR abs\/2111.00272 (2021). https:\/\/arxiv.org\/abs\/2111.00272"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"870","DOI":"10.1007\/978-3-030-81685-8_41","volume-title":"Computer Aided Verification","author":"G Amram","year":"2021","unstructured":"Amram, G., Bansal, S., Fried, D., Tabajara, L.M., Vardi, M.Y., Weiss, G.: Adapting behaviors via reactive synthesis. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 870\u2013893. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_41"},{"key":"30_CR4","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":"30_CR5","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":"30_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-46002-0_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Armoni","year":"2002","unstructured":"Armoni, R., et al.: The ForSpec temporal logic: a new temporal property-specification language. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 296\u2013311. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46002-0_21"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-031-45329-8_11","volume-title":"Automated Technology for Verification and Analysis - ATVA 2023","author":"S Bansal","year":"2023","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y., Wells, A.: Model checking strategies from synthesis over finite traces. In: Andr\u00e9, \u00c9., Sun, J. (eds.) ATVA 2023. LNCS, vol. 14215, pp. 227\u2013247. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-45329-8_11"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Computer Aided Verification","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Fisman, D., Gringauze, A., Rodeh, Y.: The temporal logic sugar. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 363\u2013367. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44585-4_33"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Computer Aided Verification","author":"I Beer","year":"1997","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 279\u2013290. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63166-6_28"},{"key":"30_CR10","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":"30_CR11","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":"30_CR12","doi-asserted-by":"publisher","unstructured":"Brunello, A., Montanari, A., Reynolds, M.: Synthesis of LTL formulas from natural language texts: state of the art and research directions. In: TIME, vol.\u00a0147, pp. 17:1\u201317:19. Schloss Dagstuhl (2019). https:\/\/doi.org\/10.4230\/LIPIcs.TIME.2019.17","DOI":"10.4230\/LIPIcs.TIME.2019.17"},{"key":"30_CR13","doi-asserted-by":"publisher","unstructured":"Camacho, A., McIlraith, S.A.: Strong fully observable non-deterministic planning with LTL and LTLf goals. In: IJCAI, pp. 5523\u20135531. ijcai.org (2019). https:\/\/doi.org\/10.24963\/IJCAI.2019\/767","DOI":"10.24963\/IJCAI.2019\/767"},{"key":"30_CR14","doi-asserted-by":"publisher","unstructured":"Chockler, H., Strichman, O.: Easier and more informative vacuity checks. In: MEMOCODE, pp. 189\u2013198. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/MEMCOD.2007.371225","DOI":"10.1109\/MEMCOD.2007.371225"},{"key":"30_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-030-89051-3_4","volume-title":"Programming Languages and Systems","author":"W Choi","year":"2021","unstructured":"Choi, W., Vazirani, M., Santolucito, M.: Program synthesis for musicians: a usability testbed for temporal logic specifications. In: Oh, H. (ed.) APLAS 2021. LNCS, vol. 13008, pp. 47\u201361. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-89051-3_4"},{"key":"30_CR16","series-title":"Lecture Notes in Business Information Processing","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-031-08848-3_4","volume-title":"Process Mining Handbook","author":"CD Ciccio","year":"2022","unstructured":"Ciccio, C.D., Montali, M.: Declarative process specifications: reasoning, discovery, monitoring. In: van der Aalst, W.M.P., Carmona, J. (eds.) Process Mining Handbook. LNBIP, vol. 448, pp. 108\u2013152. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08848-3_4"},{"issue":"1","key":"30_CR17","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1177\/001316446002000104","volume":"20","author":"J Cohen","year":"1960","unstructured":"Cohen, J.: A coefficient of agreement for nominal scales. Educ. Psychol. Measur. 20(1), 37\u201346 (1960). https:\/\/doi.org\/10.1177\/001316446002000104","journal-title":"Educ. Psychol. Measur."},{"key":"30_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-031-37703-7_18","volume-title":"Computer Aided Verification - CAV 2023","author":"M Cosler","year":"2023","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: Enea, C., Lal, A. (eds.) CAV 2023. LNCS, vol. 13965, pp. 383\u2013396. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_18"},{"issue":"1","key":"30_CR19","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/TSE.2018.2859926","volume":"46","author":"C Czepa","year":"2020","unstructured":"Czepa, C., Zdun, U.: On the understandability of temporal properties formalized in linear temporal logic, property specification patterns and event processing language. IEEE Trans. Softw. Eng. 46(1), 100\u2013112 (2020). https:\/\/doi.org\/10.1109\/TSE.2018.2859926","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-10172-9_1","volume-title":"Business Process Management","author":"G De Giacomo","year":"2014","unstructured":"De Giacomo, G., De Masellis, R., Grasso, M., Maggi, F.M., Montali, M.: Monitoring business metaconstraints based on LTL and LDL for finite traces. In: Sadiq, S., Soffer, P., V\u00f6lzer, H. (eds.) BPM 2014. LNCS, vol. 8659, pp. 1\u201317. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10172-9_1"},{"key":"30_CR21","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Iocchi, L., Favorito, M., Patrizi, F.: Restraining bolts for reinforcement learning agents. In: AAAI, pp. 13659\u201313662. AAAI Press (2020).https:\/\/doi.org\/10.1609\/AAAI.V34I09.7114","DOI":"10.1609\/AAAI.V34I09.7114"},{"key":"30_CR22","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":"30_CR23","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Masellis, R.D., Montali, M.: Reasoning on LTL on finite traces: insensitivity to infiniteness. In: AAAI, pp. 1027\u20131033. AAAI Press (2014). https:\/\/doi.org\/10.1609\/AAAI.V28I1.8872","DOI":"10.1609\/AAAI.V28I1.8872"},{"key":"30_CR24","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Rubin, S.: Automata-theoretic foundations of FOND planning for LTLf and LDLf goals. In: IJCAI, pp. 4729\u20134735. ijcai.org (2018). https:\/\/doi.org\/10.24963\/IJCAI.2018\/657","DOI":"10.24963\/IJCAI.2018\/657"},{"key":"30_CR25","doi-asserted-by":"publisher","unstructured":"De\u00a0Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860. AAAI Press (2013). https:\/\/doi.org\/10.5555\/2540128.2540252","DOI":"10.5555\/2540128.2540252"},{"issue":"5","key":"30_CR26","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"RA DeMillo","year":"1979","unstructured":"DeMillo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. CACM 22(5), 271\u2013280 (1979). https:\/\/doi.org\/10.1145\/359104.359106","journal-title":"CACM"},{"key":"30_CR27","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE, pp. 411\u2013420. ACM (1999). https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"30_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-36123-9","volume-title":"A Practical Introduction to PSL","author":"C Eisner","year":"2006","unstructured":"Eisner, C., Fisman, D.: A Practical Introduction to PSL. Springer, New York (2006). https:\/\/doi.org\/10.1007\/978-0-387-36123-9"},{"key":"30_CR29","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"},{"key":"30_CR30","doi-asserted-by":"publisher","unstructured":"Fuggitti, F., Chakraborti, T.: NL2LTL \u2013 a Python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: AAAI Conference on Artificial Intelligence, vol. 37, no. 13, pp. 16428\u201316430 (2023). https:\/\/doi.org\/10.1609\/aaai.v37i13.27068","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"30_CR31","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":"30_CR32","unstructured":"Geck, G., et al.: Iltis: teaching logic in the Web. CoRR abs\/2105.05763 (2021)"},{"key":"30_CR33","doi-asserted-by":"crossref","unstructured":"Glaser, B., Strauss, A.: The Discovery of Grounded Theory: Strategies for Qualitative Research. Sociology Press, Mill Valley (1967)","DOI":"10.1097\/00006199-196807000-00014"},{"key":"30_CR34","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":"30_CR35","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"},{"key":"30_CR36","doi-asserted-by":"publisher","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: ICSE. ACM (2008). https:\/\/doi.org\/10.1145\/1368088.1368094","DOI":"10.1145\/1368088.1368094"},{"issue":"2","key":"30_CR37","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":"2","key":"30_CR38","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/S10270-014-0435-Z","volume":"15","author":"C Haisjackl","year":"2016","unstructured":"Haisjackl, C., et al.: Understanding Declare models: strategies, pitfalls, empirical results. Softw. Syst. Model. 15(2), 325\u2013352 (2016). https:\/\/doi.org\/10.1007\/S10270-014-0435-Z","journal-title":"Softw. Syst. Model."},{"issue":"5","key":"30_CR39","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1119\/1.15129","volume":"55","author":"D Hestenes","year":"1987","unstructured":"Hestenes, D.: Toward a modeling theory of physics instruction. Am. J. Phys. 55(5), 440\u2013454 (1987). https:\/\/doi.org\/10.1119\/1.15129","journal-title":"Am. J. Phys."},{"issue":"3","key":"30_CR40","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."},{"key":"30_CR41","doi-asserted-by":"publisher","unstructured":"Hoskote, Y.V., Kam, T., Ho, P., Zhao, X.: Coverage estimation for symbolic model checking. In: Design Automation Conference, pp. 300\u2013305. ACM (1999). https:\/\/doi.org\/10.1145\/309847.309936","DOI":"10.1145\/309847.309936"},{"issue":"7","key":"30_CR42","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":"30_CR43","doi-asserted-by":"publisher","unstructured":"Konrad, S., Cheng, B.H.C.: Real-time specification patterns. In: ICSE, p. 372\u2013381. ACM (2005). https:\/\/doi.org\/10.1145\/1062455.1062526","DOI":"10.1145\/1062455.1062526"},{"issue":"2","key":"30_CR44","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. Int. J. Softw. Tools Technol. Transf. 4(2), 224\u2013233 (2003). https:\/\/doi.org\/10.1007\/s100090100062","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"30_CR45","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":"30_CR46","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)"},{"key":"30_CR47","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems\u2014A Cyber\u2013Physical Systems Approach, 2nd edn. MIT Press, Cambridge (2017)"},{"key":"30_CR48","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":"1","key":"30_CR49","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":"10","key":"30_CR50","doi-asserted-by":"publisher","first-page":"2208","DOI":"10.1109\/TSE.2019.2945329","volume":"47","author":"C Menghi","year":"2021","unstructured":"Menghi, C., Tsigkanos, C., Pelliccione, P., Ghezzi, C., Berger, T.: Specification patterns for robotic missions. IEEE Trans. Softw. Eng. 47(10), 2208\u20132224 (2021). https:\/\/doi.org\/10.1109\/TSE.2019.2945329","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR51","unstructured":"Nathan, M.J., Koedinger, K.R., Alibali, M.W.: Expert blind spot: when content knowledge eclipses pedagogical content knowledge. In: International Conference on Cognitive Sciences, pp. 644\u2013648 (2001). http:\/\/pact.cs.cmu.edu\/koedinger\/pubs\/2001_NathanEtAl_ICCS_EBS.pdf"},{"key":"30_CR52","doi-asserted-by":"crossref","unstructured":"Nathan, M.J., Petrosino, A.: Expert blind spot among preservice teachers. Am. Educ. Res. J. 40(4), 905\u2013928 (2003). https:\/\/www.jstor.org\/stable\/3699412","DOI":"10.3102\/00028312040004905"},{"issue":"OOPSLA1","key":"30_CR53","doi-asserted-by":"publisher","first-page":"1","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. PACMPL 8(OOPSLA1), 1\u201331 (2024). https:\/\/doi.org\/10.1145\/3649833","journal-title":"PACMPL"},{"key":"30_CR54","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"},{"key":"30_CR55","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"30_CR56","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"},{"key":"30_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-030-88494-9_17","volume-title":"Runtime Verification","author":"A Rajhans","year":"2021","unstructured":"Rajhans, A., Mavrommati, A., Mosterman, P.J., Valenti, R.G.: Specification and runtime verification of\u00a0temporal assessments in simulink. In: Feng, L., Fisman, D. (eds.) RV 2021. LNCS, vol. 12974, pp. 288\u2013296. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88494-9_17"},{"key":"30_CR58","unstructured":"Saarinen, S.: Query strategies for directed graphical models and their application to adaptive testing. Ph.D. thesis, Brown University (2021). https:\/\/repository.library.brown.edu\/studio\/item\/bdr:kgyft3b4\/"},{"key":"30_CR59","doi-asserted-by":"publisher","unstructured":"Saarinen, S., Krishnamurthi, S., Fisler, K., Tunnell\u00a0Wilson, P.: Harnessing the wisdom of the classes: classsourcing and machine learning for assessment instrument generation. In: SIGCSE, pp. 606\u2013612. ACM (2019). https:\/\/doi.org\/10.1145\/3287324.3287504","DOI":"10.1145\/3287324.3287504"},{"key":"30_CR60","unstructured":"Shah, A., Kamath, P., Shah, J.A., Li, S.: Bayesian inference of temporal task specifications from demonstrations. In: NeurIPS, pp. 3808\u20133817 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/13168e6a2e6c84b4b7de9390c0ef5ec5-Abstract.html"},{"issue":"3","key":"30_CR61","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1093\/ptj\/85.3.257","volume":"85","author":"J Sim","year":"2005","unstructured":"Sim, J., Wright, C.C.: The kappa statistic in reliability studies: use, interpretation, and sample size requirements. Phys. Ther. 85(3), 257\u2013268 (2005). https:\/\/doi.org\/10.1093\/ptj\/85.3.257","journal-title":"Phys. Ther."},{"key":"30_CR62","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"},{"issue":"4","key":"30_CR63","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1080\/08993408.2014.970779","volume":"24","author":"CB Taylor","year":"2014","unstructured":"Taylor, C.B., Zingaro, D., Porter, L., Webb, K.C., Lee, C.B., Clancy, M.J.: Computer science concept inventories: past and future. Comput. Sci. Educ. 24(4), 253\u2013276 (2014). https:\/\/doi.org\/10.1080\/08993408.2014.970779","journal-title":"Comput. Sci. Educ."},{"key":"30_CR64","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 (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":"30_CR65","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"},{"key":"30_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45319-9_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"MY Vardi","year":"2001","unstructured":"Vardi, M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 1\u201322. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_1"},{"key":"30_CR67","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"30_CR68","unstructured":"Wickstr\u00f6m, O.: Linear temporal logic visualizer. https:\/\/quickstrom.github.io\/ltl-visualizer"},{"key":"30_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/3-540-49116-3_3","volume-title":"STACS 99","author":"T Wilke","year":"1999","unstructured":"Wilke, T.: Classifying discrete temporal properties. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 32\u201346. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49116-3_3"},{"key":"30_CR70","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":"30_CR71","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","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:07:57Z","timestamp":1725934077000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":71,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}