A model for real - time concurrent interaction protocols in component interfaces

he set of clocks to be reset by 푒 when it 
 taking 푒1 at time 휏2, and so on, and at last 
 takes place. In the sequel, we will use the 
 transits to 푒⃗⃗⃗ ⃗⃗⃗ at time 휏 . Note that (휈푖−1 +
 subscript 푒 with 휙 and 휆 to indicate that 휙 
 휏푖 − 휏푖−1) is the value of the clock variables 
 and 휆 are associated 
 just before 푒푖’s taking place, and 휈푖 is the value 
 to 푒. 
 of the clock variables just after 푒푖’s taking 
 • ℱ ⊆ 퐿is the set of acceptance locations. place. The behavior 휎 expresses also that the 
 system stays in the location푒⃖⃗⃗푖⃗for 휏푖 − 휏푖−1 
 In this paper, for simplicity, we only 
 time units, and then transits to by 푒⃖⃗푖⃗⃗+⃗⃗⃗1⃗for (1 ≤
consider the deterministic timed automata, i.e. 
 𝑖 ≤ ). If 휎 = (푒1, 휏1)(푒2, 휏2)  (푒 , 휏 ) is a 
those timed automata which do not have more 
 behavior of timed automaton , we call 푒⃗⃗⃗ ⃗⃗⃗ a 
than one -labeled edge starting from a location 
 reachable location of and 〈푒⃗⃗⃗ ⃗⃗⃗, 휈 〉 a 
푠 for any label ∈ Σ. (discrete) reachable state of . A behavior of 
 A clock interpretation 휈 for a set of clock 
 timed automaton is accepted iff 푒⃗⃗⃗ ⃗⃗⃗ ∈ ℱ. Let 
is a mapping 휈: → 푅푒 푙푠, i.e. 휈 assigns to 
 푠푖 = 푒⃗⃗⃗⃗푖, for 1 ≤ 𝑖 ≤ , and 푠0 = 푠 . Then the 
each clock ∈ the value 휈( ). A clock run corresponding to 휎 is the sequence: 
interpretation represents the values of all clocks 푒1 푒2
 〈푠0, 휈0〉 →휏 〈푠1, 휈1〉 →휏 
in at a time point. We adopt the following 1 2 
 →푒 〈푠 , 휈 〉.
denotations. 휈0always denotes the clock 휏 
interpretation which maps from to {0}. For a The finite language of is the set of all 
clock interpretation 휈 and for 푡 ∈ 푅, 휈 + 푡 accepted behaviors of . 
denotes the clock interpretation which maps In order to solve the emptiness problem for 
each clock ∈ to the value 휈( ) + 푡. For 휆 ⊆ a timed automaton, Alur and Dill [1] have 
 , [휆 ↦ 0]휈 is the clock interpretation which introduced a finite index equivalence relation 
assigns 0 to each ∈ 휆 and agrees with 휈 over over the state space of the automaton. The idea 
the rest of the clocks. is to partition the set of the clock interpretations 
 A state of a timed automaton is a pair into a number of regions so that two clock 
〈푠, 휈〉, where 푠 ∈ 퐿 and 휈 is a clock interpretations in the same region will satisfy 
 the same set of clock constraints. 
interpretation for . The fact that is in a state 
 For each ∈ , let 퐾 be the largest integer 
〈푠, 휈〉 at a time instant means that stays in constant occurring in a clock constraint for the 
location 푠 with all clock values agreeing with 휈 clock variable of the timed automaton , i.e. 
at that instant. 
 퐾 = max{ |푒𝑖푡ℎ푒 ≤ or
 The behavior of timed automata can be ≥ occursinaclockconstraint . 
represented by timed words (or timed-stamped of휙ofatransition푒 }.
transition sequences). A behavior 휎 is a timed Let 퐾 = max ∈ 퐾 . 
word For a real number , let ( ) = − ⌊ ⌋ 
 휎 = (푒1, 휏1)(푒2, 휏2)  (푒 , 휏 ), where ≥ (⌊ ⌋ is the maximal integer number which is not 
1 and 푒푖 ∈ , 푒⃗⃗⃗푖⃗−⃗⃗⃗1⃗ = 푒⃖⃗⃗푖⃗ for 1 ≤ 𝑖 ≤ (with the greater than ) be the fractional part of . The 
convention 푒⃗⃗⃗0⃗ = 푠 ), and where 0 = 휏0 ≤ 휏1 ≤ equivalence relation ≅ over the set of clock 
휏2 ≤ ⋯ ≤ 휏 , such that (휈푖−1 + 휏푖 − 휏푖−1) interpretations is defined as follows: for two 
 clock interpretations 휈 and 휈′, 휈 ≅ 휈′ iff the 
 following three conditions are satisfied: 
