{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T18:19:55Z","timestamp":1770229195591,"version":"3.49.0"},"reference-count":39,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T00:00:00Z","timestamp":1660521600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,7,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>This paper shows how safety and liveness properties are not necessarily preserved by different kinds of copies of computational artefacts and proposes procedures to preserve them, which are consistent with ethical analyses on software property rights infringement. Safety and liveness are second-order properties that are crucial in the definition of the formal ontology of computational artefacts. Software copies are analysed at the level of their formal models as exact, inexact and approximate copies, according to the taxonomy in [3]. First, it is explained how exact copies are the only kind of copies that preserve safety and liveness properties, and how inexact and approximate copies do not necessarily preserve them. Secondly, two model checking algorithms are proposed to verify whether inexact and approximate copies actually preserve safety and liveness properties. Essential properties of termination, correctness and complexity are proved for these algorithms. Finally, contraction and expansion algorithmic operations are defined, allowing for the automatic design of safety- and liveness-preserving approximate copies. As a conclusion, the relevance of the present logical analysis for the ongoing debates in miscomputation and computer ethics is highlighted.<\/jats:p>","DOI":"10.1093\/logcom\/exac053","type":"journal-article","created":{"date-parts":[[2022,8,15]],"date-time":"2022-08-15T12:47:27Z","timestamp":1660567647000},"page":"1089-1117","source":"Crossref","is-referenced-by-count":2,"title":["Copying safety and liveness properties of computational artefacts"],"prefix":"10.1093","volume":"33","author":[{"given":"Nicola","family":"Angius","sequence":"first","affiliation":[{"name":"Department of Cognitive Science, University of Messina , Via Concezione 6, 98121 Messina, Italy"}]},{"given":"Giuseppe","family":"Primiero","sequence":"additional","affiliation":[{"name":"Department of Philosophy, Univesity of Milan , Via Festa del Perdono 7, 20122 MILANO, Italy"}]}],"member":"286","published-online":{"date-parts":[[2022,8,15]]},"reference":[{"key":"2023072417264734600_ref1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","article-title":"Defining liveness","volume":"21","author":"Alpern","year":"1985","journal-title":"Information Processing Letters"},{"key":"2023072417264734600_ref2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","article-title":"Recognizing safety and liveness","volume":"2","author":"Alpern","year":"1987","journal-title":"Distributed Computing"},{"key":"2023072417264734600_ref3","doi-asserted-by":"crossref","first-page":"1293","DOI":"10.1093\/logcom\/exy012","article-title":"The logic of identity and copy for computational artefacts","volume":"28","author":"Angius","year":"2018","journal-title":"Journal of Logic and Computation"},{"key":"2023072417264734600_ref4","first-page":"1","article-title":"Infringing software property rights: ontological, methodological, and ethical questions","volume":"33","author":"Angius","year":"2019","journal-title":"Philosophy & Technology"},{"key":"2023072417264734600_ref5","article-title":"Principles of Model Checking","author":"Baier","year":"2008"},{"key":"2023072417264734600_ref6","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","article-title":"Liveness checking as safety checking","volume":"66","author":"Biere","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2023072417264734600_ref7","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","article-title":"Synthesizing robust systems","volume":"51","author":"Bloem","year":"2014","journal-title":"Acta Informatica"},{"key":"2023072417264734600_ref8","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-642-14295-6_36","article-title":"Robustness in the presence of liveness","volume-title":"Computer Aided Verification","author":"Bloem","year":"2010"},{"key":"2023072417264734600_ref9","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1002\/smr.319","article-title":"Towards a taxonomy of software change","volume":"17","author":"Buckley","year":"2005","journal-title":"Journal of Software Maintenance and Evolution: Research and Practice"},{"key":"2023072417264734600_ref10","doi-asserted-by":"crossref","first-page":"414","DOI":"10.5840\/monist201093324","article-title":"Copies, replicas, and counterfeits of artworks and artefacts","volume":"93","author":"Carrara","year":"2010","journal-title":"The Monist"},{"key":"2023072417264734600_ref11","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/s003660070003","article-title":"Function in device representation","volume":"16","author":"Chandrasekaran","year":"2000","journal-title":"Engineering with Computers"},{"key":"2023072417264734600_ref12","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1002\/smr.220","article-title":"Types of software evolution and software maintenance","volume":"13","author":"Chapin","year":"2001","journal-title":"Journal of Software Maintenance and Evolution: Research and Practice"},{"key":"2023072417264734600_ref13","article-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"2023072417264734600_ref14","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/978-3-540-92966-6_11","article-title":"Requirements evolution and what (research) to do about it","volume-title":"Design Requirements Engineering: A Ten-Year Perspective","author":"Ernst","year":"2009"},{"key":"2023072417264734600_ref15","doi-asserted-by":"crossref","first-page":"1199","DOI":"10.1007\/s11229-014-0610-3","article-title":"On malfunctioning software","volume":"192","author":"Floridi","year":"2015","journal-title":"Synthese"},{"key":"2023072417264734600_ref16","volume-title":"Introduction to Process Algebra","author":"Fokkink","year":"2013"},{"key":"2023072417264734600_ref17","article-title":"The foundations of arithmetic a logico-mathematical enquiry into the concept of number","volume-title":"English Translation by JL Austin","author":"Frege","year":"1953"},{"key":"2023072417264734600_ref18","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/s13347-013-0112-0","volume":"26","author":"Fresco","year":"2013","journal-title":"Miscomputation. Philosophy & Technology"},{"key":"2023072417264734600_ref19","doi-asserted-by":"crossref","first-page":"E14","DOI":"10.1038\/s41586-020-2766-y","article-title":"Transparency and reproducibility in artificial intelligence","volume":"586","author":"Haibe-Kains","year":"2020","journal-title":"Nature"},{"key":"2023072417264734600_ref20","doi-asserted-by":"crossref","DOI":"10.5040\/9781474254540","volume-title":"The Aesthetics and Ethics of Copying","author":"Hick","year":"2016"},{"key":"2023072417264734600_ref21","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1126\/science.359.6377.725","article-title":"Artificial intelligence faces reproducibility crisis","volume":"359","author":"Hutson","year":"2018","journal-title":"Science"},{"key":"2023072417264734600_ref22","article-title":"Computer Ethics","volume-title":"Pearson","author":"Johnson","year":"2008"},{"key":"2023072417264734600_ref23","volume-title":"Temporal Logic and State Systems","author":"Kr\u00f6ger","year":"2008"},{"key":"2023072417264734600_ref24","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","article-title":"Model checking of safety properties","volume":"19","author":"Kupferman","year":"2001","journal-title":"Formal Methods in System Design"},{"key":"2023072417264734600_ref25","volume-title":"Events: A Metaphysical Study","author":"Lombard","year":"1986"},{"key":"2023072417264734600_ref26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2220347","article-title":"What is a criterion of identity?","volume":"39","author":"J. Lowe","year":"1989","journal-title":"The Philosophical Quarterly (1950)"},{"key":"2023072417264734600_ref27","first-page":"990","article-title":"Objects and criteria of identity","volume-title":"A Companion to the Philosophy of Language","author":"J. Lowe","year":"1997"},{"key":"2023072417264734600_ref28","doi-asserted-by":"crossref","first-page":"32:1","DOI":"10.1145\/3079368.3079412","article-title":"Principles of antifragile software","volume-title":"Companion to the First International Conference on the Art, Science and Engineering of Programming, Programming \u201817","author":"Monperrus","year":"2017"},{"key":"2023072417264734600_ref29","first-page":"200","volume-title":"Should I Copy My Neighbor\u2019s Software","author":"Nissenbaum","year":"1995"},{"key":"2023072417264734600_ref30","article-title":"Identity","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Noonan","year":"2018"},{"key":"2023072417264734600_ref31","article-title":"Software model checking of liveness properties via transition invariants","author":"Podelski","year":"2003","journal-title":"Technical Report MPI-I-2003-2-00, Max-Planck-Institut f\u00fcr Informatik"},{"key":"2023072417264734600_ref32","doi-asserted-by":"crossref","first-page":"5719","DOI":"10.1007\/s11229-019-02305-7","article-title":"A theory of change for prioritised resilient and evolvable software systems","volume":"198","author":"Primiero","year":"2021","journal-title":"Synthese"},{"key":"2023072417264734600_ref33","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0951-8320(94)90065-5","article-title":"Critical system properties: survey and taxonomy","volume":"43","author":"Rushby","year":"1994","journal-title":"Reliability Engineering & System Safety"},{"key":"2023072417264734600_ref34","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511777110","volume-title":"Introduction to Bisimulation and Coinduction","author":"Sangiorgi","year":"2011"},{"key":"2023072417264734600_ref35","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","article-title":"Safety, liveness and fairness in temporal logic","volume":"6","author":"Prasad Sistla","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"2023072417264734600_ref36","first-page":"211","article-title":"Logic and model checking by imprecise probabilistic interpreted systems","volume-title":"Multi-Agent Systems - 18th European Conference, EUMAS 2021","author":"Termine","year":"2021"},{"key":"2023072417264734600_ref37","first-page":"232","article-title":"Modelling accuracy and trustworthiness of explaining agents","volume-title":"Logic, Rationality, and Interaction - 8th International Workshop, LORI 2021","author":"Termine","year":"2021"},{"key":"2023072417264734600_ref38","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1305\/ndjfl\/1093634732","article-title":"Significant parts and identity of artifacts","volume":"34","author":"Tzouvaras","year":"1993","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"2023072417264734600_ref39","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511612756","volume-title":"Sameness and Substance Renewed","author":"Wiggins","year":"2001"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/5\/1089\/50948125\/exac053.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/33\/5\/1089\/50948125\/exac053.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,24]],"date-time":"2023-07-24T17:27:16Z","timestamp":1690219636000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/33\/5\/1089\/6663254"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,15]]},"references-count":39,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2022,8,15]]},"published-print":{"date-parts":[[2023,7,25]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exac053","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,7]]},"published":{"date-parts":[[2022,8,15]]}}}