The paper considers the problem of discovering divergences between the actions of a digital twin and those of its real-world counterpart. It observes the similarities between this problem and an existing field of formal methods called Runtime Verification (RV), and suggests leveraging and adapting RV techniques to this efect. Concretely, three important aspects of the problem are identified and for which both theoretical and practical challenges must be addressed.
A digital twin is a virtual representation of a real-world entity [
The process of detecting deviations can be summarized as illustrated in Figure 1. A real-world entity is given inputs , which can consist of controllable (i.e. user-defined) values, as well as uncontrollable (i.e. environmental) objects, in addition to any reading related to the entity’s current internal state. The entity reacts to these inputs by producing outputs ; again, these outputs can be actions directly performed by the entity, or measured values of the entity’s state or the environment. In parallel, the inputs are recorded and fed to a digital twin , which simulates the real-world entity and produces its own outputs . The observed output and the synthetic output are then fed to a comparison procedure , which decides whether they are in agreement (⊤) or not (⊥).
In this paper, we reveal the similarities that this problem shares with a research topic crossing
the fields of software engineering and formal methods, called
runtime verification (RV) [
Runtime verification is the discipline of computer science where an object called a monitor is
used to observe the behavior of another program. At various moments, instrumented codepoints
relay information about the program’s actions and state to the monitor, producing a sequence
of data elements called “events”, denoted by = 1, 2, … . The monitor compares this event
trace against a formal specification of what constitutes a correct execution; any violation
of the specification is reported on-the-fly, as the monitored program executes. Research on
runtime verification has produced a variety of monitors supporting a large class of specification
languages [
A Passive Operation As in RV, the monitoring of digital twins is mostly a passive procedure:
one is not concerned with generating inputs that drive the system, as is the case for conformance
testing [
Properties on Digital Twins A first possible application of runtime verification consists of an indirect comparison between the twin’s behavior and that of the real-world entity. It supposes the existence of conditions 1, … , , which are known to be true for all executions of the digital twin; these properties, acting as a form of “guarantee,” are extracted from the twin beforehand by an arbitrary procedure , as illustrated in Figure 2. These properties, in turn, can be converted into monitors that observe the operation of the real-world entity in real time. Any observed sequence that violates one of the is, by definition, a sequence that cannot be . . .
φn I ∧ ⊤/⊥ produced by the digital twin for the same inputs, and thus indicates a divergence between the twin and its real-world counterpart.
Note that in such a scenario, the twin itself does not need to be “executed” —that is, it is unnecessary to have the twin generate one or more traces for comparison with the real-world entity’s output. This approach can present advantages in cases where running a twin may incur a high cost. Instead of a constant synchronization between the twin and the real-world entity, the lighter monitors may observe the output of the entity as long as it corresponds to expected behavior. Further analysis (and possible adaptation of the twin) is only required when one of the properties is violated by the observations. This, in itself, may require substantial analysis to determine which are the relevant that need to be monitored.
Declarative Definition of a Twin In this first suggested mode of operation, the detection
of divergences is sound: a violation of one of the properties indicates a genuine discrepancy
between the twin and the real-world entity. The detection is complete if any sequence satisfying
⋀ is also a possible (valid) sequence produced by the twin. In such a case, the twin’s behavior
is completely captured by the conditions that serve as definitions. Thus, one can imagine
specifying the operation of the twin in a declarative way, as opposed to a “procedural” or
“imperative” way. Instead of programming the twin as an executable object that receives inputs
and produces outputs, the execution of the twin is driven by a satisfiability (SAT) solver: given a
sequence of inputs, the solver finds a sequence of outputs satisfying the properties, and returns
that sequence as the twin’s reaction to the inputs. Such a declarative approach has already been
attempted to simulate the execution of web services from temporal logic specifications [
The previous approach is the most direct application of runtime verification to digital twins.
However, its soundness rests on the hypothesis that a set of properties of the twin can be
extracted and used as formal guarantees on its execution. For a twin that is defined procedurally,
those properties can be deduced from its implementation (for example by defining properties
manually and verifying them through model checking [
However, obtaining these guarantees may be a complex process, and completely capturing the behavior of the twin in such a way may not be a realistic assumption. Another possibility consists of handling the twin as a black box, and to directly compare its output to that of the real-world entity (for a given input sequence), as described in Figure 1. A second point that this article puts forward is that this comparison can be framed as a generalization of runtime verification.
Monitoring Two Traces Contrary to RV, monitoring twins involves not one, but (at least)
two traces at the same time ( and ). The “property” that needs to be evaluated in such a
case correlates the events observed in both traces. This is a particular case of what is called a
hyperproperty [
Expressiveness As a matter of fact, an anticipated challenge for the leveraging of RV
techniques to digital twin monitoring is the relatively low expressiveness of the notations they use
as their specification language. A recent taxonomy of existing RV approaches highlights the
fact that many of them use formalisms based on propositional temporal logic or finite-state
automata [
Another important challenge lies in the fact that not all divergences between an entity and its twin are meaningful and indicative of a problem. There are situations where discrepancies between an entity and its twin are expected, if not unavoidable, and still do not represent any malfunction, modeling error, or significant drift between a twin and its real-world counterpart. (a) Loose equality (b) Multiple worlds
Sources of Divergence A first such case is caused by uncertainty in measurements. A physical entity will typically have its environment and behavior measured by sensors, whose output is intrinsically tainted with uncertainty, bias, or even spurious drop-outs. Thus one cannot expect a strict equality between values produced (or predicted) by a twin and those measured in a real-world system. It turns out that several works in the field of RV have addressed the issue of verifying properties in the presence of missing or imprecise events [23, 24, 25], which could be leveraged to the context of digital twins.
A second source of divergence may be caused by diferent interleavings in the events produced by a twin and its counterpart. This can happen when events produced by multiple components of the system happen more or less simultaneously, and are arbitrarily flattened to a particular ordering which may difer depending on uncontrollable or external factors. Instrumentation is sometimes designed on purpose to lose some ordering information, as is the case in some cyber-physical systems [26].
A final source of divergences comes from under-specification . In some cases, it is expected that the digital twin is run from a coarse-grained description of the real-world entity that does not totally capture its internal state. This typically shows up as the system appearing to operate non-deterministically, producing diferent outputs in what are apparently identical input conditions. In some other cases, non-determinism may simply arise from the fact that multiple possible (and equally acceptable) outcomes are possible for the same set of initial conditions.
For all these reasons, it is unrealistic that the comparison procedure shown in Figure 1 looks at and and simply expects both to be identical. We identify two ways of dealing with this issue, one being the opposite of the other, and illustrated in Figure 3. Single World, Loose Equality A first possibility, illustrated in Figure 3a is to let a digital twin produce a unique output for a given input (i.e. a “single possible world”). However, it is allowed (and even expected) that this output difers slightly from ; therefore, the comparison procedure does not look for strict equality between the two streams, but rather evaluates a relaxed property. For example, for a system producing a stream of numerical values, one may expect that the running average over a sliding window of values is the same, but not the individual events produced by both systems. In mathematical terms, the comparison criterion is an equivalence relation that is looser than equality. For numerical values, this can be likened to fuzzy comparators [27].
This mode of operation brings challenges of its own. First, an appropriate equivalence relation must be defined, and it is expected that such relation be specific to each problem domain. Second is the necessity of evaluating this relation eficiently at runtime, over two streams of events that are progressively produced by both the twin and the real-world entity. Deviations should be reported on-the-fly, as obviously one cannot wait for the executions to complete before starting the comparison. This seemingly innocuous observation makes it dificult to use well-known string distance criteria, such as Levenshtein distance [28], which have a high computational complexity and typically expect strings to be completely known in advance to calculate their value.
Multiple Worlds, Strict Equality An alternate approach, illustrated in Figure 3b, is to allow a twin to produce multiple possible outputs for a given input. Each of these outputs corresponds to one of the “possible worlds” the system can be in for given input conditions. Strict equality is then sought between the real-world entity’s output, and one of those possible worlds1. In this setting, the multiple possible worlds can either be represented explicitly (as an enumeration of all possible outputs) or implicitly (through an abstract property that it satisfied by all possible worlds). For example, a numerical value associated with a precision interval counts as an abstract representation of multiple exact numerical values.
The multi-world trace semantics has been used to address the question of runtime verification with uncertainty [23, 29], and could be adapted to the problem of stream comparison for digital twins.
In this paper, we have highlighted the connections that can be made between the question of detecting discrepancies between a digital twin and a concrete entity, and the problem of runtime verification already studied in the community of software engineering and formal methods. Although they present clear similarities, these two problems are nevertheless distinct, and some adaptation is therefore necessary in order to leverage existing runtime verification techniques to the particular context of digital twins.
The article identified several research directions aimed at enabling real-time divergence checking using RV techniques, which will be explored in more detail in future work. Among these, we note the design of specification languages that are more expressive and appropriate to the problem of digital twins, as well as the definition of trace comparison metrics that are less strict than a simple position-by-position equality.
1Stated otherwise, the entity’s output must be included in the possible outputs produced by the twin.
Systems, Springer US, 2009, p. 1064. [22] S. Hallé, R. Khoury, Writing domain-specific languages for beepbeep, in: C. Colombo, M. Leucker (Eds.), Runtime Verification - 18th International Conference, RV 2018, Limassol, Cyprus, November 10-13, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science, Springer, 2018, pp. 447–457. doi:10.1007/978- 3- 030- 03769- 7_27. [23] R. Taleb, R. Khoury, S. Hallé, Runtime verification under access restrictions, in: S. Bliudze,
S. Gnesi, N. Plat, L. Semini (Eds.), FormaliSE@ICSE, IEEE, 2021, pp. 31–41. [24] Y. Joshi, G. M. Tchamgoue, S. Fischmeister, Runtime verification of LTL on lossy traces, in:
A. Sefah, B. Penzenstadler, C. Alves, X. Peng (Eds.), SAC, ACM, 2017, pp. 1379–1386. [25] D. A. Basin, F. Klaedtke, S. Marinovic, E. Zalinescu, Monitoring compliance policies over incomplete and disagreeing logs, in: S. Qadeer, S. Tasiran (Eds.), RV, volume 7687 of Lecture Notes in Computer Science, Springer, 2012, pp. 151–167. [26] S. Wang, A. Ayoub, O. Sokolsky, I. Lee, Runtime verification of traces under recording uncertainty, in: S. Khurshid, K. Sen (Eds.), RV, volume 7186 of Lecture Notes in Computer Science, Springer, 2011, pp. 442–456. [27] A. Kaufmann, M. M. Gupta, Introduction to Fuzzy Arithmetic: Theory and Applications,
Van Nostrand Reinhold, 1991. [28] G. Navarro, A guided tour to approximate string matching, ACM Comput. Surv. 33 (2001) 31–88. [29] M. Leucker, C. Sánchez, T. Schefel, M. Schmitz, D. Thoma, Runtime verification for timed event streams with partial information, in: B. Finkbeiner, L. Mariani (Eds.), RV, volume 11757 of Lecture Notes in Computer Science, Springer, 2019, pp. 273–291.