{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T13:27:40Z","timestamp":1742390860737},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2006,5,11]],"date-time":"2006-05-11T00:00:00Z","timestamp":1147305600000},"content-version":"unspecified","delay-in-days":10,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2006,5]]},"abstract":"<jats:p>We address the problem of verifying clique avoidance in the TTP protocol. TTP allows several stations embedded in a car to communicate. It has many mechanisms to ensure robustness to faults. In particular, it has an algorithm that allows a station to recognize itself as faulty and leave the communication. This algorithm must satisfy the crucial \u2018non-clique\u2019 property: it is impossible to have two or more disjoint groups of stations communicating exclusively with stations in their own group. In this paper, we propose an automatic verification method for an arbitrary number of stations <jats:inline-formula id=\"ffm001\">$N$<\/jats:inline-formula> and a given number of faults <jats:inline-formula id=\"ffm002\">$k$<\/jats:inline-formula>. We give an abstraction that allows to model the algorithm by means of unbounded (parametric) counter automata. We have checked the non-clique property on this model in the case of one fault, using the ALV tool as well as the LASH tool.<\/jats:p>","DOI":"10.1017\/s1471068406002663","type":"journal-article","created":{"date-parts":[[2006,5,11]],"date-time":"2006-05-11T15:22:00Z","timestamp":1147360920000},"page":"321-353","source":"Crossref","is-referenced-by-count":1,"title":["Parametric Verification of a Group Membership Algorithm"],"prefix":"10.1017","volume":"6","author":[{"given":"AHMED","family":"BOUAJJANI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"AGATHE","family":"MERCERON","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2006,5,11]]},"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068406002663","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,31]],"date-time":"2019-03-31T19:43:33Z","timestamp":1554061413000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068406002663\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,5]]},"references-count":0,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2006,5]]}},"alternative-id":["S1471068406002663"],"URL":"https:\/\/doi.org\/10.1017\/s1471068406002663","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,5]]}}}