We provide a formal model based on extended state machines (EFSMs) with the addition of so-called admissibility functions to describe the state changes of an asset for interactions between HTTP agents and the asset by using the abstraction of properties, actions, and events. Furthermore, we describe the RESTful interface for assets that can be derived from EFSMs to ofer assets' interactions in a clearly defined way and based on established standards. We use the continuous example of a robot arm to explain our results and provide the complete interaction model for the robot arm.
In the past semantic digital twins have been built by enriching machine data with semantics
(using RDF uplifting) and making that data available [
The question arises, what the RDF that must be sent to the digital twin in order to control it, should look like. For this purpose it is very helpful to have a clearly defined interface with clear semantics for the interactions between agents and digital twins, i.e. we need an interaction model that can be formally described. This will also easy automatic composition or orchestration of several semantic digital twins.
For the interface, it makes sense to build on technologies that support semantics and are already well established for companies. Thus we want to build the interface on existing Web technologies like REST, HTTP, and RDF. Utilizing these technologies makes a semantic digital twin even more useful because it can be easily integrated into the existing IT infrastructure of companies, the number of semantic digital twins can be scaled up massively and data can be integrated among all those twins in a straightforward way.
In view of the above considerations, we will treat a digital twin as a read-write interface for assets, additional services (e.g. a predictive maintenance model) that are often seen as an integral part of a digital twin can be implemented in a decoupled way as microservices on top of that read-write interface of the digital twin.
In this paper, we provide a formal model based on extended finite state machines for the semantics of interactions between HTTP agents and digital twins. This model can be used to clearly define what efects a certain interaction with an asset has on its current state.
In the next section, we describe the related work. In Section 3 we briefly introduce the two concepts we are building our work upon, namely REST and extended finite state machines. In Section 4 we describe our formal interaction model and in Section 5 the related RESTful interface. In Section 6 we give a short discussion of the results and conclude our work in Section 7.
The Web of Things (WoT) is an initiative to solve the increasing fragmentation of Internet
of Things devices (i.e. the fact that one needs a new app for every device) by proposing a
uniform application layer: the web. One central concept of the WoT are the so-called Thing
Descriptions which are a semantic self-description of a device and its capabilities. Charpenay
et al. [
Ewert et al. [
Harth and Käfer [
Gómez-Berbís and de Amescua-Seco [
Boje et al. [
Representational State Transfer (REST) is an architecture style for distributed software systems
introduced by Fielding [
For our work, the most important point in this enumeration is resource manipulation through representations. This means that in RESTful architectures, the state of resources cannot be changed by some explicit operation but only by submitting its new state to the resource. Suppose, e.g. we have a resource ”counter” that has the state ”3”. When we want to increase the counter by one, we cannot just call an operation ”increaseByOne” that does the increment but we explicitly have to tell the ”counter” that its new state should be ”4” (in case of HTTP often done using a PUT request).
REST constraints are quite general and could be applied to many technologies, most of the time, however, the REST principles are used for building scalable HTTP APIs. Because of the popularity of HTTP-based REST APIs on the Web, we also want our interaction model for semantic Digital twins to comply with the REST constraints. This makes it easy to interface with existing Web-based infrastructure as well as to scale up the number of semantic digital twins in use, as needed when using them in large-scale factories.
Extended finite state machines (EFSMs) [
Informally, EFSMs extend FSMs by adding stateful variables to the machine, i.e. the current state of the machine is defined by an assignment of those variables together with the current symbolic state of the machine (which is comparable to the state in traditional FSMs). The current assignment of the variables is also used to determine which transitions from the current symbolic state to another one are allowed (enabled) and which are not.
The EFSM model assumes that variables are only changed when a transition happens and the way they are changed is defined in the update function for the transition. However, as we want our system to conform to the REST constraints, we need to take into account the fact, that the state of an asset can be manipulated directly and arbitrarily through the use of representations. This means that we cannot assume that the variable assignment will always stay the same while the EFSM is in the same symbolic state (as it could be changed using e.g. an HTTP PUT request). Nevertheless, we need to define which variable assignments are valid for a certain symbolic state2 and thus slightly extend the EFSM model by an admissibility function.
We thus define an EFSM as a 10-tuple = (, , , , , , , ) , where • is the set of symbolic states, • is a set of input symbols, • is a set of output symbols, • is an n-dimensional space 1 × ⋯ × (i.e. the value space of all variables), • is a set of enabling functions such that ∶ → { , } , • is a set of variable update transformations such that ∶ → , • is a transition relation such that ∶ × × → × × and • is the admissibility function such that ∶ × → { , } .
We use ( 1, … , ) = ∈ for the current variable assignment and we write (, , ) → ( ′, , ) to denote that if is in the symbolic state , it holds that () = and input symbol is received, then a transition to the new symbolic state ′ happens where the variables assignment is updated ← () and the output symbol is sent.
For the admissibility and enabling functions we use abbreviations such as 1 < 10 ∧ 2 = to denote the function ( 1, 2) = { if 1 < 10 ∧ 2 = else.
(1) as well as just and for the respective constant functions.
An EFSM can be represented using a graph where the nodes represent the symbolic states and the edges represent the transitions between them. We annotate the admissibility function 1More precisely of finite state transducers 2We need this such that nobody can send a representation with a variable assignment that is (physically) not possible or nonsensical for the asset. for each state at the node and the enabling function and input symbol as well as the update function and output symbol in the form ( , )/(, ) at each transition.
Figure 1 shows an example of an EFSM with the symbolic states = { 0, 1}, the input symbols = {, } , the output symbols = { , } the variable value space = N × { , } , two transitions ( 0, 1 > 5, ) → ( 1, 1 ∶= 7, ) and ( 1, 2 = , ) → ( 0, 1 ∶= 4, ) , and the admissibility function ( 0) = 1 > 3; ( 1) = 1 < 10 ∧ 2 = .
We want to use a robot arm as a running example for the rest of the paper. We assume the robot arm can have three diferent positions, it can sense whether an item is currently in the clamp and it can open and close its clamp. A few of the diferent possible states of the robot arm can be seen in Figure 2. Note that the two conveyor belts are other assets that can interact with the robot arm physically (by moving items) but cannot be controlled directly using the digital twin.
During the rest of this section, we will provide an interaction model for this robot arm by constructing a suitable EFSM. For this purpose will use the established abstractions of properties, actions, and events and explain how these can be represented using our formal model.
We use EFSMs with admissibility functions – in contrast to normal FSMs – for our interaction model to be able to describe the behavior of an asset in a very concise way with as few states as possible and thus prevent a state space explosion which would most of the time lead to having infinitely many states.
In our model properties are represented using the variables of an EFSM where every variable models a distinct property. An EFSM with the variable value space = {1, 2, 3} × { , } × { , } thus could be used to describe the properties of the robot arm. We will use the following variable names: (, , ) ∈ in the following.
As all variables of an EFSM always have a clearly defined value assignment, properties can always be read (by using HTTP GET requests) and return a value.
Writing properties on the other side is subject to some restrictions, as the admissibility function for the current symbolic state needs to allow the new variable assignment that is to be written. This way properties can be made read-only (and thus not be changed from the outside directly) by fixing the value through the admissibility function. If e.g. our EFSM currently is in the symbolic state 0 and ( 0) = ( = ) , then can not be changed to any other value than , i.e. it is read-only (in the current symbolic state). This would reflect the fact that in the physical world there currently is an item under the sensor, and sensors are read-only devices (that cannot make an item disappear). The admissibility function can thus be seen as an invariant over the variables for the current symbolic state.
Also complex interdependencies between diferent variables can be modeled, e.g. by assuming ( 1) = ( = 2 ∧ = ∧ = ) ∨ ( = ) ∨ (! = 2) . Here the possible value for depends on the current value of and which means that when or is changed, also might need to be changed3. We need a property interdependency in this case because a state of the robot arm where the clamp is open in position 2 and an item is sensed at the same time is physically impossible (the item would fall down) and thus must be prohibited. The two states we gave as an example can be seen in Figure 3.
3Note that we do not need transactions or anything similar – the REST principle of resource manipulation through representations makes this possible as we always set the new value for all of our properties.
s0 pos = 1 ∧ item = false (true, B)/ (pos := 1, ε)
s1 pos = 2 ∧ item = false
An important characteristic of properties is that a change of the same must always happen instantaneously. If there is some process in the physical world behind the change of a property, then such a change is often not possible instantaneously. For e.g. the position of a robot arm can not change instantaneously because the arm has to move to the given position first which takes some time; the position of a robot, therefore, is not suitable to be modeled as a property and actions should be used for this purpose instead.
Because there are interactions with an asset (or more specifically with its digital twin) that cannot be modeled using simple properties – namely those where changes to the state do not happen instantaneously but only over a longer period of time, we need to introduce a possibility to execute those interactions. We will call this type of interaction a action.
In the case of the robot arm, such an action would be the movement of the arm between diferent positions. Although there is a property that signals the current position of the robot arm, we cannot use it for setting a new position as the arm would take some time (maybe several seconds) to move there4. We model an action in an EFSM with one or multiple transitions. When an action can be modeled by a single transition the action can be identified with an input symbol of the EFSM.
Let us look at the EFSM that can be seen in Figure 4: We have two symbolic states, 0 that fixes the position to ”1” and 1 that fixes the position to ”2” (while making read-only and making no restrictions about the clamp, both). As already mentioned it would not be appropriate to change the position directly by manipulating the property, but we need a transition for this.
The transition going from 0 to ! that can be seen in the figure has the enabling function (i.e. it is always enabled), the input symbol , the update function ∶= 2 which sets the variable to ”2” (which coincides with the allowed value in symbolic state 1) and the empty output symbol (i.e. it has no output). We can now identify the action ”moveFromPos1ToPos2” with the input symbol , i.e. when an agent wants to execute this action, the input symbol is sent to the EFSM and the corresponding transition is eventually executed (updating the variables among other things). It is important to note that we make no assumption about when the transition is executed after the input symbol is sent because we do not know how long 4Note that we assume a robot arm that moves slowly (moving cannot be modeled using a property) but can close and open its clamp very fast (we assume it happens instantaneously and use a property for it). In practice, it always will depend on the scenario whether ”several seconds” can be treated as instantaneous change or change over a longer period of time.
s0 pos = 2 item = false
(true, A)/ (pos := 3, ε)
s1 pos = 3 item = false
s3 pos = 3 item = true the robot arm will take to move, however, we know the transition will eventually be executed before processing the next input symbol.
The transition from 1 to 0 on the other hand takes the input symbol and sets the position back to ”1”, so the action behind could be seen as the inverse action to the action behind . However, we can also imagine that actions can be parametrized. Then we could have just one action ”moveArm” and depending on the parameter (e.g. a boolean flag for the direction) it is chosen which input symbol is submitted to the EFSM (i.e. there needs to be a mapping from the parameter value space to the set of input symbols).
An action can not always be mapped to just one single transition and consequently not to one single input symbol. This is always the case when there is some interaction with processes in the physical environment. For our robot arm, we could want to make an action ”pickUp” available that picks up a new item when there currently is no item in the clamp. However, the robot arm cannot just spawn items but it needs to go to position ”1”, open its clamp and wait for the conveyor belt to bring an item (we assume that this will always happen if we wait long enough).
To solve this issue we need to introduce the possibility to have transitions that do not need an input symbol to be executed (we then write instead of an input symbol, similar to what we have seen for output symbols and call that transition epsilon or empty transition) but can just happen spontaneously as long as their enabling function is fulfilled. This type of transition can be used to model processes that happen in the environment and which the asset cannot influence directly.
In Figure 5 we can see an EFSM with three transitions: the first one with input symbol moving the arm to position ”3”, the second one being an epsilon transition modeling the fact that an item has arrived at the item sensor and the third one having input symbol closing the clamp. We can now model the action ”pickUp” as the sequence of input symbols [, ] . When an agent wants to execute this action, the symbols and are submitted to the input queue of the EFSM. First, the transition is executed and the robot arm moves to position ”3”. Then it waits for the epsilon transition to happen (for the item to appear) and afterward the transition is executed and the clamp is closed.
For the interaction with an asset not only the current state could be of interest but also what has happened in the past. For e.g. one could want to do something (increasing a counter, etc.) every time the robot arm delivers an item successfully to the conveyor belt at position ”1”. Every type of event can be identified with an output symbol in the EFSM. Thus every time a transition is executed, an event (of the event type belonging to the output symbol) is emitted ( means there is no event to emit).
In Figure 6 we can see an EFSM that represents exactly this case. We have two symbolic states that fix the position to ”1” and an epsilon transition between them that is active when there is an item in the clamp and it is open. As soon as the transition is executed it outputs the symbol . This occurrence of an event can be made available (together with a timestamp) to agents over the HTTP interface.
In the previous section, we explained how properties, actions, and events of an asset can be modeled using an EFSM, i.e. what efects interaction can have, but we only touched on the topic of how the interactions between HTTP agents and the asset themselves work. We now want to describe those interactions more extensively in the following.
The HTTP interface that can be derived from the EFSM is based on the Linked Data Platform
(LDP) [
As explained before the current values of the properties can be read all the time. This can be done using an HTTP GET request to an endpoint representing the robot arm (i.e. its digital twin). An example of an RDF graph the endpoint could return can be seen in Figure 7 where we can see the current value of all the properties. The RDF predicates :pos, :item, and :closed map directly to the variables of the EFSM with the respective name and are used to display the property values as RDF.
If an agent now wants to change a property it must send an HTTP PUT request against the endpoint with the RDF representing the new desired state, e.g. could the ”closed” property be changed to ”false”. The request can either be accepted by the digital twin, then it returns a 204 status code and changes the property, or it can be denied. The denial can have multiple reasons (e.g. could the server be overloaded and return a 503 status code) but the important reason for @prefix : <http://example.org/robotArm#> . </> a :RobotArm ; :pos 1 ; :item false ; :closed true ; :tasks </tasks/> ; :events </events/> . us is when the new property (and thus EFSM variable) assignment is not allowed for the current symbolic state by the admissibility function. In that case, the digital twin would return a ”409 Conflict” status code.
Agents could submit actions to the digital twin by sending a POST request with the needed parameter to an endpoint for the action (e.g. ”/pickUp”). However, this would not be in accordance with the REST principles where we always want to manipulate the state of a resource by sending a representation5. To comply with the REST constraints we create an explicit resource every time an agent wants to execute an action and call that resource a task.
A task specifies which actions should be executed with which parameters (i.e. it can be directly mapped to a sequence of input symbols for the EFSM) and tasks can also specify an order among them (when there are multiple tasks submitted by agents at the same time or shortly after each other, the asset needs to decide which one should be executed next, e.g. using a priority for the tasks).
In Figure 8 we can see the RDF that we get when referencing the task endpoint (which is an LDP container) of the robot arm and all tasks that are listed under this endpoint. We see that the robot arm currently has two tasks, the first being the task ”pickUp”, the second being a move task with a parameter6. ”PickUpTask”, as well as ”MoveTask”, can be directly mapped to a sequence of input symbols for the EFSM (possibly of size one). If an agent wants to create a new task, it can send a POST request against the task container endpoint according to the LDP standard.
Events that are created by assets are read-only for agents, thus we can just deference the event endpoint (again an LDP container) of the robot arm and get a list of events. How these events could look like can be seen in Figure 9. As we have a RESTful architecture events are not 5A POST request to an action-specific endpoint has more similarities with a Remote Procedure Call – an architecture for distributed applications opposing REST.
6As already mentioned we can treat tasks with parameters as equivalent to multiple tasks without parameters, i.e. instead of :MoveTask with a :toPos parameter we could have :MoveToPos1Task, :MoveToPos2Task, etc. @prefix : <http://example.org/robotArm#> . @prefix ldp: <http://www.w3.org/ns/ldp#> . </tasks/1> a :PickUpTask ; :priority 3 . </tasks/> a ldp:BasicContainer ; ldp:contains </tasks/1>, </tasks/2> .
</tasks/2> a :MoveTask ; :toPos 1 :priority 2 . @prefix : <http://example.org/robotArm#> . @prefix ldp: <http://www.w3.org/ns/ldp#> . proactively pushed to agents but instead have to be retrieved regularly by polling them7. By looking at the type of the event, an agent can determine the output symbol which maps to the type and thus which transition has been executed in the past.
In the previous two sections, we described in accordance with [
We defined a soft criterion (instantaneous change) for deciding whether a given capability of an asset should be modeled as a property or as a process defined by an action. We also gave a clear semantic to those actions by mapping them to a sequence of input symbols that can execute transitions – if necessary thereby also interacting with processes from the physical environment.
Events have been defined as the output of a transition, i.e. the result of a state change that can be recorded and made accessible in a RESTful way.
To verify that all of our requirements for the robot arm (moving is not instantaneous, items do appear only at the conveyor belt at position ”3”, etc.) can be expressed using our EFSM model, we give the complete model of the robot arm in Figure 10. We can see that there are diferent symbolic states for every position, such that the position can only be changed using an action. We also have the two epsilon transitions when an item appears at the conveyor belt or is delivered to the other conveyor belt; this is the only way the ”item” property can be changed.
We have four distinct input symbols , , , and each on mapping directly to a move action (e.g. ”moveToPos1”, etc.). There exists one event, namely the already mentioned ”delivery” 7If a use case requires it, pushing events (e.g. using WebSockets) would however not be a problem from our conceptual point of view. represented by the output symbol . Also, note the two transitions that go out of 5 for input symbol : They have two mutually exclusive activation functions as the item is dropped when the clamp is not closed while moving to position ”2” which leads to symbolic state 1 and to symbolic state 4 otherwise when the clamp is closed.
We provided a formal model in the form of EFSMs extended by admissibility functions for the interaction of HTTP agents with the digital twins of arbitrary assets and described a RESTful interface that can be directly derived from the EFSM. This formal model can on the one hand be used to understand the interactions between diferent agents and assets better, on the other hand, it could be communicated to the agent to help it to decide how to interact with the asset. If an agent knows e.g. that it wants to transport an item from one conveyor belt to the other, it could use the EFSM to deduce which properties to change, which tasks to submit, and for which events to wait in which order.
We think that our formal model is general enough, to also have applications outside the field of digital twins, e.g. for describing the semantics of properties, actions, and events for the Web of Things or interactions of general RESTful interfaces. A formal interaction model could be used in these cases for model checking certain properties of an asset’s behavior, e.g. whether there exists a sequence of HTTP requests that leads the asset to a deadlocked state and thus makes it unusable.
In the future, we also plan to investigate the connection between diferent EFSM that can be used to model the same asset. A still open question is if there is a way to transform diferent EFSMs modeling the same asset into each other and if we can define some canonical form. This work was funded by the German Federal Ministry of Education and Research through the MOSAIK project (grant no. 01IS18070A).