12 V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15 
 1. For all x ∈ X either ν(x) > Kx ∧ ν′(x) > 〈푠, , 휙, 휆, 푠′〉 such that 훼′ satisfies 
 Kxor ⌊ν(x)⌋ = ⌊ν′(x)⌋. 휙and 훽 = [휆 ↦ 0]훼′, 
 2. For all x, y ∈ X such that ν(x) ≤ Kx and • ℱ′ ⊆ 퐿′such that 푠′ ∈ ℱ′ iff 푠′ = 〈푠, 훼〉 
 ν(y) ≤ Ky, frac(ν(x)) ≤ frac(ν(y)) iff where 푠 ∈ ℱ and 훼 is a clock region. 
 frac(ν′(x)) ≤ frac(ν′(y)). 
 3. For all x ∈ X such that ν(x) ≤ Kx, Note that ℛ( ) is a ‘untimed’automaton, 
 frac(ν(x)) = 0 iff frac(ν′(x)) = 0. and we also denote its (untimed) language 
 When 휈 ≅ 휈′, it is not difficult to see that by ℒ(ℛ( )). 
for any clock constraint 휙 occurring in a We can simplify the automata and ℛ( ) 
 such that all states (locations) are reachable and 
transition 푒 = 〈푠, , 휙, 휆, 푠′〉 ∈ , 휈 satisfies 휙 
 all states can lead to an acceptance state. 
iff 휈′ satisfies 휙. 
 We recall some results from the timed 
 A clock region for is an equivalence 
 automata theory [1] that will be used in our 
class of the clock interpretations induced by ≅. 
 checking procedure later. Let ℒ( ) denote the 
We denote by [휈] the clock region to which a 
 휔-timed language (language of infinite timed 
clock interpretation 휈 belongs. From the 
 words) generated by (by adding 휀-transitions 
definition of ≅, a region is characterized by the 
 from a final state to itself we can extend the 
integer part of the value of each clock when it 
 finite language of to the 휔 language). 
is not greater than 퐾 , by the order between the 
 Theorem 1 
fraction part of the clocks when they are 
 1.For the timed automaton , 
different from 0. Therefore, the number of 
 푛푡𝑖 푒 (ℒ( )) = ℒ(ℛ( )). Therefore, 
clock regions is bounded by | |! ⋅ 2| | ⋅
 the emptiness problem for is decidable. 
∏ (2퐾 + 2). A configuration is defined as 
 ∈ 2. If 〈푠 , 휈 〉 →푒1 〈푠 , 휈 〉 →푒2  →푒 〈푠 , 휈 〉is 
a pair 〈푠, 훼〉 where 푠 ∈ 퐿 and 훼 is a clock 0 0 휏1 1 1 휏2 휏 
region. Based on the clock regions, the region a run from the initial state of then 
 푒1 푒2 푒 
automaton of , whose states are 〈푠0, [휈0]〉 → 〈푠1, [휈1]〉 →  → 〈푠 , [휈 ]〉 
configurations of , and whose transitions are is a run of ℛ( ), and reversely, if 
 푒1 푒2 푒 
the combination of a time transition and a 〈푠0, [휈0]〉 → 〈푠1, [휈1]〉 →  → 〈푠 , [휈 ]〉 
action transition from . There is a time is a run in ℛ( ) then there are 휏1,  , 휏 
transition from 〈푠, 훼〉 to 〈푠, 훽〉 iff 훽 = 훼 + 푡 for such that 
 〈푠 , 휈 〉 →푒1 〈푠 , 휈 〉 →푒2  →푒 〈푠 , 휈 〉 is 
