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 []. 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.

Copying safety and liveness properties of computational artefacts / N. Angius, G. Primiero. - In: JOURNAL OF LOGIC AND COMPUTATION. - ISSN 0955-792X. - (2022), pp. exac053.1-exac053.29. [10.1093/logcom/exac053]

Copying safety and liveness properties of computational artefacts

G. Primiero
2022

Abstract

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 []. 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.
Philosophy of computing; philosophy of information; artefact copy; temporal logic; model checking; software theory change
Settore M-FIL/02 - Logica e Filosofia della Scienza
PRIN202022GPRIM_01 - BIAS, RISK, OPACITY in AI: design, verification and development of Trustworthy AI - PRIMIERO, GIUSEPPE - PRIN2020 - PRIN bando 2020 - 2022
Article (author)
File in questo prodotto:
File Dimensione Formato  
exac053.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 1.3 MB
Formato Adobe PDF
1.3 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
paper3_preprint.pdf

accesso aperto

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 192.92 kB
Formato Adobe PDF
192.92 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/944215
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact