{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:12Z","timestamp":1753894392267,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2022,11,17]],"date-time":"2022-11-17T00:00:00Z","timestamp":1668643200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We provide a generic algorithm for constructing formulae that distinguish\nbehaviourally inequivalent states in systems of various transition types such\nas nondeterministic, probabilistic or weighted; genericity over the transition\ntype is achieved by working with coalgebras for a set functor in the paradigm\nof universal coalgebra. For every behavioural equivalence class in a given\nsystem, we construct a formula which holds precisely at the states in that\nclass. The algorithm instantiates to deterministic finite automata, transition\nsystems, labelled Markov chains, and systems of many other types. The ambient\nlogic is a modal logic featuring modalities that are generically extracted from\nthe functor; these modalities can be systematically translated into custom sets\nof modalities in a postprocessing step. The new algorithm builds on an existing\ncoalgebraic partition refinement algorithm. It runs in time O((m+n) log n) on\nsystems with n states and m transitions, and the same asymptotic bound applies\nto the dag size of the formulae it constructs. This improves the bounds on run\ntime and formula size compared to previous algorithms even for previously known\nspecific instances, viz. transition systems and Markov chains; in particular,\nthe best previous bound for transition systems was O(mn).<\/jats:p>","DOI":"10.46298\/lmcs-18(4:6)2022","type":"journal-article","created":{"date-parts":[[2022,11,22]],"date-time":"2022-11-22T15:20:55Z","timestamp":1669130455000},"source":"Crossref","is-referenced-by-count":2,"title":["Quasilinear-time Computation of Generic Modal Witnesses for Behavioural Inequivalence"],"prefix":"10.46298","volume":"Volume 18, Issue 4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8993-6486","authenticated-orcid":false,"given":"Thorsten","family":"Wi\u00dfmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2021-1644","authenticated-orcid":false,"given":"Stefan","family":"Milius","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2022,11,17]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/lmcs.episciences.org\/10320\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/lmcs.episciences.org\/10320\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,20]],"date-time":"2023-11-20T20:20:06Z","timestamp":1700511606000},"score":1,"resource":{"primary":{"URL":"http:\/\/lmcs.episciences.org\/9941"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,17]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-18(4:6)2022","relation":{"has-preprint":[{"id-type":"arxiv","id":"2203.11175v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2203.11175","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2203.11175","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2022,11,17]]},"article-number":"9941"}}