{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,9]],"date-time":"2024-11-09T05:11:52Z","timestamp":1731129112090,"version":"3.28.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2015,12,8]],"date-time":"2015-12-08T00:00:00Z","timestamp":1449532800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/K001698\/1 (UNCOVER) and EP\/L025507\/1 (A4A)"],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"project IMPRO","award":["ANR-2010-BLAN-0317"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,12,8]]},"abstract":"In partially observed Petri nets, diagnosis is the task of detecting whether the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution, an occurrence of a fault can eventually be diagnosed.<\/jats:p>\n In this article, we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever\u2014it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed\u2014in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.<\/jats:p>","DOI":"10.1145\/2832910","type":"journal-article","created":{"date-parts":[[2015,12,10]],"date-time":"2015-12-10T14:22:10Z","timestamp":1449757330000},"page":"1-19","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Diagnosability under Weak Fairness"],"prefix":"10.1145","volume":"14","author":[{"given":"Vasileios","family":"Germanos","sequence":"first","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Stefan","family":"Haar","sequence":"additional","affiliation":[{"name":"INRIA & LSV (ENS Cachan & CNRS)"}]},{"given":"Victor","family":"Khomenko","sequence":"additional","affiliation":[{"name":"Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Stefan","family":"Schwoon","sequence":"additional","affiliation":[{"name":"INRIA & LSV (ENS Cachan & CNRS)"}]}],"member":"320","published-online":{"date-parts":[[2015,12,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3182\/20120829-3-MX-2028.00083"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/SMC.2013.71"},{"volume-title":"Proc. ICCA. 378--383","year":"2013","author":"Biswas S.","key":"e_1_2_1_3_1","unstructured":"S. Biswas. 2013b. Fair diagnosability in PN-based DES models. In Proc. ICCA. 378--383."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-009-0077-4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2012.2200372"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2014.9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.15"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.940942"},{"volume-title":"Proc. IFIP Congr.\u201983","year":"1983","author":"Lamport L.","key":"e_1_2_1_9_1","unstructured":"L. Lamport. 1983. What good is temporal logic? In Proc. IFIP Congr.\u201983. Elsevier, 657--668."},{"volume-title":"Proc. SysTol\u201910","author":"Madalinski A.","key":"e_1_2_1_10_1","unstructured":"A. Madalinski and V. Khomenko. 2010. Diagnosability verification with parallel LTL-X model checking based on Petri net unfoldings. In Proc. SysTol\u201910. IEEE Computer Society Press, 398--403."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.3233\/KES-2010-0191"},{"volume-title":"Maria: The Modular Reachability Analyzer.","year":"2005","author":"M\u00e4kel\u00e4 M.","key":"e_1_2_1_12_1","unstructured":"M. M\u00e4kel\u00e4. 2005. Maria: The Modular Reachability Analyzer. Retrieved from http:\/\/www.tcs.hut.fi\/Software\/maria\/index.en.html."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.412626"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1625275.1625367"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.844722"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00049-I"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2002.802763"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2832910","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,8]],"date-time":"2024-11-08T11:25:37Z","timestamp":1731065137000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2832910"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,8]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,8]]}},"alternative-id":["10.1145\/2832910"],"URL":"https:\/\/doi.org\/10.1145\/2832910","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,12,8]]},"assertion":[{"value":"2014-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-09-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-12-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
