Keywords

1 Introduction

Real-time computer systems, are hardware or software systems which work on the basis of a time schedule [15]. Controller of car engines, networks of wireless sensors and actuators, and multimedia data streaming applications are examples of real-time systems. The correct behavior of real-time systems is achieved by correctness of calculated values as well as the time those values were produced [14, 22]. So, verification of a real-time system requires considering both the functional and time behavior of the systems [15]. In the modeling of real-time systems, presenting nondeterministic time behavior may be required. For example, the best response time of drivers when braking (with a high probability of signal prediction) was reported as a value in the range of 0.7 to 0.75 s [8]. Using time intervals is a widely used notion to model such behavior. Supporting time intervals for nondeterministic time behavior raises challenges in the schedulability analysis of real-time systems [16].

Examples of nondeterministic time behavior in real-time systems include the network delay in communication systems, driver’s reaction time when braking a car, and the execution time of programs on processors. In such cases, determining the exact duration of the tasks is not always possible. Instead, a time interval can be used to specify that the time value will be within a specific range. It is well-known that Worst Case Execution Time (WCET) analysis does not necessarily show the worst time behavior [7]. Hence, using the upper bounds for the actions does not help when analyzing time-sensitive safety properties. In Timed Rebeca, the values of timing primitives are discrete values [12, 13]. Therefore, it is useful to propose an extension on Timed Rebeca for modeling and analyzing real-time systems with time intervals.

Using formal methods, in general, and model checking [6] in particular, is a verification technique which guarantees correctness of systems. Model checking tools for real-time models exhaustively explore state spaces of systems to make sure that given properties hold in all possible executions of the system and specified time constraints are satisfied. Timed Automata and UPPAAL are widely used for modeling and model checking of real-time systems [4]. Timed Automata are automata in which clock constraints (i.e. time interval constraints associated with clocks) can be associated with both transition guards and location invariants [3].

In the context of distributed systems, Actor is used to model systems composed of a number of distributed components communicating via message passing [2, 10]. There are some extensions on the Actor model for modeling real-time systems, e.g. Timed Rebeca [17] and Creol [5], which provide model checking for timed properties such as schedulability and deadlock freedom. Creol models are transformed to timed automata for the model checking purpose which suffers from support for simple expressions for time constrains and state space explosion for middle-sized models. In contrast, Timed Rebeca provides direct model checking toolset; but, only for models with discrete timing primitives [11, 12] as described in detail in Sect. .

In this paper, we extend Timed Rebeca to support modeling and analysis of real-time systems with time intervals (Sect. ). To this end, the notion of Interval-Time Transition System (ITTS) is introduced, which can serve as the basis for the semantic description of timed actor systems. Here, we formally describe the semantics of Timed Rebeca based on ITTS in Sect. . In the second step, we illustrate how the notion of shift equivalence relation for ITTS is used to make the transition system finite, if possible. Using bisimulation method, in Sect. , it is proved that shift equivalence relation can be used for detecting equivalent system states in ITTS.

2 Timed Actors

A well-established paradigm for modeling concurrent and distributed systems is the Actor model. Actor is introduced by Hewitt  [10] as an agent-based language and is later developed as a model of concurrent computation by Agha  [2]. Actors are seen as the universal primitives of concurrent computation, such that each actor provides some services which can be requested by other actors by sending messages to it. Execution of a service of an actor may result in changing the state of the actor and sending messages to some other actors. In [1], Timed Rebeca is introduced as an extension on the actor model for modeling of real-time systems.

2.1 Timed Rebeca

Timed Rebeca is introduced in [1] as the real-time extension of the Rebeca modeling language [18, 19, 21]. We explain Timed Rebeca using the example of a simple Ping-Pong model (taken from [20] with slight modifications). In this model, the ping actor sends pong message to the pong actor and the pong actor sends ping message to the ping actor. A Timed Rebeca model consists of a number of reactive classes, each describing the type of a number of actors (also called rebecs)Footnote 1. There are two reactive classes PingClass and PongClass in the Ping-Pong model (Listing  lines 1 and 16). Each reactive class declares a set of state variables (e.g. lines 5–7). The local state of each actor is defined by the values of its state variables and the contents of its message bag. Communication in Timed Rebeca models takes place by asynchronous message passing among actors. Each actor has a set of known rebecs to which it can send messages. For example, an actor of type PingClass knows an actor of type PongClass (line 3), to which it can send pong message (line 12). Reactive classes may have some constructors that have the same name as the declaring reactive class and do not have a return value (lines 8–10 for PingClass). They may initialize actor’s state variables and put the initially needed messages in the message bag of that actor (line 9). The way of responds to a message is specified in a message server which are methods defined in reactive classes. An actor can change its state variables through assignment statements, makes decisions through conditional statements, communicates with other actors by sending messages (e.g., line 12), and performs periodic behavior by sending messages to itself. Since communication is asynchronous, each actor has a message bag from which it takes the next incoming message. The ordering of the messages in a message bag is based on the arrival times of messages. An actor takes the first message from its message bag, executes its corresponding message server in an isolated environment, takes the next message (or waits for the next message to arrive) and so on.

