{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T17:40:08Z","timestamp":1750441208858,"version":"3.41.0"},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"5-6","license":[{"start":{"date-parts":[[2004,8,12]],"date-time":"2004-08-12T00:00:00Z","timestamp":1092268800000},"content-version":"unspecified","delay-in-days":0,"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":[[2004,9]]},"abstract":"<jats:p>A system is data-independent with respect to a data type <jats:inline-formula>$X$<\/jats:inline-formula> iff the operations it can perform on values of type <jats:inline-formula>$X$<\/jats:inline-formula> are restricted to just equality testing. The system may also store, input and output values of type <jats:inline-formula>$X$<\/jats:inline-formula>. We study model checking of systems which are data-independent with respect to two distinct type variables <jats:inline-formula>$X$<\/jats:inline-formula> and <jats:inline-formula>$Y$<\/jats:inline-formula>, and may in addition use arrays with indices from <jats:inline-formula>$X$<\/jats:inline-formula> and values from <jats:inline-formula>$Y$<\/jats:inline-formula>. Our main interest is the following <jats:italic>parameterised model-checking<\/jats:italic> problem: whether a given program satisfies a given temporal-logic formula for all non-empty finite instances of <jats:inline-formula>$X$<\/jats:inline-formula> and <jats:inline-formula>$Y$<\/jats:inline-formula>. Initially, we consider instead the abstraction where <jats:inline-formula>$X$<\/jats:inline-formula> and <jats:inline-formula>$Y$<\/jats:inline-formula> are infinite and where partial functions with finite domains are used to model arrays. Using a translation to data-independent systems without arrays, we show that the <jats:inline-formula>$\\mu$<\/jats:inline-formula>-calculus model-checking problem is decidable for these systems. From this result, we can deduce properties of all systems with finite instances of <jats:inline-formula>$X$<\/jats:inline-formula> and <jats:inline-formula>$Y$<\/jats:inline-formula>. We show that there is a procedure for the above parameterised model-checking problem of the universal fragment of the <jats:inline-formula>$\\mu$<\/jats:inline-formula>-calculus, such that it always terminates but may give false negatives. We also deduce that the parameterised model-checking problem of the universal disjunction-free fragment of the <jats:inline-formula>$\\mu$<\/jats:inline-formula>-calculus is decidable. Practical motivations for model checking data-independent systems with arrays include verification of memory and cache systems, where <jats:inline-formula>$X$<\/jats:inline-formula> is the type of memory addresses, and <jats:inline-formula>$Y$<\/jats:inline-formula> the type of storable values. As an example we verify a fault-tolerant memory interface over a set of unreliable memories.<\/jats:p>","DOI":"10.1017\/s1471068404002054","type":"journal-article","created":{"date-parts":[[2004,10,14]],"date-time":"2004-10-14T08:31:43Z","timestamp":1097742703000},"page":"659-693","source":"Crossref","is-referenced-by-count":6,"title":["On model checking data-independent systems with arrays without reset"],"prefix":"10.1017","volume":"4","author":[{"given":"R. S.","family":"LAZI\u0106","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. C.","family":"NEWCOMB","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. W.","family":"ROSCOE","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2004,8,12]]},"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\/S1471068404002054","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T17:04:29Z","timestamp":1750439069000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068404002054\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,8,12]]},"references-count":0,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2004,1]]}},"alternative-id":["S1471068404002054"],"URL":"https:\/\/doi.org\/10.1017\/s1471068404002054","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"type":"print","value":"1471-0684"},{"type":"electronic","value":"1475-3081"}],"subject":[],"published":{"date-parts":[[2004,8,12]]}}}