{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:29:35Z","timestamp":1743013775739,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030995232"},{"type":"electronic","value":"9783030995249"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Diagnosability is a fundamental problem of partial observable systems in safety-critical design. Diagnosability verification checks if the observable part of system is sufficient to detect some faults. A counterexample to diagnosability may consist of infinitely many indistinguishable traces that differ in the occurrence of the fault. When the system under analysis is modeled as a B\u00fcchi automaton or finite-state Fair Transition System, this problem reduces to look for ribbon-shaped paths, i.e., fair paths with a loop in the middle.<\/jats:p><jats:p>In this paper, we propose to solve the problem by extending the liveness-to-safety approach to look for lasso-shaped paths. The algorithm can be applied to various diagnosability conditions in a uniform way by changing the conditions on the loops. We implemented and evaluated the approach on various diagnosability benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_30","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"543-560","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Searching for Ribbon-Shaped Paths in Fair Transition Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4135-103X","authenticated-orcid":false,"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8506-8212","authenticated-orcid":false,"given":"Viktoria","family":"Vozarova","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Allen\u00a0Emerson, E., Lei, C.L.: Temporal reasoning under generalized fairness constraints. In: Monien, B., Vidal-Naquet, G. (eds.) STACS 86. pp. 21\u201336. Springer Berlin Heidelberg, Berlin, Heidelberg (1986)","DOI":"10.1007\/3-540-16078-7_62"},{"key":"30_CR2","doi-asserted-by":"publisher","unstructured":"BARTHE, G., D\u2019ARGENIO, P.R., REZK, T.: Secure information flow by self-composition. Mathematical Structures in Computer Science 21(6), 1207\u20131252 (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","DOI":"10.1017\/S0960129511000193"},{"key":"30_CR3","doi-asserted-by":"publisher","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66(2), 160\u2013177 (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80410-9, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S1571066104804109, fMICS\u201902, 7th International ERCIM Workshop in Formal Methods for Industrial Critical Systems (ICALP 2002 Satellite Workshop)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Bittner, B., Bozzano, M., Cavada, R., Cimatti, A., Gario, M., Griggio, A., Mattarei, C., Micheli, A., Zampedri, G.: The xSAP Safety Analysis Platform. In: TACAS. Lecture Notes in Computer Science, vol.\u00a09636, pp. 533\u2013539. Springer (2016)","DOI":"10.1007\/978-3-662-49674-9_31"},{"key":"30_CR5","doi-asserted-by":"publisher","unstructured":"Bozzano, M., Cimatti, A., Gario, M., Tonetta, S.: Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic. Logical Methods in Computer Science 11(4), \u00a0 (2015). https:\/\/doi.org\/10.2168\/LMCS-11(4:4)2015, https:\/\/doi.org\/10.2168\/LMCS-11(4:4)2015","DOI":"10.2168\/LMCS-11(4:4)2015"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: VMCAI. Lecture Notes in Computer Science, vol.\u00a06538, pp. 70\u201387. Springer (2011)","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Binary Decision Diagrams. In: Handbook of Model Checking, pp. 191\u2013217. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_7"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv Symbolic Model Checker. In: CAV. Lecture Notes in Computer Science, vol.\u00a08559, pp. 334\u2013342. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Magnago, E., Roveri, M., Tonetta, S.: Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. In: CAV (1). Lecture Notes in Computer Science, vol. 11561, pp. 376\u2013386. Springer (2019)","DOI":"10.1007\/978-3-030-25540-4_21"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Hamaguchi, K.: Another Look at LTL Model Checking. Formal Methods in System Design 10(1), 47\u201371 (1997)","DOI":"10.1023\/A:1008615614281"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Temporal and Modal Logic. Handbook of theoretical computer science 2, 995\u20131072 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"30_CR13","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 144\u2013163. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8, https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"30_CR14","unstructured":"Grastien, A.: Symbolic testing of diagnosability. In: International Workshop on Principles of Diagnosis (DX). pp. 131\u2013138 (2009)"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Jiang, S., Huang, Z., Chandra, V., Kumar, R.: A Polynomial-time Algorithm for Diagnosability of Discrete Event Systems. IEEE Transactions on Automatic Control 46(8), 1318\u20131321 (2001)","DOI":"10.1109\/9.940942"},{"key":"30_CR16","unstructured":"M. Bozzano and A. Cimatti and S. Tonetta: Testing Diagnosability of Fair Discrete-Event Systems. In: Proc. International Workshop on Principles of Diagnosis (DX-19) (2019)"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Sampath, M., Sengupta, R., Lafortune, S., Sinnamohideen, K., Teneketzis, D.: Diagnosability of Discrete-event Systems. IEEE Transactions on Automatic Control 40(9), 1555\u20131575 (1995)","DOI":"10.1109\/9.412626"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., St\u00e5lmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: FMCAD. Lecture Notes in Computer Science, vol.\u00a01954, pp. 108\u2013125. Springer (2000)","DOI":"10.1007\/3-540-40922-X_8"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:27:55Z","timestamp":1648535275000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"159","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}