{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:01:25Z","timestamp":1750309285625,"version":"3.41.0"},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,16]],"date-time":"2024-04-16T00:00:00Z","timestamp":1713225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NFR","award":["316022"],"award-info":[{"award-number":["316022"]}]},{"name":"European Union\u2019s Horizon 2020 research and innovation programme","award":["MSCA-101031081"],"award-info":[{"award-number":["MSCA-101031081"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>We study the existence of finite characterisations for modal formulas. A finite characterisation of a modal formula \u03c6 is a finite collection of positive and negative examples that distinguishes \u03c6 from every other, non-equivalent modal formula, where an example is a finite pointed Kripke structure. This definition can be restricted to specific frame classes and to fragments of the modal language: a modal fragment \u2112 admits finite characterisations with respect to a frame class \u2131 if every formula \u03c6 \u2208 \u2112 has a finite characterisation with respect to \u2112 consisting of examples that are based on frames in \u2131. Finite characterisations are useful for illustration, interactive specification and debugging of formal specifications, and their existence is a precondition for exact learnability with membership queries. We show that the full modal language admits finite characterisations with respect to a frame class \u2131 only when the modal logic of \u2131 is locally tabular. We then study which modal fragments, freely generated by some set of connectives, admit finite characterisations. Our main result is that the positive modal language without the truth-constants \u22a4 and \u22a5 admits finite characterisations w.r.t.\u00a0the class of all frames. This result is essentially optimal: finite characterisability fails when the language is extended with the truth constant \u22a4 or \u22a5 or with all but very limited forms of negation.<\/jats:p>","DOI":"10.1145\/3649461","type":"journal-article","created":{"date-parts":[[2024,2,27]],"date-time":"2024-02-27T12:57:26Z","timestamp":1709038646000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Characterising Modal Formulas with Examples"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2538-5846","authenticated-orcid":false,"given":"Balder","family":"ten Cate","sequence":"first","affiliation":[{"name":"ILLC, University of Amsterdam, Amsterdam, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9000-4675","authenticated-orcid":false,"given":"Raoul","family":"Koudijs","sequence":"additional","affiliation":[{"name":"University of Bergen, Bergen, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,16]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2043652.2043656"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022821128753"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.5555\/381193"},{"key":"e_1_3_3_5_2","volume-title":"Model Theory","author":"Chang Chen Chung","year":"1973","unstructured":"Chen Chung Chang and H. Jerome Keisler. 1973. Model Theory. North-Holland Pub. Co."},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093891703"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.24963\/kr.2022\/17"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2021\/260"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2022\/364"},{"key":"e_1_3_3_10_2","doi-asserted-by":"crossref","unstructured":"D. Janin and I. Walukiewicz. 1995. Automata for the modal \\(\\mu\\) -calculus and related results. In Mathematical Foundations of Computer Science 1995. Lecture Notes in Computer Science Vol. 969. Springer 552\u2013562.","DOI":"10.1007\/3-540-60246-1_160"},{"key":"e_1_3_3_11_2","volume-title":"Saying It with Pictures: A Logical Landscape of Conceptual Graphs","author":"Kerdiles Gwen","year":"2001","unstructured":"Gwen Kerdiles. 2001. Saying It with Pictures: A Logical Landscape of Conceptual Graphs. ILLC Dissertation Series (DS). ILLC."},{"key":"e_1_3_3_12_2","unstructured":"Raoul Koudijs. 2022. Learning Modal Formulas via Dualities. Master\u2019s Thesis. ILLC. https:\/\/eprints.illc.uva.nl\/id\/eprint\/1957\/1\/MoL-2022-07.text.pdf"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/7.4.501"},{"key":"e_1_3_3_14_2","first-page":"217","volume-title":"Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS \u201986)","author":"Mannila Heikki","year":"1986","unstructured":"Heikki Mannila and Kari-Jouko R\u00e4ih\u00e4. 1986. Test data for relational queries. In Proceedings of the 5th ACM SIGACT-SIGMOD Symposium on Principles of Database Systems (PODS \u201986). 217\u2013223."},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00042-6"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008275906015"},{"key":"e_1_3_3_17_2","unstructured":"Patrik Sestic. 2023. Unique Characterisability of Linear Temporal Logic. Master\u2019s Thesis. ILLC."},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","unstructured":"Slawek Staworko and Piotr Wieczorek. 2015. Characterizing XML twig queries with examples. In Proceedings of the 18th International Conference on Database Theory (ICDT \u201915). 144\u2013160. DOI:10.4230\/LIPIcs.ICDT.2015.144","DOI":"10.4230\/LIPIcs.ICDT.2015.144"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3559756"},{"key":"e_1_3_3_20_2","unstructured":"Balder ten Cate V\u00edctor Dalmau and Jakub Opr\u0161al. 2023. Right-adjoints for datalog programs and homomorphism dualities over restricted slasses. arXiv:cs.LO\/2302.06366 (2023)."},{"key":"e_1_3_3_21_2","volume-title":"Modal Correspondence Theory","author":"Benthem J. van","year":"1976","unstructured":"J. van Benthem. 1976. Modal Correspondence Theory. Ph.D. Dissertation. University of Amsterdam."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649461","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649461","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:03:17Z","timestamp":1750291397000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649461"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,16]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3649461"],"URL":"https:\/\/doi.org\/10.1145\/3649461","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,4,16]]},"assertion":[{"value":"2023-04-17","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-02-12","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}