Finally, the main block is used to instantiate the actors of the model. In the Ping-Pong model, two actors are created receiving their known rebecs and the parameter values of their constructors upon instantiation (lines 26–27).

figure a

Timed Rebeca adds three primitives to Rebeca to address timing issues: delay, deadline and after. A delay statement models the passage of time for an actor during execution of a message server (line 13). Note that all other statements of Timed Rebeca are assumed to execute instantaneously. The keywords after and deadline are used in conjunction with a method call. The term \(\mathtt {after(n)}\) indicates that it takes n units of time for a message to be delivered to its receiver (lines 12 and 21). The term \(\mathtt {deadline(n)}\) expresses that if the message is not taken in n units of time, it will be purged from the receiver’s message bag automatically [1].

2.2 Timed Transition Systems

One way of modeling real-time systems is using timed transition systems [9]. The Semantics of Timed Rebeca is defined in terms of timed transition systems in [11]. In this semantics, the global state of a Timed Rebeca model is represented by a function that maps actors’ ids to tuples. A tuple contains, the state variables valuations, the content of message bags, local time, the program-counter which shows the position of the statements which will be executed to finish the service to the message currently being processed, and the time when the actor resumes execution of the remained statements.

Transitions between states occur as the results of actors’ activities including: taking a message from the mailbox, continuing the execution of statements, and progress of time. In timed transition system of Timed Rebeca, progress of time is only enabled when the other actions are disabled for all of the actors. This rule performs the minimum required progress of time to make one of the other rules enabled. As a result, the model of progress of time in the timed transition system of Timed Rebeca is deterministic. The detailed SOS rules of transition relations are defined in [11].

Figure  shows the beginning part of the timed transition system of the Ping-Pong example. In this figure, \(\sigma \) denotes the next statement in the body of the message server which is being processed. The pair of \(\sigma = \langle ping, 1 \rangle \) in the second state of Fig.  shows that pi executed the statements of its ping message server up to the statement in line 1. In each state, r is the time when the actor can resume the execution of its remained statements. The first enabled actor of the model is pi (as its corresponding reactive class PingClass has a constructor which puts message ping in its bag, line 9), so, the first possible transition is taking message ping. As shown in the detailed contents of the second state (the gray block), taking the message ping results in setting the values of \(\sigma \) and r for the actor pi. The next transition results in executing the first statement of the message server ping and results in putting the message pong in the bag of the actor po with release time 1 (because of the value of after in line 7). Note that the deadline for messages in this model is \(\infty \) as no specific value is set as the deadline for these messages. As the next statement of the message server ping is a delay statement, pi cannot continue the execution. The actor po cannot cause a transition too. So, the only possible transition is progress of time which is by 1 unit from the third to the fourth state.

Fig. 1.
figure 1

The beginning part of the transition system of the Ping-Pong example [20].

Full size image

3 Timed Rebeca with Intervals

The time interval extension to Timed Rebeca enables the use of time intervals with the timing directive after. In this model, a time interval is associated with each state of the transition system. To simplify the presentation of this paper, the time features delay and deadline are omitted. The modified version of Listing  which contains time interval for after directive is presented in Listing . Note that in Line 9, after([4,8]) means that message pong arrives its destination during [4, 8) time units after it has been sent. This value models the nondeterministic delay of the network in message delivery.

figure b

4 Semantics of Timed Rebeca with Intervals

We define the semantics of a Timed Rebeca with Intervals model as an ITTS which is based on the usual transition system semantics for actor systems [11]. Although in timed transition systems (TTS) time intervals can be used as timing constraints on transitions [9], describing the semantics of Timed Rebeca with intervals using TTS makes the semantics complicated, as it does not fit the timing model of TTS. Also, using such semantics as a basis for state space generation and model analysis may result in performance overheads. Thus, it is necessary to define a semantics for Timed Rebeca with intervals which naturally reflects its timing model.

The states in ITTS are composed of the local states of the actor in the system. A key idea behind ITTS is to associate with each state a time interval during which the local states of the actors do not change. The transitions are of two types, namely message processing and time progress. The former includes taking or processing of a message by an actor (which changes the local state of the actor). Time progress transition changes the state of the system by increasing the left end-point of the time interval of the state.

To keep the semantics description focused on timed behavior, we assume the messages do not have parameters, as they do not affect the time behavior of the model. Otherwise, the semantics rules will be cluttered with actual parameters evaluation and scope management.

Before we describe the formal semantics of ITTS, we introduce a few notations that are used throughout the paper.

4.1 Notation and Basic Definitions