some 푡 (here for 훼 = [휈] we define 훼 + 푡 = 0 0 휏1 1 1 휏2 휏 
[휈 + 푡]). a run from the initial state of . 
 Definition 4 (Region automata) Given a Let in the sequel, for an automaton the 
timed automaton as in Definition 3, the size of (the number of transitions and 
region automaton of is the automaton locations) be denoted by | |. 
ℛ( ) = 〈퐿′, 푠′ , 훴, ′, ℱ′〉, where Now, we return to the problem to decide if 
 • The set of states 퐿′ consists of all 푛푡𝑖 푒 (ℒ(𝒜))|Σ𝑖 ⊆ 푅푖 for a given timed 
 configurations of , automaton 𝒜. It turns out that this problem is 
 • 푠′ = 〈푠 , [휈휃]〉where휈휃 is the clock solvable, and just a corollary of Theorem 1. 
 valuation that assigns 0 to all clock Theorem 2 Given a regular expression 푅푖 
 variables in , and a timed automaton 𝒜 the problem 
 • ′ is the set of transitions of ℛ( ) such 푛푡𝑖 푒 (ℒ(𝒜))|훴𝑖 ⊆ 푅푖 is decidable in 
 that a transition ((푠, 훼), , (푠′, 훽)) ∈ ′ 풪(|ℛ(𝒜)|. |푅푖|) time. 
 iff there is a timed transition from 〈푠, 훼〉 Proof. Let ℬ be an automaton that 
 to 〈푠, 훼′〉 and a transition in recognizes all the strings on Σ푖 that do not 
 belong to 푅푖, i.e. an automaton that recognizes 
 V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15 13 
 Fig. 1. Transitions in 𝒜 and 𝒜′: , ∈ Σ푖, ∈ Σ푖. 
the complement 푅̅푖 of 푅푖. The synchronized by a timed word from ℒ(𝒜). If 훿( ) = 0 for all 
 , then the second condition for is satisfied 
product ℬ ×Σ𝑖 ℛ(𝒜) recognizes the language ∈ Σ푖 𝑖
 ̅ ̅ trivially. Otherwise, Theorem 1 gives that this 
푅푖||ℒ(ℛ(𝒜)) ({푤 | 푤|Σ𝑖 ∈ 푅푖 ∧ 푤|Σ′ ∈
ℒ(ℛ(𝒜))}). It follows Theorem 1 that condition is violated if and only if there is a 
 run
푅̅푖||ℒ(ℛ(𝒜)) = 푅̅푖|| 푛푡𝑖 푒 (ℒ(𝒜)). The 
 푒1 푒2 푒 
emptiness of the language generated by 〈푠0, [휈0]〉 → 〈푠1, [휈1]〉 →  → 〈푠 , [휈 ]〉 
ℬ × ℛ(𝒜) is decidable in 풪(|ℛ × ℛ(𝒜)|) in ℛ(𝒜′) in which there are two transitions 푒푙 
 and 푒푙+ℎ corresponding to resetting clocks 푖 in 
