Copying safety and liveness properties of computational artefacts

被引:1
|
作者
Angius, Nicola [1 ]
Primiero, Giuseppe [2 ]
机构
[1] Univ Messina, Dept Cognit Sci, Via Concez 6, I-98121 Messina, Italy
[2] Univ Milan, Dept Philosophy, Via Festa Perdono 7, I-20122 Milan, Italy
关键词
Philosophy of computing; philosophy of information; artefact copy; temporal logic; model checking; software theory change; REPRODUCIBILITY; EVOLUTION;
D O I
10.1093/logcom/exac053
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:1089 / 1117
页数:29
相关论文
共 50 条
  • [31] PRESERVING LIVENESS - COMMENTS ON SAFETY AND LIVENESS FROM A METHODOLOGICAL POINT-OF-VIEW
    ABADI, M
    ALPERN, B
    APT, KR
    FRANCEZ, N
    KATZ, S
    LAMPORT, L
    SCHNEIDER, FB
    INFORMATION PROCESSING LETTERS, 1991, 40 (03) : 141 - 142
  • [32] Spanning the Spectrum from Safety to Liveness
    Faran, Rachel
    Kupferman, Orna
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 183 - 200
  • [33] Spanning the spectrum from safety to liveness
    Faran, Rachel
    Kupferman, Orna
    ACTA INFORMATICA, 2018, 55 (08) : 703 - 732
  • [34] Spanning the spectrum from safety to liveness
    Rachel Faran
    Orna Kupferman
    Acta Informatica, 2018, 55 : 703 - 732
  • [35] Safety and Liveness Properties based on Activity Chain for Composite Web Services and The Compliance Verifications
    Chen, Bo
    Zeng, Guosun
    IEEE 15TH PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING, PROCEEDINGS, 2009, : 115 - 120
  • [36] The logic of identity and copy for computational artefacts
    Angius, Nicola
    Primiero, Giuseppe
    JOURNAL OF LOGIC AND COMPUTATION, 2018, 28 (06) : 1293 - 1322
  • [37] PRESERVING LIVENESS - COMMENTS ON SAFETY AND LIVENESS FROM A METHODOLOGICAL POINT-OF-VIEW - REPLY
    DEDERICHS, F
    WEBER, R
    INFORMATION PROCESSING LETTERS, 1991, 40 (03) : 143 - 143
  • [38] Duke Ellington's Newport Up! Liveness, artefacts and the seductive menace of jazz revisited
    Williams, Katherine
    NEW JAZZ CONCEPTIONS: HISTORY, THEORY, PRACTICE, 2017, : 111 - 129
  • [39] Generalized Counterexamples to Liveness Properties
    Aleksandrowicz, Gadi
    Baumgartner, Jason
    Ivrii, Alexander
    Nevo, Ziv
    2013 FORMAL METHODS IN COMPUTER-AIDED DESIGN (FMCAD), 2013, : 169 - 172
  • [40] Quantitative information flow as safety and liveness hyperproperties
    Yasuoka, Hirotoshi
    Terauchi, Tachio
    THEORETICAL COMPUTER SCIENCE, 2014, 538 : 167 - 182