We use the notation \( TInterval \) (ranged over by \(\alpha \), \(\beta \), and \(\gamma \)) to denote the set of all time intervals in \(R_{\ge 0}\) which are left-closed right-open or left-closed right-closed. Such intervals are written as \([t_1,t_2)\) and \([t_1,t_2]\) respectively. Time interval \([t_1,t_1]\) corresponds to time value \(t_1\) of Timed Rebeca. For \(\alpha \in TInterval \), \(\alpha _\ell \) and \(\alpha _r\) denotes the left and the right endpoints of \(\alpha \) respectively (regardless of being right-open or right-closed). The notation \(\alpha _{\ell \leftarrow x}\) (resp. \(\alpha _{r\leftarrow x}\)) denote the interval obtained from replacing the left (resp. right) endpoint of \(\alpha \) with x, e.g., \([t_1,t_2)_{r\leftarrow x}\) is \([t_1,x)\).

For a function \(f:X\rightarrow Y\), we use the notation \(f[x\mapsto y]\) to denote the function \(\{(a,b)\in f|a\ne x\}\cup \{(x,y)\}\). We also use the notation \(x\mapsto y\) as an alternative to (x, y).

The following notations is used for working with sequences. Given a set A, the set \(A^*\) is the set of all finite sequences over elements of A, ranged over by \(\sigma \) and \(\sigma '\). For a sequence \(\sigma \in A^*\) of length n, the symbol \(a_i\) denotes the \(i^\mathrm {th}\) element of the sequence, where \(1\le i\le n\). In this case, we may also write \(\sigma \) as \(\langle a_1,a_2,\ldots ,a_n\rangle \). The empty sequence is represented by \(\epsilon \), and \(\langle h|T\rangle \) denotes a sequence whose first element is \(h\in A\) and \(T\in A^*\) is the sequence comprising the elements in the rest of the sequence. For \(x\in A\) and \(\sigma ,\sigma '\in A^*\), the expressions \(x\oplus \sigma \) and \(\sigma \oplus x\) denote a sequence obtained from prepending and appending x to \(\sigma \) respectively. Also, \(\sigma \oplus \sigma '\) is the sequence obtained by concatenating \(\sigma '\) to the end of \(\sigma \). The deletion operator is defined such that \(\sigma \ominus x\) is the sequence obtained by removing the first occurrence of x in \(\sigma \). Finally, we define the membership operator for sequences as \(x\in \langle a_1,a_2,\ldots ,a_n\rangle \overset{ def }{=} \exists 1\le i\le n\cdot a_i=x\).

\( VName \) is defined as the set of all variable names in the model, and \( Value \) as the set of all values the state variables can take. We do not address typing issues in this paper to keep the focus on time behavior of the actors. Let \( Stat \) denote the set of all statements appearing in the actors’ message handlers, \( MName \) denote the set of all message names, and \( ActorID \) denote the set of all unique identities of the actors. The function \( body : ActorID \times MName \rightarrow Stat \) is defined such that \( body (x,m)\) returns the sequence of statements in the body of the message handler of m in the actor with ID x. The set \( Act \) is defined as \( MName \cup \{\tau \}\cup \{ TP \}\).

4.2 Messages and Message Bags

A message in ITTS is a tuple \(( sID , rID ,m,\alpha )\), where \( rID \) and \( sID \) denote the receiver ID and the sender ID respectively, m denotes the message name, while \(\alpha \) denotes the “after” interval. It means that this message arrives its destination during \(\alpha \) time units after it has been sent. The set of all messages is defined as \( Msg \). In ITTS, each actor has an associated message bag that holds all its received messages. The set of all message bags is defined as \( Bag ( Msg )= Msg ^{*}\). For the notation to be simpler, message bags are written in the form of sequences. But it is not necessary for message bags to be sequences, as they can be defined as multisets in general.

4.3 States in ITTS

The system state is composed of the local states of the actors in the system. The local state of an actor with ID x, is defined as the triple \((v_x, mb _x,\sigma _x)\), where \(v_x\) is the valuation function of the state variables of the actor, \( mb _x\) is the message bag of the actor, and \(\sigma _x\) denotes the sequence of statements the actor is going to execute in order to finish the processing of the message being handled. The set of all local states of the actors is denoted as \( ActorState =( VName \rightarrow Value )\times Bag ( Msg )\times Stat ^{*}\).

A (global) system state in ITTS is a tuple \((s,\alpha )\), where \(s\in ActorID \rightarrow ActorState \) is a function mapping each actor ID to its local state, and \(\alpha \in TInterval \) is the time interval associated with the system state. It is assumed that S is the set of all possible system states, ranged over by gs (short for global state). In the initial system state, we let the time interval of the system state to be [0, 0].

4.4 Order of Events in ITTS

As stated before, to define time progress transitions, we must determine the earliest time in which a change is possible in the local state of an actor (called an event). As such changes happen only as a result of taking or executing a message, the earliest and the latest times the messages can be taken determine the order of events in the system. To specify the ordering of the events, a message bag is defined for every system state called “system state message bag”, denoted by \(B( gs )\), which consists of all messages in message bags of all actors in that system state (which may contain duplicate messages).

The ordering of the events regarding to a state \(gs\in S\) is denoted by \( EE _i( gs )\) which is the \(i^{\mathrm {th}}\) smallest value in the set of all lower and upper bounds of the time intervals of all messages in \(B( gs )\).