time. But 푅̅푖|| 푛푡𝑖 푒 (ℒ(𝒜)) is empty if and 
only if 푛푡𝑖 푒 (ℒ(𝒜))| ⊆ 푅 . Hence, the 𝒜′: 푒푙 = (〈푠푙, [휈푙]〉, , 〈푠푙+1, [휈푙+1]〉 where ∈
 Σ𝑖 푖 Σ , 휈 ( ) = 0, and 푒 =
theorem is proved. 푖 푙+1 푖 푙+ℎ
 where 
 Now we consider the problem to decide if (〈푠푙+ℎ, [휈푙+ℎ]〉, , 〈푠푙+ℎ+1, [휈푙+ℎ+1]〉 ∈
 Σ , 휈 ( ) = 0, and transitions 
all the strings generated by 𝒜 satisfy the second 푖 푙+ℎ+1 푖
 푒 ,  , 푒 do not have label in Σ (not 
item of Definition 2. Let 𝒜 = 〈퐿, 푠 , Σ, , , ℱ〉. 푙+1 푙+ℎ−1 푖
 corresponding to transitions in 𝒜′ resetting 
Let Σ ⊆ Σ. Let be a new clock variable, 
 푖 푖 clock ) that makes the following condition 
 ∈ . Define 𝒜′ to be the automaton that is 푖
 푖 satisfied: Let the run in 𝒜′ according to 
the same as 𝒜 except that transitions with label 
 Theorem 1 corresponding to that path be 
in Σ푖 will have to reset the clock 푖 as well, i.e. 푒푙 푒푙+ℎ−1
 〈푠푙, 휈푙〉 →휏  →휏
𝒜′ = 〈퐿, 푠 , Σ, ∪ { 푖}, ′, ℱ〉, and ′ = {푒′ = 푙 푙+ℎ−1
(푠, , 휙, ∪ { }, 푠′) | 푒 = (푠, , 휙, , 푠′) ∈ ∧ 〈푠 , 휈 〉 →푒푙+ℎ 〈푠 , 휈 〉
 푖 푙+ℎ 푙+ℎ 휏푙+ℎ 푙+ℎ+1 푙+ℎ+1
 ∈ Σ푖} ∪ {푒′ = (푠, , 휙, , 푠′) | 푒 = Then, 휈푙+ℎ( 푖) + 휏푙+ℎ < 훿( ). This implies the 
(푠, , 휙, , 푠′) ∈ ∧ ∈ Σ푖}We illustrate the following: After having removed all non-
difference of transitions in 𝒜 and 𝒜′ in Fig. 1. reachable states from ℛ(𝒜′), and adding time 
 transitions (labeled with “time”) to ℛ(𝒜′), we 
 Since clock variable 푖 does not appear in 
any guard 휙 of 𝒜, the automaton 𝒜′ generates have that there is also a path in ℛ(𝒜′) 
 푒푙 푒푙+ℎ−1
the same timed language as 𝒜 does. Adding the 〈푠푙, [휈푙]〉 →  →
 푡푖 푒
clock variable 푖 is just for the purpose of 〈푠푙+ℎ, [휈푙+ℎ]〉 → 
 푒푙+ℎ
counting time between two (consecutive) 〈푠푙+ℎ, [휈푙+ℎ + 휏푙+ℎ]〉 → 〈푠푙+ℎ+1, [휈푙+ℎ+1]〉
transitions in Σ푖. A clock valuation for 𝒜′ now in which 휈푙+ℎ( 푖) + 휏푙+ℎ < 훿( ) where 
is of the form 휈 ∪ { 푖 ↦ 푣} for some 푣 ∈ is the label of 푒푙, and 푒푙+ℎ has label in Σ푖. A 
푅푒 푙푠. Now we construct the region graph path in ℛ(𝒜′) satisfying this condition is called 
ℛ(𝒜′) for 𝒜′, and analyze this graph to see if “violation” path. Now, checking for the 
the second condition of Definition 2 is violated 
14 V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15 
violation of the second condition of Definition nonreachable states. Search in ℛ(𝒜′) for a 
2 from 𝒜 is done by searching in the graph of single violation path. If such a path is found 
ℛ(𝒜′) for a single path (not containing a loop) for some i, stop with the output “no”. 
from 푒푙 to 푒푙+ℎ with the violation property as 5. Stop with the output “yes”. 
mentioned above (we call it violation path). If Note that a concurrent real-time system can 
no such a path found, then the timed language be modeled as a timed automata network which 
ℒ(𝒜) satisfies the condition. This can be done is a synchronized product of a number of timed 
in 풪(|ℛ(𝒜′)|2) time. Therefore, we have: automata, where the concurrency can be 
 Theorem 3 The problem “if a given timed expressed explicitly. A synchronized product of 
automaton 𝒜 conforms to a real-time a number of timed automata is also a timed 
concurrent interaction protocol ” is decidable automaton, and hence, our algorithm works also 
in time 풪(|ℛ(𝒜′)|2). on timed automata networks. 
 We sumarizes our results in the following 
deciding procedure: 
Algorithm (Deciding if a timed automaton 4. Conclusion 
satisfies a real-time interaction protocol) 
Input:A real-time protocol = We have proposed a simple but powerful 
 technique to specify interaction protocols for 
〈(Σ1, 푅1),  , (Σ , 푅 ), 훿〉, 
 ≥ the interface of components. Our model can 
where 훿: ⋃푖=1 Σ푖 → ℕ , and 푅푖 is a regular 
expression on Σ for 𝑖 = 1,  , . specify many aspects for interaction: the 
 푖 temporal order between services, concurrency 
A timed automaton 𝒜 = 〈퐿, 푠 , Σ, , , ℱ〉 that 
 for services, and timing constraints. We also 
satisfies Σ ⊆ Σ for all 𝑖 ≤ . 
 푖 have shown that the problem of checking if a 
Output: “Yes” if ℒ(𝒜) ⊧ , “no” otherwise. timed automaton conforms to a given real-time 
Methods: protocol is decidable, and developed a decision 
 1. Construct the region automaton of 𝒜, procedure for solving the problem. The 
 namely the automaton ℛ(𝒜). complexity of the procedure is proportional to 
 2. For each 𝑖 = 1,  , construct automata the size of the region graph of the input timed 
 ℬ푖 that recognizes regular language 푅̅푖. automaton which is acceptable for many cases 
 Then, construct the synchronized product (like the way that the tool UPAAL handles 
 systems). We will incorporate this technique to 
 ℛ(𝒜) ×Σ𝑖 ℬ푖 and check if ℒ(ℛ(𝒜) ×Σ𝑖 ℬ푖) 
 our model for real-time component-based 
 is empty. If ℒ(ℛ(𝒜) ×Σ𝑖 푖) is not empty 
 for some 𝑖, stop with output “no”. systems in our future work. We believe that our 
 3. If there is no time constraint in , i.e. 훿 is results can be extended to the cases in which 
 systems are modeled by timed automata with 
 0 mapping on Σ, stop with output “yes”. 
 parameters, i.e. timed automata where a 
 4. For each , where is not a -
 𝑖 = 1,  , 훿 0 parameter can appear in guards and can be reset 
 mapping on Σ푖, construct the timed by a transition. 
 automaton 
 𝒜′ = 〈L, sI, Σ, X ∪ {ci}, E′, ℱ〉, where E′ =
 {e′ = (s, a, ϕ, C ∪ {ci}, s′) | e = Acknowledgments 
 (s, a, ϕ, C, s′) ∈ E ∧ a ∈ Σi} ∪ {e′ =
 (s, a, ϕ, C, s′) | e = (s, a, ϕ, C, s′) ∈ E ∧ This research was funded by Vietnam 
 a ∈ Σi}, and then construct the region graph National Foundation for Science and 
 ℛ(𝒜′). Add all “time” transitions to ℛ(𝒜′) Technology Development (NAFOSTED) under 
 and simplify it by removing all grant number 102.03-2014.23. 
 V.H. Dang et al. / VNU Journal of Science: Comp. Science & Com. Eng., Vol. 33, No. 1 (2017) 8-15 15 
References He on the Occasion of His 70th Birthday, 
 pages 136-150, 2013. 
 [1] R. Alur and D.L. Dill. A Theory of Timed [5] Hung Ledang and Dang Van Hung. Timing 
 Automata. Theoretical Computer Science, and concurrency specification in component-
 pages 183-235, 1994. based real-time embedded systems 
 [2] Luca de Alfaro and Thomas A. Henzinger. development. In TASE, pages 293-304. 
 Interface Automata. In ACM Symposium on IEEE Computer Society, 2007. 
 Foundation of Software Engineering (FSE), 2001. [6] Stavros Tripakis, Ben Lickly, Thomas A. 
 [3] Jifeng He, Zhiming Liu, and Xiaoshan Li. Henzinger, and Edward A. Lee. On relational 
 rCOS: A refinement calculus of object systems. interfaces. In EMSOFT’09, pages 67-76. 
 Theor. Comput. Sci., 365(1-2):109-142, 2006. ACM, 2009. 
 UNU-IIST TR 322. [7] Dang Van Hung. Toward a formal model for 
 [4] Dang Van Hung and Hoang Truong. Modeling component interfaces for real-time systems. In 
 and specification of real-time interfaces with Proceedings of the 10th international workshop 
 UTP. In Theories of Programming and on Formal methods for industrial critical 
 Formal Methods - Essays Dedicated to Jifeng systems, FMICS ’05, pages 106-114, New York, 
 NY, USA, 2005. ACM.