Copying Safety and Liveness Properties of Computational Artefacts.

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.