4.5 Transitions Definition

As explained before, transitions in ITTS are classified into two major types: message processing and time progress. The former includes taking a message from message bag or processing a message by an actor. As with Timed Rebeca, we assume executing the statements in a message server is instantaneous.

Message Processing. For a system state \((s,\alpha )\) we call an actor x idle, if it has no remaining statement to execute from its previously taken message. If such an actor has a message in its mailbox whose after interval starts from \(\alpha _\ell \), a message processing transition can take place:

$$\begin{aligned} \frac{ gs =(s,\alpha )\in S\wedge s(x)=(v, mb ,\epsilon )\wedge msg =(y,x,m,\beta )\in mb \wedge \beta _\ell =\alpha _\ell }{ gs \overset{m}{\rightarrow }(s[x\mapsto (v\cup \{ ( self , x), ( sender , y)\}, mb \ominus msg , body (x, msg ))],\alpha )} \end{aligned}$$
(1)

The execution of each statement in the body of a message handler is considered an internal action in ITTS. The statements such as assignments, conditionals and loops only alter the local state of the executing actor. The only statement that affects the state of other actors is send which may put a message in another actor’s message bag. The semantics of send and assignment statements are stated here and the others are left out to save space.

An assignment statement of the form \( var = expr \) overrides the value of \( var \) in the executing actor’s state variables to the value of the expression \( expr \), denoted by \( eval _x( expr )\). To keep the description simple, it is assumed that the message servers do not have local variables, so the left side of the assignment is always a state variable of the actor executing the message server.

$$\begin{aligned} \frac{ gs =(s,\alpha )\in S\wedge s(x)=(v, mb ,\langle var = expr |\sigma \rangle )}{ gs \rightarrow (s[x\mapsto (v[ var \mapsto eval _x( expr )], mb ,\sigma )],\alpha )} \end{aligned}$$
(2)

The send statement \(y.m() after \ \gamma \) denotes sending a message m with the after interval \(\gamma \) to the receiver y. The semantics of the send statement is defined as

$$\begin{aligned} \frac{ gs =(s,\alpha )\in S\wedge s(x)=(v, mb ,\langle y.m() after \ \gamma |\sigma \rangle ) \wedge s(y)=(v', mb ',\sigma ')}{ gs \rightarrow (s[x\mapsto (v, mb ,\sigma )][y\mapsto (v', mb '\oplus (x,y,m,\beta ),\sigma ')],\alpha _{r\leftarrow t})} \end{aligned}$$
(3)

where \(\beta \) is the interval whose left and right endpoints are \(\alpha _\ell +\gamma _\ell \) and \(\alpha _r+\gamma _r\) respectively, and is right-closed if both \(\alpha \) and \(\gamma \) are right-closed and is right-open otherwise. Furthermore, \(t= min (\alpha _r, \beta _\ell )\) which means that after the message is sent, \(\beta _\ell \) may be the second earliest event, replacing \(\alpha _r\) in that case.

Time Progress. In ITTS, two types of time progress transitions are defined. The first type corresponds to the case that the only possible transition is time progress, while for the second type, a nondeterministic choice between time progress and another transition is enabled.

Type 1 Time Progress Transition: If the lower bound of the time interval for a system state \( gs \) is smaller than the earliest event of that system state (\(\alpha _\ell < EE _1( gs )\)), the only possible transition is time progress. After executing Type 1 time progress transition, the time interval for the successor state is \([ EE _1( gs ), EE _2( gs ))\).

