Data di Pubblicazione:
2022
Citazione:
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]
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.
Tipologia IRIS:
01 - Articolo su periodico
Keywords:
Philosophy of computing; philosophy of information; artefact copy; temporal logic; model checking; software theory change
Elenco autori:
N. Angius, G. Primiero
Link alla scheda completa:
Link al Full Text: