{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:21Z","timestamp":1753889841092,"version":"3.41.2"},"reference-count":29,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,16]],"date-time":"2012-02-16T00:00:00Z","timestamp":1329350400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, i.e. the number of processes in the network. We use CSP as our formalism. We present a type reduction theory, which, for a given verification problem, establishes a function \\phi that maps all (sufficiently large) instantiations T of the parameter to some fixed type T^ and allows us to deduce that if Spec(T^) is refined by \\phi(Impl(T)), then (subject to certain assumptions) Spec(T) is refined by Impl(T). The theory can be used in practice by combining it with a suitable abstraction method that produces a t-independent process Abstr that is refined by {\\phi}(Impl(T)) for all sufficiently large T. Then, by testing (with a model checker) if the abstract model Abstr refines Spec(T^), we can deduce a positive answer to the original uniform verification problem. The type reduction theory relies on symbolic representation of process behaviour. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements, and we provide a set of translation rules that allow us to concretise symbolic transition graphs. Based on this, we prove results that allow us to infer behaviours of a process instantiated with uncollapsed types from known behaviours of the same process instantiated with a reduced type. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in a wide range of settings.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:4)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":1,"title":["A type reduction theory for systems with replicated components"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Tomasz","family":"Mazur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gavin","family":"Lowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2012,2,16]]},"reference":[{"key":"10.2168\/LMCS-8(1:4)2012_Apt:1986","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"10.2168\/LMCS-8(1:4)2012_Pnueli:1981","doi-asserted-by":"publisher","DOI":"10.1145\/567532.567551"},{"key":"10.2168\/LMCS-8(1:4)2012_Burch:1992","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"10.2168\/LMCS-8(1:4)2012_Clarke:1981","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. InLogic of Programs: Workshop, pages 52-71, London, UK, 1981. Springer-Verlag.","DOI":"10.1007\/BFb0025774"},{"key":"10.2168\/LMCS-8(1:4)2012_Clarke:1986","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"issue":"5","key":"10.2168\/LMCS-8(1:4)2012_Clarke:1992","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E. M. Clarke, O. Grumberg, and D. E. Lon","year":"1994","journal-title":"Transactions on Programming Languages and Systems 16(5):1512-1542, September 1994"},{"key":"10.2168\/LMCS-8(1:4)2012_Clarke:1999","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled.Model checking. MIT Press, Cambridge, MA, USA, 1999."},{"key":"10.2168\/LMCS-8(1:4)2012_Creese:1998","unstructured":"S. Creese and A. W. Roscoe. TTP: A case study in combining induction and data independence. Technical report, University of Oxford, 1998."},{"key":"10.2168\/LMCS-8(1:4)2012_Creese:1999a","unstructured":"S. Creese and A. W. Roscoe. Formal verification of arbitrary network topologies. InPDPTA'99: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications. CSREA Press, 1999."},{"key":"10.2168\/LMCS-8(1:4)2012_Dav58","unstructured":"M. Davis.Computability and Unsolvability. McGraw-Hill, 1958."},{"key":"10.2168\/LMCS-8(1:4)2012_EC80","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and E. M. Clarke. Characterizing Correctness Properties of Parallel Programs Using Fixpoints. InProceedings of ICALP, pages 169-181, 1980.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"10.2168\/LMCS-8(1:4)2012_FDR:Manual","unstructured":"Formal Systems (Europe) Ltd.Failures-Divergences Refinement -- FDR2 user manual, {http:\/\/www.fsel.com\/fdr2manual.html}, 2009. C. A. R. Hoare.Communicating sequential processes. Prentice Hall Europe, 1985."},{"key":"10.2168\/LMCS-8(1:4)2012_Lazic:1999","unstructured":"R. S. Lazi\u00c4\u0087.A semantic study of data independence with applications to model checking. DPhil thesis, University of Oxford, 1999."},{"key":"10.2168\/LMCS-8(1:4)2012_Lowe:2004","unstructured":"G. Lowe. On the application of counterexample-guided abstraction refinement and data independence to the parameterised model checking problem. InAVIS'04: Proceedings of the 3rd International Workshop on Automatic Verification of Infinite-State Systems, 2004."},{"key":"10.2168\/LMCS-8(1:4)2012_Lazic:1998","unstructured":"R. S. Lazi\u00c4\u0087 and A. W. Roscoe. Verifying determinism of concurrent systems which use unbounded arrays. Technical report, University of Oxford, 1998."},{"key":"10.2168\/LMCS-8(1:4)2012_Lub84","first-page":"12","volume":"21","author":"B. D. Lubachevsky","year":"1984","journal-title":"\u00c3\u0085cta Informatica"},{"key":"10.2168\/LMCS-8(1:4)2012_Tomasz-thesis","unstructured":"T. Mazur. Model Checking Systems with Replicated Components using CSP. DPhil thesis, University of Oxford, 2010."},{"key":"10.2168\/LMCS-8(1:4)2012_Mazur:2007","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.012"},{"key":"10.2168\/LMCS-8(1:4)2012_Mazur:2010","unstructured":"T. Mazur and G. Lowe. CSP-based counter abstraction for systems with node identifiers. Submitted for publication."},{"key":"10.2168\/LMCS-8(1:4)2012_McMillan:1992","doi-asserted-by":"crossref","unstructured":"K. L. McMillan.Symbolic Model Checking. PhD thesis, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"10.2168\/LMCS-8(1:4)2012_moffat:2010","unstructured":"N. Moffat. Identifying and Exploiting Symmetry for CSP Refinement Checking. DPhil thesis, University of Oxford, submitted 2010."},{"key":"10.2168\/LMCS-8(1:4)2012_Pnueli:1977","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. InSFCS'77: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46-57, Washington, DC, USA, 1977. IEEE Computer Society.","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.2168\/LMCS-8(1:4)2012_Pnueli:2002","doi-asserted-by":"crossref","unstructured":"A. Pnueli, J. Xu, and L. D. Zuck. Liveness with (0, 1,infty)-counter abstraction. InCAV'02: Proceedings of the 14th International Conference on Computer Aided Verification, pages 107-122, London, UK, 2002. Springer-Verlag.","DOI":"10.1007\/3-540-45657-0_9"},{"issue":"2-3","key":"10.2168\/LMCS-8(1:4)2012_Roscoe:1999","doi-asserted-by":"crossref","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"A. W. Roscoe and P. J. Broadfoot","year":"1999","journal-title":"Journal of Computer Security"},{"key":"10.2168\/LMCS-8(1:4)2012_Roscoe:2004","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068404002054"},{"key":"10.2168\/LMCS-8(1:4)2012_Roscoe:1997","unstructured":"A. W. Roscoe.The theory and practice of concurrency. Prentice Hall PTR, 1997."},{"key":"10.2168\/LMCS-8(1:4)2012_Roscoe:1998","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. Proving security protocols with model checkers by data independence techniques. InCSFW'98: Proceedings of the 11th IEEE workshop on Computer Security Foundations, page 84, Washington, DC, USA, 1998. IEEE Computer Society.","DOI":"10.1109\/CSFW.1998.683158"},{"key":"10.2168\/LMCS-8(1:4)2012_Roscoe:2008b","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe. The three platonic models of divergence-strict CSP. InICTAC'08: Proceedings of the 5th International Colloquium on Theoretical Aspects of Computing, pages 23-49, Berlin, Heidelberg, 2008. Springer-Verlag.","DOI":"10.1007\/978-3-540-85762-4_3"},{"key":"10.2168\/LMCS-8(1:4)2012_Roscoe:2010","doi-asserted-by":"crossref","unstructured":"A. W. Roscoe.Understanding Concurrent Systems. Springer, 2010.","DOI":"10.1007\/978-1-84882-258-0"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/869\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/869\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:09:50Z","timestamp":1744067390000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,16]]},"references-count":29,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:4)2012","relation":{"references":[{"id-type":"doi","id":"10.1007\/3-540-45657-0_9","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1201.1716","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1201.1716","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,16]]},"article-number":"869"}}