$$\begin{aligned} \frac{ gs =(s,\alpha ) \wedge \alpha _\ell < EE _1( gs )}{ gs \overset{ TP }{\rightarrow }(s,[ EE _1(gs), EE _2(gs))} \end{aligned}$$
(4)

Type 2 Time Progress Transition: In ITTS, in situations which in a system state, time progress transition and at least one other transition are enabled, second type of time progress transition can occur. Consider a global state \( gs =(s,\alpha )\). Unlike Type 1 transitions we have \(\alpha _\ell = EE _1( gs )\), so there exists a message \( msg _1\) in the system with interval \(\beta \) such that \(\alpha _\ell =\beta _\ell \). Now, if no other message exists which can be taken before \(\beta _r\), the only possible transition from \( gs \) is to take \( msg _1\) and there is no time progress transition. Hence, there must be a message \( msg _2\) in the system with interval \(\gamma \) such that \( EE _2( gs )=\gamma _\ell \) and \(\beta _\ell \le \gamma _\ell <\beta _r\). In such a state \( gs \), two transitions are possible: taking \( msg _1\), and waiting till \(\gamma _\ell \). Note that this nondeterminism enables the interleaving of processing \( msg _1\) and \( msg _2\).

To model this type of time progress, we shift the lower bound of the time interval of \( msg _1\) from \(\beta _\ell \) to \(\gamma _\ell \) and update the time interval of the global state accordingly. Note that there may be multiple messages that start from \(\beta _\ell \). Hence, we define the function \( ds \) (short for delay starts), such that \( ds ( mb , t)\) changes the lower bound of the messages in \( mb \) which start earlier than t to t. Formally,

$$ \begin{array}{rcl} ds (\epsilon , t) &{} = &{} \epsilon \\ ds (\langle (x,y,m,\alpha |T\rangle , t) &{} = &{} \langle (x,y,m,\alpha _{\ell \leftarrow max (\alpha _\ell ,t)})| ds (T,t)\rangle \end{array} $$

We lift the definition of \( ds \) to the function s which returns the local state of the actors:

$$ ds (s, t)=\{x\mapsto (v, ds ( mb ,t),\sigma )| x\mapsto (v, mb ,\sigma )\in s\} $$

Now, we can define Type 2 time progress transitions as below.

$$\begin{aligned} \frac{ gs =(s,\alpha ) \wedge \alpha _\ell = EE _1(gs) \wedge (x,y,m,\gamma )\in B( gs ) \wedge \gamma _\ell = EE _2( gs )}{ gs \overset{ TP }{\rightarrow }( ds (s, EE _2(gs)),[ EE _2(gs), EE _3(gs))} \end{aligned}$$
(5)

Figure  shows part of the ITTS of the Ping-Pong example of Listing  which is generated based on the proposed semantics of this section.

5 Making State Space Finite

Based on the semantics of Timed Rebeca, there is no explicit time reset operator in the language; so, the progress of time results in an infinite number of states in ITTS of models. However, reactive systems which generally show periodic or recurrent behaviors are modeled using Timed Rebeca, i.e. performing recurrent behaviors over infinite time. This fact enables us to propose the notion for equivalence relation between two states with time intervals, aiming to make ITTSs finite, called shift equivalence relation in ITTS. The idea of defining shift equivalence relation in states of ITTSs is inspired from [12]. Intuitively, in the shift equivalence relation two states are equivalent if and only if they are the same except for the parts related to the time and the timed parts can be mapped by shifting them with an specific value.

5.1 Shift Equivalence Relation in ITTS

In the first step, the shift equivalence of two time intervals with distance \(c\in R\) is defined as:

$$\begin{aligned} \alpha \approx _{c}\alpha '\overset{ def }{=}\alpha '_{\ell }=\alpha _{\ell }+c\wedge \alpha '_{r}=\alpha _{r}+c \end{aligned}$$
(6)

Then, the shift equivalence of two messages with distance \(c\in R\) is defined as:

$$\begin{aligned} \forall sID , rID \in ActorID ,m&\in MName ,\beta ,\beta ' \in TInterval\ \cdot \nonumber \\&\,\,\,\, ( sID , rID ,m,\beta )\approx _{c} ( sID , rID ,m,\beta ')\Leftrightarrow \beta \approx _{c}\beta ' \end{aligned}$$
(7)
Fig. 2.
figure 2

A part of the interval time transition system of the Ping-Pong example. The transition from \( gs _{1}\) to \( gs _{3}\) is a take message transition. The transition from \( gs _{3}\) to \( gs _{4}\) is an internal transition. The transition from \( gs _{4}\) to \( gs _{5}\) is a Type 1 time progress. The transition from \( gs _{1}\) to \( gs _{2}\) is a Type 2 time progress.

Full size image

Using Eq. 7, the shift equivalence of two message bags \(B=\langle m_{1},...,m_{n}\rangle \) and \(B'\langle m'_{1},...,m'_{n}\rangle \) with distance \(c\in R\) is defined as:

$$\begin{aligned} B\approx _{c}B'\Leftrightarrow \exists 1\le i\le n,1\le i'\le n\cdot m_{i}\approx _{c}m'_{i}\wedge B\ominus m_{i}\approx _{c}B'\ominus m'_{i'} \end{aligned}$$
(8)

Now, the shift equivalence of two local states of an actor with ID x with distance \(c\in R\) is defined as:

$$\begin{aligned} (s(x)=(v_{x}, mb _{x},\sigma _{x})\big )\equiv _{c}\big (s'(x)&=(v'_{x}, mb '_{x},\sigma '_{x})\big )\Leftrightarrow \nonumber \\&\qquad \quad v_{x}=v'_{x}\wedge \sigma _{x} = \sigma '_{x} \wedge mb _{x}\approx _{c} mb '_{x} \end{aligned}$$
(9)

Consequently, the shift equivalence of two system states gs and \(gs'\) (\(gs,gs'\in S\)) with distance \(c\in R\) is defined as:

