OBJECTIVES
The logical relation of copy holding between an artefact and its DT can be represented by a formal simulation between a probabilistic and a deterministic model, formulating the outcomes generated by a ML or a DL set of algorithms over data passed as input of the technical physical artefact. Examples of models of this sort are probabilistic transition systems such as discrete-time Markov chains and Markov decision processes [Baier et al. 2006]. Safety, liveness, reliability, accuracy and other properties of interest of the artefact can then be inferred from and checked for such probabilistic models. This significantly changes the logical framework for copies advanced in [Angius, Primiero, 2018; submitted], where logical relations of property preservation run along two deterministic models, namely the deterministic State Transition Systems (STS) for both copied and copying systems. In the context of DT models, the main question is whether the deterministic STS of the copied system (the artefact) preserves properties of the probabilistic transitions system of the copying system (the DT possibly equipped with ML inputs). The formal relations between the two models that this project intends to investigate need to be captured by simulation relations from process algebra theory for probabilistic systems. Also, the epistemological relations between the two models are mediated by the ML algorithm: one is required to assess whether the probabilistic STS is an adequate representation of the ML model outputs. To do so, a grounded general formal representation of the ontology of the system under investigation is required.
Hence, the research questions that this project aims to answer can be formulated as follows:
QUESTION 1
Ontological
Question
What kind of entities are DTs? Which relations do they entertain with the twin physical systems?
In particular, can existing notions such as replica, copy and counterpart, as discussed in the philosophy of technology literature [Carrara and Soavi 2010], be adapted to make sense of the engineering view on DTs, or is a new conceptual framework required?
QUESTION 2
Epistemological
Question
What are the epistemological roles played by ML models, computational probabilistic models, and deterministic artefact models in DT simulations? How are the validation and verification processes, typically characterising model construction in simulative sciences, arranged in view of such an abundance of models? What types of error can we expect and prevent?
QUESTION 3
Logical
Question
Once the ontological status of DTs is defined, what kind of logical relations do technical artefacts and their DTs entertain and how do we formalise them? To what extent can one infer safety/liveness/reliability/accuracy of the actual artefact from the properties being validated (if they are) from a DT based on ML/DL techniques, and is checking these properties feasible?
To answer these questions, we articulate the aims of this research project as follows:
OBJECTIVE 1:
understanding, from an ontological perspective, what kind of entities DTs are within a larger ontology of technical artefacts, engineering specifications, and engineering (mal-)functions. Building on the state of the art in philosophy of technology [Kroes 2012], formal ontology and engineering [Borgo et al. 2014, Masolo and Sanfilippo 2020], the goal is to characterise the properties that a (digital) specification has to satisfy to count as the DT of a technical artefact as distinct from other types of models.
TASK 1.1: understand what it means to consider a model as the copy of a physical item, thus to classify it as its DT, and provide a conceptual framework to establish when, in which sense and within which limitations a digital specification can be understood as a reliable counterpart of a physical system.
TASK 1.2: define ontological and engineering relationships (e.g. the comparison between physical and digital compositionalities) across artefacts and their DTs.
TASK 1.3: establish procedures to treat faults within an ontological representation, possibly distinguishing structural, behavioural, and functional failures in terms of DT simulations. This latter task will sensibly extend current literature on miscomputation [Fresco, Primiero 2013; Floridi et al. 2015].
TASKS 1.1, 1.2 and 1.3 will be the main research tasks of the post-doctoral researcher hired by ISTC-CNR Trento, working in collaboration with all units.
OBJECTIVE 2:
defining the appropriate epistemological framework for simulation in the DT scheme just outlined, as it differs from those designed for deterministic computational systems, such as that conceptualised in [Primiero 2019]. Computer simulations are typically defined by a target simulated system, a mathematical model usually in the form of a set of differential equations, a computational model approximating differential equations, and a simulative program providing numerical solutions to the differential equations.
TASK 2.1: to verify whether ideal properties of simulation relations hold for the DT scenario, i.e. full isomorphism between mathematical models and the target system; correct implementation of computational models by their simulative programs; and bisimulation relations (or simulation relation in one of the two directions) between mathematical and computational models [Guala 2002]. If these relations hold, simulative programs should be able to map onto target systems providing adequate predictions of their behaviours [Humphreys 2004].
TASK 2.2: to expand such a framework for DT simulations, wherein industrial artefacts and their digital twins simulate each other in real time, and where different kinds of models are involved.
TASKS 2.1, and 2.2 will be the main research tasks of the post-doctoral researcher hired by UNIME, working in collaboration with all units.
OBJECTIVE 3:
defining appropriate formal simulation relations across probabilistic systems that best represent the dynamic copy relation between the probabilistic output of a ML model and its implementation in the physical artefact. Once formal ontological relations of copy have been identified between ML models and probabilistic STS on the one hand, and between the artefact and probabilistic STS on the other, in the light of the epistemological framework previously developed, probabilistic process algebra can be used for its formalisation.
TASK 3.1: to identify the most appropriate probabilistic model between available ones (e.g Markov Chains and Markov Decision Processes) to analyse at a sufficiently fine level of abstraction the simulation performed by the DT, so as to offer equivalence relations and property preservation for the physical artefact.
TASK 3.2: to develop formal verification algorithms of security properties of the ML program, qua digital twin, to answer whether certain behavioural properties hold of the copy, along the line of what proposed in [Angius and Primiero submitted]. To this aim, probabilistic temporal logics, including PCTL and PLTL and their extensions, have to be taken into account and existing model checking algorithms adapted for the case at hand.
TASKS 3.1 and 3.2 will be the main research tasks of the post-doctoral researcher hired by UNIMI, working in collaboration with all units.