$$\begin{aligned} \big ( gs =(s ,\alpha )\big )\equiv _{c}\big (gs'=(s',\alpha ')\big )\Leftrightarrow \alpha \approx _{c}\alpha '\wedge \forall x\in ActorID . s(x)\equiv _{c}s'(x) \end{aligned}$$
(10)

5.2 Shift Equivalence Relation in ITTS Is a Bisimulation Relation

The shift equivalence relation aims to make ITTSs of models finite. To this end, we have to show that there is a timed bisimulation relation between finite and infinite ITTSs of a given model to prove that they preserve the same set of timed branching-time properties (i.e., \(\equiv _{c}\) is a bi-simulation relation). To this end, the following theorem should be proven:

Theorem 1

\(\forall ( gs _{1}, gs '_{1})\in \equiv _{c}\) and \(\forall a \in Act \):

$$\begin{aligned} \forall gs _{2}\in S. gs _{1}\overset{a}{\rightarrow } gs _{2}\Rightarrow \exists gs '_{2}\in S. gs '_{1}\overset{a}{\rightarrow } gs '_{2}\wedge ( gs _{2}, gs '_{2})\in \equiv _{c} \end{aligned}$$
(11)
$$\begin{aligned} \forall gs '_{2}\in S. gs '_{1}\overset{a}{\rightarrow } gs '_{2}\Rightarrow \exists gs _{2}\in S. gs _{1}\overset{a}{\rightarrow } gs _{2}\wedge ( gs _{2}, gs '_{2})\in \equiv _{c} \end{aligned}$$
(12)

To prove the first condition of bisimulation relation (i.e., Eq. (11)) it has to be proven that it holds for for all transition types in ITTS.

Take Message Transitions: Assume that \( gs _{1}=(s_{1},\alpha )\), \(s_{1}(x)=(v_{x}, mb _{x},\epsilon )\), \( msg =(y,x,m,\beta )\in mb _{x}\) and \(\beta _{\ell }=\alpha _{\ell }\). Thus take message transition is enabled in \( gs _{1}\) and \( gs _{1}\overset{m}{\rightarrow } gs _{2}\). Assume that \( gs '_{1}=(s'_{1},\alpha ')\), \(s'_{1}(x)=(v'_{x}, mb '_{x},\epsilon )\) and \( gs _{1}\equiv _{c} gs '_{1}\). Therefore \(\alpha '_{\ell }=\alpha _{\ell }+c\). From \(s_{1}(x)\equiv _{c}s'_{1}(x)\), it can be concluded that a message \( msg '\) exists in \( mb '_{x}\) such that \( msg \approx _{c} msg '\). Thus \(msg'\) is of the form \((y,x,m,\beta ')\) such that \(\beta '_{\ell }=\alpha '_{\ell }\) and \(\beta '_{r}=\beta _{r}+c\). Therefore take message transition is enabled in \( gs '_1\). Hence, \( gs '_{2}\) exists in ITTS such that \( gs '_{1}\overset{m}{\rightarrow } gs '_{2}\). From Eq. (1), It can be concluded that:

$$\begin{aligned} \begin{array}{c} gs _{2}=(s_{2},\alpha )= (s_{1}[x\mapsto (v_{x}\cup A, mb _{x} \ominus msg , body (x, msg )],\alpha )\\ gs '_{2}=(s'_{2},\alpha ')= (s'_{1}[x\mapsto (v'_{x}\cup A, mb '_{x} \ominus msg ', body (x, msg ')],\alpha ')\\ A=\{ ( self ,x),( sender ,y)\} \end{array} \end{aligned}$$

To prove that \( gs _{2}(x)\equiv _{c} gs '_{2}(x)\), the following points should be considered:

  1. 1.

    \(s_{1}(x)\equiv _{c}s'_{1}(x)\Rightarrow v_{x}=v'_{x} \)

    \(\Rightarrow v_{x}\cup \{ ( self ,x),( sender ,y)\}=v'_{x}\cup \{ ( self ,x),( sender ,y)\}\)

  2. 2.

    \( mb _{x}\approx _{c} mb '_{x}\wedge msg \approx _{c} msg '\Rightarrow mb _{x}\ominus msg \approx _{c} mb '_{x}\ominus msg '\)

  3. 3.

    \( msg \approx _{c} msg '\Rightarrow body (x, msg )= body (x, msg ')\)

  4. 4.

    \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow \alpha \approx _{c}\alpha '\)

Based on the above equations, \( gs _{2}\equiv _{c} gs '_{2}\) can be concluded, which is required for proving Eq. 11.

Internal Transitions: Assuming that \( gs _{1}=(s_{1},\alpha )\), \( gs '_{1}=(s'_{1},\alpha ')\), \( gs _{1}\equiv _{c} gs '_{1}\), two cases are possible:

  • Assignment Statement: Assume that \(s_{1}(x)=(v_{x}, mb _{1x},\langle var = expr |\sigma _{x} \rangle )\). Therefore internal action is enabled in \( gs _{1}\) and \( gs _{1}\overset{\tau }{\rightarrow } gs _{2}\). From \( gs _{1}\equiv _{c} gs '_{1}\), it can be concluded that \(s_{1}(x)\equiv _{c}s'_{1}(x)\), so \(s'_{1}(x)=(v_{x}, mb '_{1x},\langle var = expr |\sigma _{x} \rangle )\). Thus internal action is enabled in \( gs '_{1}\) and \( gs '_{1}\overset{\tau }{\rightarrow } gs '_{2}\). The produced next states \( gs _{2}\) and \( gs '_{2}\) are:

    $$\begin{aligned} gs _{2}=(s_{1}[x\mapsto (v_{x}[ var \mapsto eval _{x}( expr )],mb_{1x},\sigma _{x})],\alpha )\\ gs '_{2}=(s'_{1}[x\mapsto (v_{x}[ var \mapsto eval _{x}( expr )],mb'_{1x},\sigma _{x})],\alpha ') \end{aligned}$$

    To prove that \( gs _{2}\equiv _{c} gs '_{2}\), the following points should be considered:

    1. 1.

      \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow \alpha \approx _{c}\alpha '\)

    2. 2.

      \(s_{1}(x)\equiv _{c}s'_{1}(x)\Rightarrow mb _{1x}\approx _{c} mb '_{1x}\)

    On the basis of the above results (1,2), \( gs _{2}\equiv _{c} gs '_{2}\) can be concluded.

  • Send Statement: Assume that \(s_{1x}=(v_{x}, mb _{1x},\langle y.m() after \ \gamma |\sigma _{x}\rangle )\) such that \(\gamma _{\ell }\) and \(\gamma _{r}\) are relative time values and \(s_{1y}=(v_{y}, mb _{1y},\sigma _{y})\). After executing send statement in \( gs _{1}\), \( msg =(x,y,m,\beta )\) will be appended to \( mb _{1y}\) such that \(\beta _{\ell }=\alpha _{\ell }+\gamma _{\ell }\) and \(\beta _{r}=\alpha _{r}+\gamma _{r}\). From \( gs _{1}\equiv _{c} gs '_{1}\), it can be concluded that \(s'_{1x}=(v_{x}, mb '_{1x},\langle y.m() after \ \gamma |\sigma _{x}\rangle )\) and \(s'_{1y}=(v_{y}, mb '_{1y},\sigma _{y})\) exist in ITTs. After executing send statement in \( gs '_{1}\), \( msg '=(x,y,m,\beta ')\) will be appended to \( mb '_{1y}\) such that \(\beta '_{\ell }=\alpha '_{\ell }+\gamma _{\ell }\) and \(\beta '_{r}=\alpha '_{r}+\gamma _{r}\):

    $$\begin{aligned} mb _{2y}= mb _{1y}\oplus msg = mb _{1y}\oplus (x,y,m,\beta )\\ mb '_{2y}= mb '_{1y}\oplus msg '= mb '_{1y}\oplus (x,y,m,\beta ') \end{aligned}$$

    Time interval of \( gs _{2}\) is \(\alpha _{r\leftarrow t}\) such that \(t= min (\alpha _{r},\beta _{\ell })\) and Time interval of \( gs '_{2}\) is \(\alpha '_{r\leftarrow t'}\) such that \(t'= min (\alpha '_{r},\beta '_{\ell })\):

    $$\begin{aligned} gs _{2}=(s_2,\alpha _{r\leftarrow t})=(s_1[x\mapsto (v_{x}, mb _{1x},\sigma _{x})][y\mapsto (v_{y}, mb _{2y},\sigma _{y})],\alpha _{r\leftarrow t})\\ gs '_{2}=(s'_2,\alpha '_{r\leftarrow t'})=(s'_1[x\mapsto (v_{x}, mb '_{1x},\sigma _{x})][y\mapsto (v_{y}, mb '_{2y},\sigma _{y})],\alpha '_{r\leftarrow t'}) \end{aligned}$$

    To prove the equivalency of \( gs _{2}\) and \( gs '_{2}\), the following points should be considered:

    1. 1.

      \(s_{2}(x)\equiv _{c} s'_{2}(x)\)

    2. 2.

      \(msg\approx _{c} msg'\wedge mb_{1y}\approx _{c} mb'_{1y} \Rightarrow mb_{2y}\approx _{c} mb'_{2y}\Rightarrow s_{2}(y)\equiv _{c} s'_{2}(y)\)

    3. 3.

      \(\alpha _{r\leftarrow t}\approx _{c} \alpha '_{r\leftarrow t'}\)

    On the basis of the above results (1–3), it can be concluded that \( gs _{2}\equiv _{c} gs '_{2}\).

So, in both cases of internal transitions, \( gs _{2}\equiv _{c} gs '_{2}\) as required for proving Eq. 11.

Time Progress Transition: In ITTS, two types of time progress transitions were defined (Eq. 4 and 5). So, it has to be proven that the first condition holds for these two types. In the following, we assume that \( gs _{1}=(s_{1},\alpha )\), \( gs '_{1}=(s'_{1},\alpha ')\), \( gs _{1}\equiv _{c} gs '_{1}\).

  • Type 1 Time Progress Transition: Assume that Type 1 time progress transition is enabled in \( gs _{1}\). On the basis of (4), \(\alpha _{\ell }< EE _{1}( gs _{1})\) and \( gs _{1}\overset{ TP }{\rightarrow } gs _{2}\). From \( gs _{1}\equiv _{c} gs '_{1}\), it can be concluded that \(\alpha '_{\ell }< EE _{1}( gs '_{1})\). Therefore Type 1 time progress transition is enabled in \( gs '_{1}\) and \( gs '_{1}\overset{ TP }{\rightarrow } gs '_{2}\). According to Eq. (4), \( gs _{2}\) and \( gs '_{2}\) are of the following forms:

    $$\begin{aligned} gs _{2}=(s_{1},[ EE _{1}( gs _{1}), EE _{2}( gs _{1})))\\ gs '_{2}=(s'_{1},[ EE _{1}( gs '_{1}), EE _{2}( gs '_{1}))) \end{aligned}$$

    To prove that \( gs _{2}\equiv _{c} gs '_{2}\), the following points should be considered:

    1. 1.

      \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow s_{1}\equiv _{c}s'_{1}\)

    2. 2.

      \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow EE _{1}( gs '_{1})= EE _{1}( gs _{1})+c\wedge EE _{2}( gs '_{1})= EE _{2}( gs _{1})+c\Rightarrow [ EE _{1}( gs _{1}), EE _{2}( gs _{1}))\approx _{c}[ EE _{1}( gs '_{1}), EE _{2}( gs '_{1}))\)

    On the basis of the above results (1,2), \( gs _{2}\equiv _{c} gs '_{2}\) can be concluded.

  • Type 2 Time Progress Transition: Assume that Type 2 time progress transition is enabled in \( gs _{1}\). On the basis of Eq. (5), \(\alpha _{\ell }= EE _{1}( gs _{1})\) and message \((x,y,m,\gamma )\) exists in \(B( gs _{1})\) such that \(\gamma _{\ell }= EE _{2}( gs _{1})\). Therefore \( gs _{1}\overset{ TP }{\rightarrow } gs _{2}\). On the basis of \( gs _{1}\equiv _{c} gs '_{1}\), it can be concluded that \(\alpha '_{\ell }= EE _{1}( gs '_{1})\) and message \((x,y,m,\gamma ')\) exists in \(B( gs '_{1})\) such that \(\gamma '_{\ell }= EE _{2}( gs '_{1})\). Therefore Type 2 time progress transition is enabled in \( gs '_{1}\) and \( gs '_{1}\overset{ TP }{\rightarrow } gs '_{2}\). According to Eq. (5), \( gs _{2}\) and \( gs '_{2}\) are of the following forms:

    $$\begin{aligned} gs _{2}=(s_{2},[ EE _{2}( gs _{1}), EE _{3}( gs _{1})))=( ds (s_{1}, EE _{2}( gs _{1})),[ EE _{2}( gs _{1}), EE _{3}( gs _{1})))\\ gs '_{2}=(s'_{2},[ EE _{2}( gs '_{1}), EE _{3}( gs '_{1})))=( ds (s'_{1}, EE _{2}( gs '_{1})),[ EE _{2}( gs '_{1}), EE _{3}( gs '_{1}))) \end{aligned}$$

    To prove that \( gs _{2}\equiv _{c} gs '_2\), the following points should be considered:

    1. 1.

      \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow ds (s_{1}, EE _{2}( gs _{1}))\equiv _{c} ds (s'_{1}, EE _{2}( gs '_{1}))\Rightarrow s_{2}\equiv _{c}s'_{2}\)

    2. 2.

      \( gs _{1}\equiv _{c} gs '_{1}\Rightarrow [ EE _{2}( gs _{1}), EE _{3}( gs _{1}))\approx _{c}[ EE _{2}( gs '_{1}), EE _{3}( gs '_{1}))\)

    On the basis of the above results (1,2), it can be concluded that \( gs _{2}\equiv _{c} gs '_{2}\).

Therefore Eq. 11 holds for both types of time progress transitions.

The proof of the second condition of the bisimulation relation (i.e. Eq. 12) is almost the same as the first condition and omitted from this paper because of lack of space.

6 Conclusion

The correctness of behavior in real-time systems, depends on the calculated values and the time of producing theses values [14, 22]. In many real life applications, nondeterministic time behavior is present; In such circumstances, time intervals can be used to define the time behavior of a real-time system.

In this paper, a time interval extension to Timed Rebeca was presented. Timed Rebeca with intervals can be used for modeling real-time systems with nondeterministic time behavior. Using this method, the models of such real-time systems can be described with a high-level language and they can be efficiently analyzed. The semantics of Timed Rebeca with intervals models was defined as Interval Time Transition System (ITTS). In ITTS, every time feature is defined as an interval of non-negative real numbers. A time interval is associated with every system state. The semantics of ITTS was explained and messages, system states, and transitions for different action types were defined. Using the presented semantics, the state space of timed actor systems with time intervals could be generated. In order to determine equivalent system states, shift equivalence relation in ITTS was defined. Using bi-simulation method, it was proved that shift equivalence relation in ITTS could help detect equivalent system states. In many cases with finite time intervals, state space explosion could be prevented using shift equivalence relation in ITTS.

Other equivalence relations can be proposed in the future for detection of equivalent states in cases with infinite time intervals. Another line of research is implementation of the proposed semantics and testing its efficiency on actor models.