TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

1

The Opacity of Real-time Automata
Lingtai Wang, Naijun Zhan, and Jie An

Abstract—Opacity is an important property on information
flow to guarantee that a system under attack keeps its “secrets”,
possibly subsets of traces (language-based opacity) or subsets ofstates (state-based opacity), opaque to the outside intruder withpartial observability. In this paper, we investigate the opacity
problems of real-time automata (RTA), which is a popular model
for real-time systems. In order to prove that the languageopacity problem of RTA is decidable, we introduce the notionof trace-equivalence and then translate RTA into finite-state
automata (FA) with timed alphabets. Besides, we also introduce
the notions of partitioned timed alphabet and language toguarantee trace equivalence is preserved by complementationand product operations over FA with timed alphabets. Thus, ourdecision procedure can be sketched as follows: first, translate the
RTA to model a system under attack and the RTA to specify
the secret behaviour of the system into FA, respectively; then,compute another FA, which accepts all traces accepted by the
first FA, but not by the second one; afterwards, project these FA
onto the given observable set; finally, unify the alphabets of theseFA such that for any two timed actions with the same event, theirtime parts do not have any overlap. Thus, whether the original
system is language-opaque with respect to the secret RTA andthe observable set is reduced to the inclusion problem of regular
languages. Similarly, we can show decidability of initial-opacityof RTA.
Index Terms—Real-time automata, language-opacity, initialstate opacity, decidability, trace-equivalence

I. I NTRODUCTIONA

S network communications and online services are ubiquitous in modern life, security and privacy have become
more and more important. Opacity is an information flow
property aiming at keeping the “secret” of a system opaque
to its outsider (called the intruder, who is believed to know
everything about the structure of the system, but only has
partial observability over it). Once the intruder has observed
the execution, he can get an estimation whether the execution
belongs to the secret. There are two types of secrets: subsets
of traces and subsets of states. Opacity properties are divided
into language-based opacity and state-based opacity, according
to in which type the secrets are.
A system is called language-opaque if an intruder withpartial observability can never determine whether a trace ofthe system is secret no matter what he has observed, while a
L. Wang and N. Zhan (the corresponding author) are with the State Key
Lab. of Comp. Sci., Institute of Software, Chinese Academy of Sciences, andUniv. of Chinese Academy of Sciences, email: {wanglt, znj}@ios.ac.cn
J. An is with School of Software Engineering, Tongji University, email:1510796@tongji.edu.cn.
This article was presented in the International Conference on Embedded
Software 2018 and appears as part of the ESWEEK-TCAD special issue.
This work is funded partly by NSFC under grant No. 61625206, 61732001
and 61472279, by “973 Program” under grant No. 2014CB340701, and by the
CAS/SAFEA International Partnership Program for Creative Research Teams.

system is called initial-state opaque if the intruder is unable
to determine whether it starts from a secret state.
The notion of opacity was firstly introduced in the context
of security protocols in [1]. Opacity has then been modelledin Petri nets (PNs), for example, in [2] it is proved that the
problems of initial-opacity, final-opacity and always-opacity
are all decidable if the set of all markings reachable fromany initial markings is finite. In [3], an approach based on
basis reachability graph (BRG) was proposed so that initialstate opacity of bounded PNs can be verified. In [4], theauthors generalised opacity to labelled transition systems andproved that opacity is undecidable in such systems. To thisend, they further proposed a decidable approximation to theoriginal opacity, which was named as under/over-opacity. In
the framework of automata, verification of initial-opacity is
PSPACE-complete [5]. State estimators are constructed in [5]–[8] for verification of different kinds of state-based opacity.
Probabilistic models are also taken into consideration, such as[9]–[12].
In [13], the notion of opacity was first extended to time
settings, with the result that the language-based opacity problem is already undecidable for a very restrictive class of event
recording timed automata (ERA).
As time is an important attack vector against secure systems,
we still would like to consider the language-based and initialstate based opacity problems on a timed model. In this paper,
we concentrate on real-time automata (RTA) [14], a subclassof timed automata with a single clock to be reset at eachtransition, which can be regarded as finite automata with time
information for each transition. RTA is a popular model for
real-time systems. Note that RTA is not comparable with ERA
as pointed out in [14].
In this paper, we show that the language-opacity problemof RTA is decidable by reduction to the inclusion problem ofregular languages, which is decidable from automata theory[15]. The basic idea can be sketched as follows: First, we
introduce the notion of trace-equivalence between languagesof RTA and finite-state automata (FA) with timed alphabets.
Second, in order to guarantee trace-equivalence to be preservedby the complementation and product operation over FA withtimed alphabets, we introduce the concepts of partitioned
timed alphabet and partitioned language. So refined FA withpartitioned timed alphabet are constructed. Third, we define a
projection operation on FA onto the given observable set Σo ,by removing all unobservable transitions and merging theirtime durations into the subsequent observable transition.
Given A (the system under attack), As (specifying secretbehaviours) and Σo (the observables), the whole process isshown below, where 0 stands for translation from RTA to FA,
1 for refinement by partition, 2 for complementation, 3 for

0000–0000/00$00.00 c 2018 IEEE

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

production, and 4 for projection.
1&2/ c 3 /
4 /
1&2/
0 /
Bs
Bs
Bns ↑Σo(Bns ↑Σo )c
As
: Bns
1&3

3


/B
/ B ↑Σo/ BfinalA
Among those automata, Bns accepts the language traceequivalent to L(A) \ Lf (As ), and Bfinal accepts the language
trace-equivalent to PΣo ,t (L(A))\PΣo ,t (L(A)\Lf (As )). Thus,
the original A is language-opaque with respect to Lf (As ) andΣo iff Lf (Bfinal ) is empty.
Besides, the decidability of the initial-state opacity of RTA
can be proved by reduction to the inclusion problem of regular
languages similarly.
Related work: The technique used in our work is similar
to Dima’s in [14] to establish Kleene Theorem and Pumping
Lemma for RTA. In [14], the Floyd-Warshall algorithm andpartition are used for transforming an augmented RTA intoa stuttering-free one and then into a deterministic one, fora given RTA, so that the resulted RTA is closed undercomplementation, which can correspond to an FA. In ourwork, we consider the opacity problems of RTA. To thisend, partition is used to eliminate overlap of time domains
so that a trace-equivalence between RTA and FA can bepreserved by their product and complementation operations; inaddition, the Floyd-Warshall algorithm is utilized only once formerging successive unobservable transitions and constructing
the projection of FA. So, the complexity of Dima’s approach ismuch higher than ours, with his approach, the number of statesin the stuttering-free one is n = 2|Σ| · |S|, and the number ofstates in the deterministic one is at most 3n .
Organization: The remainder of this paper is organized as follows. In Section II, we recall preliminaries including FA, regular expressions, RTA, and the problems oflanguage/initial-opacity of RTA. Translation from RTA to FA
preserving trace-equivalence is introduced in Section III. Section IV provides the method to project an FA obtained in theprevious section onto an observable alphabet. In Section V wecome to the conclusion that the problems of language/initialopacity are decidable for RTA, and provide a very simple
example for illustration. A prototypical implementation ispresented in Section VI, and Section VII concludes this paper.
0

4

1&3

II. P RELIMINARIES
We use R≥0 , Q≥0 , and N to denote the set of nonnegative real numbers, nonnegative rational numbers, and natural
numbers respectively.
Let Σ, a set of events, be the alphabet. A word or string
over Σ is a finite sequence w = σ1 σ2 . . . σn , where σi ∈ Σ
for i = 1, 2, . . . , n. |w| = n is the length of w. ε is the empty
word, with |ε| = 0. Σ∗ is the set of all the finite words over
Σ including ε. L is a language over Σ if L ⊆ Σ∗ .
Commonly-used operations on languages include union,intersection, and difference as in set theory, as well as concatenation, Kleene closure and projection defined below:
Concatenation: Let L1 , L2 ⊆ Σ∗ , the concatenation L1 ·L2 = {s1 · s2 | s1 ∈ L1 ∧ s2 ∈ L2 }. The “·” can be omitted if
no confusion.

2

Kleene closure: Let L ⊆ Σ∗ , and L0 = {ε}, Lk S
= (Lk−1 )L∗for k > 0, then the Kleene closure of L is L = k∈N Lk ={ε} ∪ L ∪ LL ∪ · · · .
Projection: Given Σ and a subset Σo ⊆ Σ, we can define a
projection Po : Σ∗ → Σ∗o , where
Po (ε) = ε(
Po (σs) =σPo (s), if σ ∈ Σo
, for σ ∈ Σ and s ∈ Σ∗ .
Po (s),
otherwise

Given any B ⊆ Σ∗ and C ⊆ Σ∗o , the image of B under Po is
Po (B) = {Po (s) | s ∈ B} ⊆ Σ∗o and the inverse image of C
under Po is Po−1 (C) = {s ∈ Σ∗ | Po (s) ∈ C} ⊆ Σ∗ .
Consider the alphabet Σ × R≥0 . A timed word over Σ isa finite word over the alphabet Σ × R≥0 with the form of
wt = (σ1 , t1 )(σ2 , t2 ) . . . (σn , tn ), where 0 ≤ t1 ≤ t2 ≤ · · · ≤tn , meaning that σi occurs at ti successively for 1 ≤ i ≤ n.
TW∗ (Σ) denotes the set of all timed words over Σ. A subset
of TW∗ (Σ) is a timed language. If Σo ⊆ Σ is the observable alphabet, PΣo ,t denotes the projection from TW∗ (Σ)
into TW∗ (Σo ). For example, if wt = (a, 2)(b, 3)(a, 5)(b, 8),
P{b},t (wt ) = (b, 3)(b, 8) and P{a},t (wt ) = (a, 2)(a, 5).
A. Finite-state automata and regular expressions
Automata is a kind of well-known and commonly used model to study discrete transition systems and their behaviours.
Finite-state automata (FA) are automata with finite states,
including deterministic and non-deterministic ones.
Definition 1: • A deterministic finite-state automaton(DFA) is a 5-tuple Ad = (S, Σ, δ, s0 , F ), where– S is a finite set of states;– Σ is a finite alphabet;– δ : S × Σ → S is the transition relation, a partial
function on S × Σ;
– s0 ∈ S is the initial state; and– F ⊆ S is the set of accepting states.
• A non-deterministic finite-state automaton (NFA) is a 5tuple An = (S, Σ ∪ {ε}, δ, Init, F ), where– S is a finite set of states;– Σ is a finite alphabet;– δ : S × (Σ ∪ {ε}) → 2S is the transition function;– Init ⊆ S is the set of initial states; and– F ⊆ S is the set of accepting states.
Obviously, a DFA can be viewed as a special kind of NFA,
where there is only one initial state, one or zero state in eachδ(s, σ), and no ε-transition.
For an NFA A, (s1 , σ, s2 ) is called a σ-transition if s2 ∈δ(s1 , σ). Preσ and Postσ denotes the set of states from which
and to which are σ-transitions respectively.
A run of A is either a single state s0 where s0 ∈ Init, or aσ1σ2σnsequence s0 −→s1 −→· · · −−→
sn where n > 0, s0 ∈ Init,σi ∈ Σ ∪ {ε} and si ∈ δ(si−1 , σi−1 ) for 1 ≤ i ≤ n. An
accepting run is a run ending in a state sn ∈ F .
The trace of a run ρ is a finite word over Σ, written as
trace(ρ). trace(s0 ) is ε, and the trace of the sequence froms0 to sn is a finite word obtained by projecting σ1 σ2 . . . σnonto Σ, that is, the string a1 a2 . . . am obtained by removing

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

each ε from σ1 σ2 . . . σn ; hence the length of the trace is m,less than or equal to n.
Let Tr(s0 ) be the set of traces of runs from s0 , and Tr(S0 )be the set of traces of runs from any state s0 ∈ S0 .
The language generated by A, denoted by L(A), is the setof traces of runs of A, i.e., L(A) = Tr(Init); the language
accepted by A, denoted by Lf (A), is the set of traces of
accepting runs. A language is said to be regular if it can be
accepted by a finite-state automaton.
Regular expressions is another way to define regular languages.
Definition 2: Regular expressions over alphabet Σ can be
defined recursively as follows:
1. (Base Clause.) ∅, ε, σ ∈ Σ are regular expressions, where∅ denotes the empty set, ε denotes the set {ε}, and σdenotes the set {σ} for σ ∈ Σ.
2. (Inductive Clause.) If r, r1 , r2 are regular expressions, so
are r1 · r2 , r1 + r2 , r∗ . r1 · r2 denotes the concatenation of
the languages defined by r1 and r2 , r1 + r2 denotes theunion of the two languages, and r∗ denotes the Kleene
closure of the language defined by r.
3. (External Clause.) Regular expressions can only be constructed by applying 1 and 2.
Theorem 2.1 (Kleene’s Theorem): Any regular language is
accepted by an FA; any language accepted by an FA is regular.
1) Complementation and product over DFA: Two automata are called language-equivalent, or equivalent for short,
if they generate and accept the same languages. An NFA
An = (S, Σ, δ, Init, F ) can be transformed into an equivalent
DFA Ad = (S 0 , Σ, δ 0 , Init0 , F 0 ) defined below. Let εR(s, ε)denote the set of states which are reachable from state s via
no transitions or only ε-transitions, and εR(s, σ) the set ofstates which are reachable from state s via one σ-transition
together with ε-transitions
S before and after it. Then in Ad ,S 0 = 2S ; δ 0 (S1 , σ) = s1 ∈S1 εR(s1 , σ); Init0 = εR(s0 , ε);F 0 = {S1 | S1 ∩ F 6= ∅}.
Consider a DFA A = (S, Σ, δ, s0 , F ). The complement
automaton Acomp which accepts Lf (A)c = Σ∗ \ Lf (A) can
be constructed as follows:
1. Augment S with a new state snew ∈/ S;
2. Augment δ such that it becomes a total function, denotedas δ comp . For all (s, σ) ∈ S × Σ, if δ(s, σ) is defined,let δ comp (s, σ) = δ(s, a); if δ(s, σ) is not defined, let
δ comp (s, σ) = snew . Also δ(snew , σ) = snew for each σ ∈Σ. After that Σ∗ becomes the language generated, while
the language accepted keeps unchanged;
3. Let (S \ F ) ∪ {snew } be the set of accepting states.
comp

comp

To sum up, A= (S ∪ {snew }, Σ, δ
, s0 , S \ F ∪ {snew }).
Given two DFA A1 = (S1 , Σ1 , δ1 , s0,1 , F1 ) and A2 = (S2 ,Σ2 , δ2 , s0,2 , F2 ) with S1 ∩ S2 = ∅, the product of A1 and A2
is Ap = A1 × A2 = (S p , Σp , δ p , sp0 , F p ), defined as follows:
S p = S1 × S2 ; Σp = Σ1 ∩ Σ2 ; δ p ((s1 , s2 ), σ) = (s01 , s02 ) if
δ(s1 , σ) = s01 and δ(s2 , σ) = s02 , and is not defined otherwise;
sp0 = (s0,1 , s0,2 ); F p = F1 × F2 .
Lf (A1 × A2 ) = Lf (A1 ) ∩ Lf (A2 ).

3

B. Real-time automata (RTA)
RTA are very similar to classical automata despite theirtaking time into account as well. We can easily get an RTA
by attaching time information to each transition of a given
automaton.
Definition 3: An RTA is a 6-tuple A = (S, Σ, ∆, Init, F,µ), where- S is a finite set of states;- Σ is a finite alphabet;- ∆ ⊆ S × Σ × S is the transition relation;- Init ⊆ S is the set of initial states;- F ⊆ S is the set of accepting states; and- µ : ∆ → 2R≥0 \ {∅} is the time labelling function.
Transitions (s1 , σ, s2 ) ∈ ∆ are called σ-transitions. Preσand Postσ denotes the set of states from which and to whichare σ-transitions respectively.
A run of A is either a single initial state s0 ∈ Init or aσ2σ1σnsn where n > 0,
· · · −−→
s1 −→finite sequence ρ = s0 −→
λ2

λ1

λn

s0 ∈ Init, (si−1 , σi , si ) ∈ ∆, and λi ∈ µ(si−1 , σi , si ) for1 ≤ i ≤ n.
The trace of a run ρ, denoted by trace(ρ), is a timed word
defined as follows: trace(s0 ) = εt where subscript “t” is usedσ1σ2σnto emphasize the time factor; if ρ = s0 −→s1 −→. . . −−→
sn ,
λ1
λ2
λn
Pi
trace(ρ) = (σ1 , t1 )(σ2 , t2 ) . . . (σn , tn ) where ti =j=1 λjfor 1 ≤ i ≤ n.
Let Tr(s0 ) be the set of traces of runs from s0 , andTr(S0 ) be the set of traces of runs from any state s0 ∈ S0 .
Then languages generated
and accepted by A can be defined:S
L(A) = Tr(Init) = s0 ∈Init Tr(s0 ), and Lf (A) = {trace(ρ) |ρ starts from s0 ∈ S0 and ends in sf ∈ F }.
Example 1: Consider the two RTA in Figure 1. In A1 ,Tr(s0 ) = {εt } ∪ {(a, ta ) | ta ∈ [1, 2]} ∪ {(a, ta )(b, tb ) |ta ∈ [1, 2], tb − ta ∈ [2, 3]}, and Tr(s3 ) = {εt } ∪ {(b, tb ) |tb ∈ [3, 4]}. A1 generates L(A1 ) = Tr(s0 ) ∪ Tr(s3 ); and A1
accepts Lf (A1 ) = {(a, ta ) · (b, tb ) | ta ∈ [1, 2], tb − ta ∈[2, 3]} ∪ {(b, tb ) | tb ∈ [3,S4]}.
In A2 , let a∗ = {ε} ∪ k≥1 {(a, t1 ) . . . (a, tk ) | ti − ti−1 ∈[1, 2]} (t0 = 0), and a∗ b = a∗ · (b, tb ) where tb ∈ [3, 5]. Then
Tr(s00 ) = a∗ ∪ a∗ b; L(A2 ) = Tr(s00 ); Lf (A2 ) = a∗ b.
s0

s3

a
s1
[1, 2][2, 3]
b[3, 4]

a [1,2]bs2s0(a) A1bs1[3, 5](b) A2

Fig. 1: RTA A1 and A2

C. Language and initial-state opacity of RTA
Given an RTA A = (S, Σ, ∆, Init, F, µ) and an observablealphabet Σo ⊆ Σ, although L(A) is generated, intruders canonly observe timed words in PΣo ,t (L(A)).

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

Suppose we have a secret timed language, Lsecret , over Σ. In
this case, can intruders make sure that a trace of the systemfalls into the secret set Lsecret according to what they haveobserved? This is considered in the language-opacity problem.
Similarly, suppose we have some secret states, Ssecret ⊆ S.
The problem of initial-state opacity (initial-opacity for short)considers whether intruders can make sure that a trace starts
from Ssecret . Formally,
Definition 4: Given an RTA A = (S, Σ, ∆, Init, F, µ), an
observable alphabet Σo ⊆ Σ, a secret timed language Lsecretover Σ and a secret set of states Ssecret ⊆ S,
• Language-opacity: A is language-opaque with respect
to Lsecret and Σo iff for all wt ∈ L(A) ∩ Lsecret , ∃wt0 ∈L(A) \ Lsecret s.t.
PΣo ,t (wt ) = PΣo ,t (wt0 ),equivalently,PΣo ,t (L(A) ∩ Lsecret ) ⊆ PΣo ,t (L(A) \ Lsecret ), orPΣo ,t (L(A)) ⊆ PΣo ,t (L(A) \ Lsecret ).
•Initial-state opacity: A is initial-state opaque with respect to Ssecret and Σo iff for all s0 ∈ Init ∩ Ssecret and all
wt ∈ Tr(s0 ), ∃s00 ∈ Init \ Ssecret , ∃wt0 ∈ Tr(s00 ) s.t.
PΣo ,t (wt ) = PΣo ,t (wt0 ),equivalently,PΣo ,t (Tr(Init ∩ Ssecret ))) ⊆ PΣo ,t (Tr(Init \ Ssecret )), orPΣo ,t (L(A)) ⊆ PΣo ,t (Tr(Init \ Ssecret )).

The language-opacity problem of RTA: Is an RTA A= (S, Σ, ∆, Init, F, µ) language-opaque with respect tosome given secret timed language Lsecret and Σo ⊆ Σ?
• The initial-state opacity problem of RTA: Is an RTA
A = (S, Σ, ∆, Init, F, µ) initial-state opaque with respect
to some given secret set Ssecret ⊆ S and Σo ⊆ Σ?
Example 2: We still consider the automata A1 shown in
Figure 1(a). Let Σo = {b}, Lsecret = {(a, ta ) · (b, tb ) | 1 ≤ta ≤ 3 ∧ 2 ≤ tb ≤ 5}, and Ssecret = {s3 }.
Firstly, A1 is not language-opaque with respect to Lsecretand Σo . This is because there only exists wt = (a, 2) · (b, 5)in L(A1 ) satisfying PΣo ,t (wt ) = (b, 5) and wt is from Lsecret .
So if PΣo ,t (wt ) = (b, 5), we can easily know that the trace isabwt = (a, 2) · (b, 5) and the run is ρ = s0 −→ s1 −→ s2 . Thus,2
3
the secret is exposed in this case.
From another perspective, L(A1 ) ∩ Lsecret = {(a, ta ) ·(b, tb ) | ta ∈ [1, 2], tb − ta ∈ [2, 3]}, and L(A1 ) \ Lsecret ={εt } ∪ {(a, ta ) | ta ∈ [1, 2]} ∪ {(b, tb ) | tb ∈ [3, 4]}. The
projections are PΣo ,t (L(A1 ) ∩ Lsecret ) = {(b, t) | t ∈ [3, 5]},PΣo ,t (L(A1 ) \ Lsecret ) = {εt } ∪ {(b, t) | t ∈ [3, 4]}, andPΣo ,t (L(A1 )) = {εt } ∪ {(b, t) | t ∈ [3, 5]}. So A1 is notlanguage-opaque with respect to Lsecret and Σo .
Secondly, A1 is initial-opaque with respect to Ssecret andΣo . This is because for any wt = (b, tb ) in Tr(s3 ) with 3 ≤tb ≤ 4, there always exists wt0 = (a, 1) · (b, tb − 1) ∈ Tr(s0 )•4such that PΣo ,t (wt0 ) = PΣo ,t (wt ), whose corresponding run isabρ = s0 −→ s1 −−−→ s2 . Hence the secret is concealed.
1

tb −1

From another perspective, PΣo ,t (Tr(s0 )) = {εt } ∪ {(b, t) |t ∈ [3, 5]}, and PΣo ,t (Tr(s3 )) = {εt } ∪ {(b, t) | t ∈ [3, 4]}.
So A1 is initial-opaque with respect to Ssecret = {s3 } andΣo = {b}.
III. F ROM RTA TO FA
In this section we construct FA from RTA, such that theirlanguages are “equivalent” in some sense, which is called
the trace-equivalence relation in this paper. Also, we put
some restriction on the alphabet of the derived FA, called
the partitioned alphabet, so that product and complementation
operations still work on those FA.
A. Trace-equivalence relation
RTA and FA are similar in their structure, except that
RTA maintain time information as well. Thus it is natural toconsider the transformation of an RTA into its correspondingFA, by attaching time information to the respective event ineach transition, in order to utilize the existing results of FA.
We first introduce the concept of trace-equivalence between
a timed language overS a finite alphabet Σ and a language over
the alphabet Σt = σ∈Σ {σ} × Tσ where each Tσ is a finite
subset of 2R≥0 . Σt is called a timed alphabet. Σt is finite asΣ is finite and Tσ is finite for each σ ∈ Σ.
Given a fixed word w = (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . · (σn , Λn ),where Λi ⊆ R≥0 and Λi 6= ∅, we write [w] to denote the setof all the timed words of the form wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . ·(σn , tn ) with t1 ∈ Λ1 and (ti − ti−1 ) ∈ Λi for 1 < i ≤ n.
Definition 5: Given LS1 , a timed language over Σ, and L2 ,a language over Σt = σ∈Σ {σ} × Tσ , where each Tσ is a
finite subset of 2R≥0 , L2 is said to be trace-equivalent to L1 ,denoted by L2 ≈tr L1 , if
• εt ∈ L1 iff ε ∈ L2 ;• if any timed word wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . · (σn , tn ) ∈L1 , then there exists some w = (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . ·(σn , Λn ) ∈ L2 such that wt ∈ [w];
• if w = (σ1 , Λ1 ) · (a2 , Λ2 ) · . . . · (an , Λn ) ∈ L2 , then all
timed words wt ∈ [w] are in L1 , i.e., [w] ⊆ L1 .
B. A first trial: directly derived FA
Given an RTA A = (S, Σ, ∆, Init, F, µ), an FA B = (S 0 , Σt ,δ, Init0 , F 0 ) can be directly built which has the same setsof states, initial states and accepting states as A, that is,S 0 = S, Init0 = Init, and F 0 = F . The difference is thattime information of each transition describedSby µ in A istransferred into its label in B. Formally, Σt = σ∈Σ {σ} × Tσ ,where Tσ = {µ(s, σ, s0 ) | ∃(s, σ, s0 ) ∈ ∆}, and δ(s, (σ, Λ)) ={s0 | ∃(s, σ, s0 ) ∈ ∆∧µ(s, σ, s0 ) = Λ}. B constructed as above
is called the directly derived FA from A. B0 is constructed
same as B except that its accepting states is set to be S. Thismeans that B0 accepts L(B).
Lemma 3.1: L(B) ≈tr L(A), and Lf (B) ≈tr Lf (A).
Proof: If εt ∈ L(A), a possible run is s0 ∈ Init. Thus,
s0 ∈ Init0 . It means that B has a run s0 whose trace is ε,TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

i.e., ε ∈ L(B). On the other hand, suppose ε ∈ L(B), which
implies there exists an initial state s0 ∈ Init0 . It follows thats0 ∈ Init. Hence, εt ∈ L(A).
If wt = (σ1 , t1 )·(σ2 , t2 )·. . .·(σn , tn ) ∈ L(A), there exists aσnσ2
σ1−→ sn , such that
→ · · · −−−−
s1 −−−
run of A, say ρ = s0 −→t1

tn −tn−1t2 −t1s0 ∈ Init, (si−1 , σi , si ) ∈ ∆ and ti − ti−1 ∈ µ(si−1 , σi , si )for 1 ≤ i ≤ n. So there exists a run of B from s0 ∈ Init0 ,(σ1 ,Λ1 )(σ2 ,Λ2 )(σn ,Λn )that is, ρ0 = s0 −−−−−→ s1 −−−−−→ · · · −−−−−→ sn , whereΛi = µ(si−1 , σi , si ) for 1 ≤ i ≤ n. Thus, there exists a tracew = (σ1 , Λ1 )·(σ2 , Λ2 )·. . .·(σn , Λn ) ∈ L(B) such that t1 ∈ Λ1
and (ti − ti−1 ) ∈ Λi for 1 < i ≤ n, in other words, wt ∈ [w].
Given a word w = (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . · (σn , Λn ) ∈(σ1 ,Λ1 )(σ2 ,Λ2 )L(B), there must be a run of the form s0 −−−−−→ s1 −−−−−→(σn ,Λn )· · · −−−−−→ sn , where s0 ∈ Init0 . Hence (si−1 , σi , si ) ∈ ∆and µ(si−1 , σi , si ) = Λi for 1 ≤ i ≤ n. It follows that forany t1 , t2 , ..., tn such that t1 ∈ Λ1 and (ti − ti−1 ) ∈ Λi for
σn
σ2
σ1
−→
s1 −−−→ · · · −−−−
1 < i ≤ n, there exists a run s0 −→t1

t2 −t1tn −tn−1

sn ; therefore wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . · (σn , tn ) ∈ L(A).
Hence, [w] ⊆ L(A).
The proof for Lf (B) ≈tr Lf (A) is similar, except that theconsidered run should end in an accepting state.
However, such trace-equivalence relationship may not bepreserved by intersection and complementation operations. For
instance, let Σ = {a} and Σt = {(a, [2, 4]), (a, [3, 5])},and L11 = {(a, t) | t ∈ [3, 5]}, L12 = {(a, t) | t ∈[2, 4]}, L21 = {(a, [3, 5])} and L22 = {(a, [2, 4])}. Clearly,
L21 ≈tr L11 and L22 ≈tr L12 , but it can easily followthat L21 ∩ L22 is not trace-equivalent to L11 ∩ L12 , since
L11 ∩ L12 = {(a, t) | t ∈ [3, 4]}, while L21 ∩ L22 = ∅.
This is because (a, [2, 4]) and (a, [3, 5]) are different eventsin the timed alphabet Σt , but the actual timed words they
represent overlap. As for the complementation operation, weonly choose and compare subsets of words/timed words withlength 1. Timed words in TW∗ (Σ) \ L11 with length 1 is{(a, t) | t ∈ [0, 3) ∪ (5, +∞)}, while words in Σ∗t \ L21 withlength 1 is {(a, [2, 4])}. This is because the union of [3, 5]
and [2, 4] does not cover R≥0 and the intersection of [3, 5]
and [2, 4] is not empty.
C. Partitioned timed alphabet and partitioned language
As a consequence, restrictions should be placed on the timedalphabet.
S Suppose the timed alphabet under consideration isΣt = σ∈Σ {σ} × Tσ . There are two main restrictions on eachTσ :• any two different elements of Tσ should be disjoint;• the union of all elements of Tσ should be equal to R≥0 .
Hence the concept of partition in mathematics can be exploited
here. A partition of a nonempty set B is a set of B’s non-empty
subsets satisfying each element x ∈ B is in one and only oneof those subsets. Tσ satisfies the two restrictions above if it isa partition of R≥0 . We introduce the definition of partitioned
alphabet and partitioned language below.
S
Definition 6: A finite timed alphabet Σt = σ∈Σ {σ} × Tσ
is called partitioned if for any σ ∈ Σ, Tσ is a partition of
R≥0 .

5

A language L over a timed alphabet Σt is called partitioned
if Σt is a partitioned alphabet.
Partitioned languages can guarantee that the relation of
trace-equivalence is preserved by language complementationand intersection.
Lemma 3.2: If L1 is a timed language
over Σ, L2 isS
a partitioned language over Σt = σ∈Σ {σ} × Tσ withL2 ≈tr L1 , then we have (Σ∗t \ L2 ) ≈tr (TW∗ (Σ) \ L1 ).
Proof: Firstly, εt ∈ TW∗ (Σ) \ L1 ⇔ εt ∈/ L1 ⇔ ε ∈/ L2⇔ ε ∈ Σ∗t \ L2 .
Secondly, suppose wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . · (σn , tn ) ∈TW∗ (Σ)\L1 , then there must be a unique Λi ∈ Tσi containingti − ti−1 for each σi (t0 is deemed to be 0 here), as Tσi isa partition of R≥0 . Thus, it follows (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . ·(σn , Λn ) ∈ Σ∗t . We can easily know (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . ·(σn , Λn ) is not in L2 , otherwise wt would be in L1 , which
is a contradiction. So (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . · (σn , Λn ) is inΣ∗t \ L2 .
On the other hand, suppose w = (σ1 , Λ1 ) · (σ2 , Λ2 ) · . . . ·(σn , Λn ) ∈ Σ∗t \ L2 . Let wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . · (σn , tn )be any timed word with t1 ∈ Λ1 and ti − ti−1 ∈ Λi for
i = 2, . . . , n. It holds that wt ∈/ L1 , otherwise there would
exist some w0 = (σ1 , Λ01 ) · (σ2 , Λ02 ) · . . . · (σn , Λ0n ) ∈ L2 suchthat t1 ∈ Λ01 and ti −ti−1 ∈ Λ0i for 1 < i ≤ n since L2 ≈tr L1 .
The fact that Λi and Λ0i are both in a partition Tσi of R≥0and Λi ∩ Λ0i 6= ∅ indicates that Λi = Λ0i and therefore w = w0 ,which results in a contradiction. Hence wt ∈ TW∗ (Σ) \ L1 .
To sum up, (Σ∗t \ L2 ) ≈tr (TW∗ (Σ) \ L1 ) by Def. 5.
Lemma 3.3: If L11 and L12 are timed languages over Σ,
L21 and L22 areover the same timed

S partitioned languages
alphabet Σt = σ∈Σ {σ}×Tσ , and L21 ≈tr L11 and L22 ≈tr
L12 , then it follows that (L21 ∩ L22 ) ≈tr (L11 ∩ L12 ).
Proof: Firstly, εt ∈ L11 ∩ L12 ⇔ εt ∈ L11 ∧ εt ∈ L12 ⇔ε ∈ L21 ∧ ε ∈ L22 ⇔ ε ∈ L21 ∩ L22 by Def. 5.
Secondly, if wt = (σ1 , t1 ) · (σ2 , t2 ) · . . . · (σn , tn ) ∈ L11 ∩L12 , then wt ∈ L11 ∧ wt ∈ L12 . As wt ∈ L11 , there exists
a w1 = (σ1 , Λ11 ) · (σ2 , Λ12 ) · . . . · (σn , Λ1n ) ∈ L21 such thatti −ti−1 ∈ Λ1i for each i (here t0 = 0). Similarly, as wt ∈ L12 ,there exists a w2 = (σ1 , Λ21 ) · (σ2 , Λ22 ) · . . . · (σn , Λ2n ) ∈ L22
such that ti − ti−1 ∈ Λ2i for each i (also t0 = 0). Since
L21 and L22 are over a common alphabet Σt , Λ1i and Λ2i areboth in Tσi , a partition of R≥0 . Λ1i ∩ Λ2i 6= ∅ means that
Λ1i = Λ2i , for i = 1, . . . , n. Therefore w1 = w2 . So there
exists a w = w1 = w2 such that w ∈ L21 ∧ w ∈ L22 , i.e.,w ∈ L21 ∩ L22 .
On the other hand, if w = (a1 , Λ1 )(a2 , Λ2 ) . . . (an , Λn ) ∈L21 ∩ L22 , obviously w ∈ L21 and w ∈ L22 . This implies that[w] ⊆ L11 and [w] ⊆ L12 , and therefore [w] ⊆ L11 ∩ L12 .
To sum up, (L21 ∩ L22 ) ≈tr (L11 ∩ L12 ) by Def. 5.
According to the above lemmas, if timed languages overan alphabet Σ are represented by FA accepting their traceequivalent languages over a partitioned timed alphabet Σt ,then the trace-equivalence relationship can be preserved undercomplementation and intersection over these FA.
D. Refined FA over partitioned timed alphabets

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

In this section we construct another FA B 0 with a partitioned
timed alphabet Σ0t , such that Lf (B 0 ) is also trace-equivalent
to Lf (A).
The key point is to obtain the partitioned timed alphabet
Σ0t . Each transition of B, say (s1 , (σ, Λ), s2 ), should be split
into finite transitions in B 0 , with the same pre- and post-states:(s1 , (σ,SkΛ1 ), s2 ), (s1 , (σ, Λ2 ), s2 ), . . . , (s1 , (σ, Λk ), s2 ), suchthat j=1 Λj = Λ and Λi ∩ Λj = ∅ for any i 6= j.
The finite set Tσ of B contains time labels of all σtransitions for each σ. Then Tσ0 meeting the above requirements can be computed from Tσ . The alphabet of B 0 is thus
constructed as Σ0t = {σ} × Tσ0 .
An auxiliary function P is recursively defined here tocompute a finite partition given a finite set C ⊆ 2R≥0 .
• P(C) = {R≥0 } if |C| = 0, i.e., C = ∅.
• P(C ∪ Λ) = ({Λ1 ∩ Λ, . . . , Λm ∩ Λ} ∪ {Λ1 \ Λ, . . . , Λm \Λ}) \ {∅}, if P(C) = {Λ1 , . . . , Λm } and Λ ∈/ C.
|C|Additionally, |P(C)| is no more than 2 .
By the definition of P, each nonempty Λ ∈ C is partitioned
into several subsets which are mutually disjoint, and the setof these subsets is denoted as PC,Λ , or PΛ if there is noambiguity. For instance, given C = {[2, 5], [3, 6]}, we canconstruct P(C) = {[3, 5], [2, 3), (5, 6], [0, 2) ∪ (6, +∞)},
satisfying [2, 5] = [2, 3) ] [3, 5], and [3, 6] = [3, 5] ] (5, 6].
NowSgiven an FA B = (S, Σt , δ, Init, F ) whose alphabet
Σt = σ∈Σ {σ} × Tσ is finite, we can obtain another FA
B 0 = (S 0 , Σ0t , δ 0 , Init0 , F 0 ) such that Σ0t is partitioned. We
fix the set Tσ+ , a finite superset of Tσ in advance, and let
Tσ0 = P(Tσ+ ) for each σ. The selection strategy of Tσ+ is
discussed at the end of this section.
Definition 7: Given B and {Tσ0 }σ∈Σ as above, the refinedFA, also called the refinement of B, B 0 = (S 0 , Σ0t , δ 0 , Init0 , F 0 )is as follows:00- S 0 = S,
S Init = Init, 0F = F ;0- Σt = σ∈Σ {σ} × Tσ ;- S
δ 0 (s1 , (σ, Λ0 )) = {s2 | s2 ∈ δ(s1 , (σ, Λ)) ∧ Λ0 ⊆ Λ} ={δ(s1 , (σ, Λ)) | Λ0 ⊆ Λ}.
Lemma 3.4: Let B 0 be a refinement of B, then L(B 0 ) is
trace-equivalent to a timed language Lt if L(B) is traceequivalent to Lt . And Lf (B 0 ) is trace-equivalent to a timed
language Lt,f if Lf (B) is trace-equivalent to Lt,f .
Proof: If εt ∈ Lt (resp. Lt,f ), ε ∈ L(B) (resp. Lf (B)). A
possible run is s0 , where s0 ∈ Init (resp. Init∩F ). So s0 ∈ Init0(resp. Init0 ∩ F 0 ) and ε ∈ L(B 0 ) (resp. Lf (B)). On the other
hand, suppose ε ∈ L(B) (resp. Lf (B)), which implies there
exists s0 ∈ Init0 (resp. Init0 ∩ F 0 ). It follows that s0 ∈ Init
(resp. Init ∩ F ); therefore ε ∈ L(B) (resp. Lf (B)) and εt ∈ Lt
(resp. Lt,f ).
Suppose wt = (σ1 , t1 ) · . . . · (σn , tn ) ∈ Lt (resp. Lt,f )where n ≥ 1, so there exists a word w = (σ1 , Λ1 ) · (σ2 , Λ2 ) ·. . . · (σn , Λn ) ∈ L(B) (resp. Lf (B)) such that t1 ∈ Λ1 and(ti − ti−1 ) ∈ Λi for 1 < i ≤ n. Thus, there exists somew0 = (σ1 , Λ01 ) · (σ2 , Λ02 ) · . . . · (σn , Λ0n ) ∈ L(B 0 ) (resp. Lf (B 0 ))such that t1 ∈ Λ01 and (ti −ti−1 ) ∈ Λ0i for 1 < i ≤ n according
to the construction above.
Given a word w0 = (σ1 , Λ01 )·(σ2 , Λ02 )·. . .·(σn , Λ0n ) ∈ L(B 0 )(resp. Lf (B 0 )), there exists a word w = (σ1 , Λ1 ) · (σ2 , Λ2 ) ·6. . . · (σn , Λn ) ∈ L(B) (resp. Lf (B)) such that Λ0 ⊆ Λ for1 ≤ i ≤ n. So any word in [w] is also in Lt (resp. Lt,f ).
Since [w0 ] ⊆ [w], all words in [w0 ] is in Lt (resp. Lt,f ).
Now let’s come back to the selection strategy of Tσ+ foreach σ. Suppose the FA under consideration are B, B1 and B2
which have n, n1 , n2 states respectively. Let Tσ (resp. Tσ,1and Tσ,2 ) be the duration parts of σ-transitions in B (resp.
in B1 and B2 ), and kσ , kσ,1 and kσ,2 be their cardinalities,
respectively.
If we need to get the “complement” of Lf (B), we shouldchoose Tσ+ = Tσ , as Tσ0 = P(Tσ ) is sufficient for
P each σ.
Accordingly, the refined FAPB 0 has n states, at most σ∈Σ 2kσtimed events and at most σ∈Σ kσ 2kσ transitions.
If we need to get the “intersection” , “union”, or “minus”
of Lf (B1 ) and Lf (B2 ), we should choose Tσ+ = Tσ,1 ∪ Tσ,2for all of them.PThus Tσ0 = P(Tσ,1 ∪ Tσ,2 ). Bi has ni
kσ,1 +kσ,2states,at most) timed events and at mostσ∈Σ (2
P
kσ,1 +kσ,2) transitions for i = 1, 2.
σ∈Σ kσ,i (2Note that the idea of partition is similar to the proofof Theorem 4.4 in [14]. But our calculation of partitionof nonnegative reals is more flexible by choosing different
parameters for P for different operations, that can reduce thenumber of states and/or transitions essentially.
By translating RTA into FA, further into refined FA, we canget a better understanding of their timed languages. Moreover,
the trace-equivalence relationship allows to compute complementation and intersection of such languages.
IV. P ROJECTION
In this section we concentrate on projection of FA overtimed alphabets. Given B and a timed language Lt satisfying
Lf (B) ≈tr Lt , we would like to build B ↑Σo from B, such that
Lf (B ↑Σo ) ≈tr PΣo ,t (Lt ), where Σo denotes the observablealphabet.
We use symbols a, b, c, ... (with or without subscripts) todenote the observable symbols from Σo , and the single symbolτ (with or without subscripts) to denote all the unobservable
ones from Σ \ Σo in the following discussions.
A. Projection of languages
We start our analysis with an arbitrary timed word
wt0 = (a1 , t1 )(a2 , t2 ) . . . (an , tn )(1)

in the timed language PΣo ,t (Lt ). The case where wt0 is εt isalso contained in the form (1), by letting n = 0. There must
exist some wt in Lt such that PΣo ,t (wt ) = wt0 . Without lossof generality, wt is of the form
wt = u1t · (a1 , t1 ) · u2t · (a2 , t2 ) · · · unt · (an , tn ) · un+1t(2)

where for 1 ≤ j ≤ n + 1, ujt is either εt or an “unobservable”

timed word (τ, tj1 ) . . . (τ, tjmj ) with tj−1 ≤ tj1 ≤ . . . ≤tjmj ≤ tj (t0 and tn+1 are deemed to be 0 and +∞respectively).
As Lf (B) ≈tr Lt , there also exists in Lf (B) some w similar
to wt in the structure, that is,
w = u1 · (a1 , Λ1 ) · u2 · (a2 , Λ2 ) · · · un · (an , Λn ) · un+1 (3)TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

where for 1 ≤ j ≤ n + 1, uj is either ε or a timed word(τ, Λj1 ) . . . (τ, Λjmj ) such that for 1 ≤ j ≤ n + 1, tj − tjkj ∈Λj and for 1 ≤ k ≤ mi tjk − tj(k−1) ∈ Λjk (t0 and tn+1 aredeemed to be 0 and +∞ respectively, and each tj0 is tj−1 for1 ≤ j ≤ n + 1).
Although the projection of a timed word wt as in (2) over
Σo is PΣo ,t (wt ) = (a1 , t1 )(a2 , t2 ) . . . (an , tn ) = wt0 , this is
not suitable for the projection of w as in (3). If we delete all
the unobservable uj roughly, the result would be (a1 , Λ1 ) ·(a2 , Λ2 ) · . . . · (an , Λn ), which does not satisfy wt0 ∈ [w0 ]any more, because in a timed word wt , each time stamp isthe amount of time elapsed since the beginning of wt (i.e.,
the physical time when the event occurs), while in w, each
duration contains all the possibilities of time elapsed since
the occurrence of its previous action (i.e., the logical time
related to its previous event). In other words, each symbolduration pair, no matter observable or not, plays a part bothin w and in its projection. The projection of w, denoted as
w0 = P↑Σo (w) and to guarantee {P↑Σo (w)} ≈tr PΣo ,t ([w]),will be defined below. We use a different notation here to
avoid confusion with the projection of normal words and timed
words. And slightly overloading the notation, P↑Σo (L) denotes
the set {P↑Σo (w) | w ∈ L}.
There still remains one thing to do before formally defining
the function P↑Σo , to recall the addition operation “+” (and“Σ”) on sets of nonnegative real numbers. Let Λ1 , Λ2 , ..., Λmbe subsetsPof R≥0 . Λ1 + Λ2 := {λ1 + λ2 | λ1 ∈ Λ1 ∧ λ2 ∈mΛ2 }, and j=1 Λj = Λ1 + Λ2 + · · · + Λm . This operation iscommutative and associative.
Moreover the star operation canS
be defined: Λ∗ = k∈N kΛ, where 0Λ = {0} and (k + 1)Λ =kΛ + Λ.
For w as in (3), P↑Σo (w) is inductively defined based on
the number of observable symbol-duration pairs in w:
P↑Σo (u1 ) = ε;1P↑Σo (u (a1 , Λ1 )) =((a1 , Λ1 ),if u1 = εPm1(a1 , k=1 Λ1k + Λ1 ), otherwiseP↑Σo ((u1 (a1 , Λ1 )) · wsuffix ) = P↑Σo (u1 (a1 , Λ1 )) · P↑Σo (wsuffix )where u1 is either ε or (τ, Λ11 ) . . . (τ, Λ1m1 ). According to its
definition, if we factorise the duration word w into w1 · . . . ·wn · un+1 where wj = uj · (aj , Λj ) for each 1 ≤ j ≤ k, wewill have P↑Σo (w) = P↑Σo (w1 ) · P↑Σo (w2 ) · . . . · P↑Σo (wn ) ·P↑Σo (un+1 ) = P↑Σo (w1 ) · P↑Σo (w2 ) · . . . · P↑Σo (wn ).
Lemma 4.1: {P↑Σo (w)} ≈tr PΣo ,t ([w]).
Proof: Firstly, P↑Σo (w) = ε if w is either ε or (τ, Λ11 ) ·. . . · (τ, Λ1m1 ). In either case, PΣo ,t (wt ) = ε for each wt in[w], so [w] = {εt }. Then {P↑Σo (w)} ≈tr PΣo ,t ([w]).
Secondly, let w = w1 · . . . · wn · un+1 , and w0 = P↑Σo (w) =P↑Σo (w1 )·P↑Σo (w2 )·. . .·P↑Σo (wn )·P↑Σo (un+1 ) = (a1 , Λ01 )·(a2 , Λ02 ) · . . . · (an , Λ0n ).
For any wt ∈ [w], wt = (τ, t11 ) · . . . · (τ, t1m1 ) · (a1 , t1 ) · . . . ·(τ, tn1 )·. . .·(τ, tnmn )·(an , tn )·(τ, t(n+1)1 )·. . . (τ, t(n+1)mn+1 ),and wt0 = (a1 , t1 ) · . . . · (an , tn ). If uj = ε, tj − tj−1 ∈Λj = Λ0j . If uj is not an empty word, as tj − tjkj ∈ Λj andtjk − tj(k−1) ∈ ΛP
jk for 1 ≤ j ≤ n + 1 and 1 ≤ k ≤ mi ,mj
tj − tj−1 ∈ Λj + k=1
Λjk = Λ0j .

7

Similarly, for any wt0 = (a1 , t1 ) · (a2 , t2 ) · . . . · (an , tn ) ∈PΣo ,t ([w]), it holds that each tj − tj−1 ∈ Λ0j (t0 = 0).
To sum up, {P↑Σo (w)} ≈tr PΣo ,t ([w]).
B. Projection of FA
We show how to construct B ↑Σo .
Suppose the FA under considerationis B=
S(S, Σt , δ, Init, F ), where Σt =
{σ}
×
T
and
σ
σ∈Σ
Σ = Σo ] {τ } is partitioned into an observable set Σoand an unobservable set {τ }. Fix a run ρ of B, whose trace
is w ∈ Lf (B), such that w = w1 · . . . · wn · un+1 , where
wj = uj · (aj , Λj ) for each 1 ≤ j ≤ k. Its projection is w0 =P↑Σo (w) = P↑Σo (w1 )·P↑Σo (w2 )·. . .·P↑Σo (wn )·P↑Σo (un+1 ).
Although P↑Σo (un+1 ) = ε, un+1 still matters since the trace
is an accepted one. Hence we can deal with each segment
wj separately and finally put them together. Each wj also
comprises two parts: the first is uj which is unobservable or
empty, and the second is observable (aj , Λj ) meaning that
there is a transition (sjmj , (aj , Λj ), s0jmj ).
1) Sum of successive unobservable transitions: We firstdeal with the case where uj is a sequence of unobservabletransitions, that is, uj = (τ, Λj1 ) . . . (τ, Λjmj ). So the corre(τ,Λj1 )(τ,Λjmj )sponding segment of the run ρ is sj0 −−−−→ sj1 · · · −−−−−−→(aj ,Λj )sjmj −−−−−→ s0jmj . If j = 1, the starting state s10 should
be an initial state of B. If j > 1, sj0 should be thesame as the ending state of its previous segment, that is,
sj0 = s0(j−1)mj−1 is also the post-state of the observabletransition (s(j−1)mj−1 , (aj−1 , Λj−1 ), s0(j−1)mj−1 ).
In the case where uj = ε, the corresponding segment of ρ is(aj ,Λj )therefore sj0 −−−−−→ s0j0 , such that sj0 is initial if j = 1 andis the post-state of (s(j−1)mj−1 , (aj−1 , Λj−1 ), s0(j−1)mj−1 ) if
j > 1.
As a consequence, we should delete all the unobservable transitions from B, and add new transitions with labelsP↑Σo (wj ).
A new transition (s, (aj , Λ0j ), s0 ) with an observable label
should be subject to the following restrictions:• Its pre-state s is an initial state, or the post-state of anobservable transition;0• its post-state s is the post-state of an observable transition
with symbol aj , say (sjmj , (aj , Λj ), s0jmj );•(τ,Λj1 )(τ,Λjmj )there is a segment of run sj0 −−−−→ sj1 · · · −−−−−−→(aj ,Λj )sjmj −−−−−→ s0jmj , where mj ≥ 1 such that s = sj0 ,Pmj
s0 = s0jmj and Λ0j = k=1
Λjk + Λj .
In the sequel we explain the steps to obtain such newtransitions based on B.
Firstly we calculate the sum of durations of a sequence ofunobservable transitions, of which the first starts in either an
initial state of B or the post-state of an observable transition,and of which the last ends in the pre-state of an observabletransition. Slightly overloading the notation, Prea and Posta
denote the set of states which are pre- and post-states oftransitions with the observable symbol “a” in its label. To
this end, a new FA Bτ is constructed according to B.
Definition 8: Bτ = (Sτ , Στ , δτ , Initτ , Fτ ), where

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

- Sτ = S;- Στ = Tτ , the set of the duration parts of τ -transitions inB;- δt (s1 , Λ) = {s2 | s2 ∈ δ(s1 , (τ, Λ))}, in other words,(s1 , Λ, s2 ) is a transition in Bτ iff (s1 , (τ, Λ), s2 ) is atransition in B;S- Initτ = InitS∪ a∈Σo Posta , and- Fτ = F ∪ a∈Σo Prea .
Below is shown how to calculate regular expressions corresponding to traces in Bτ from one state to another andto transform each regular expression into a duration, i.e., asubset of nonnegative real numbers. This can be done byfollowing the Floyd-Warshall algorithm (a well-known method
for proving the Kleene’s Theorem).
We first rename states in Sτ as s1 , ... , s|Sτ | , since Sτ isfinite.
Suppose si → . . . → sj is a run from si to sj whoselabels above the right arrows are omitted for simplicity here.
If there is no state between si and sj , the set of all suchruns is denoted as Runi,j (0), and REi,j (0) is used to denote
the regular expression expressing all the traces of runs in
Runi,j (0). If all the states between si and sj have subscripts
less or equal to k, the set of all such runs is denoted as
Runi,j (k), and REi,j (k) is defined similarly. It is trivial that
Runi,j (k) ⊆ Runi,j (k + 1) for 0 ≤ k < |Sτ |; therefore
REi,j (k) can be calculated inductively for 0 ≤ k ≤ |Sτ |.
Thus we can finally obtain the required REi,j (|Sτ |) for eachpair of (s0 , sf ) ∈ Initτ × Fτ .
In the base case, we compute REi,j (0) for each pair (si , sj )as: 1) If si 6= sj and there is no transition from si to sj ,REi,j (0) = ∅. 2) If si 6= sj and the set of labels of transitions
from si to sj , Σi,j = {Λ | sj ∈ δt (si , Λ)} is nonempty,
we rename those labels as Λ1 , ..., Λ|Σi,j | . Then REi,j (0) =Λ1 + . . . + Λ|Σi,j | . 3) If si = sj and there is no transition
from si to sj , REi,j (0) = ε. 4) If si = sj and the set oflabels of transitions from si to sj , Σi,j = {Λ | sj ∈ δt (si , Λ)}
is nonempty, we rename those labels as Λ1 , ..., Λ|Σi,j | . Then
REi,j (0) = ε + Λ1 + . . . + Λ|Σi,j | .
In the step case, we recursively compute REi,j (k + 1) =REi,j (k) +REi,k+1 (k) · REk+1,k+1 (k)∗ · REk+1,j (k). This isbecause any run ρ in Runi,j (k + 1) is either in Runi,j (k) or
is a run where the state sk+1 occurs at least once. If the statesk+1 occurs at least once in a run ρ, this run can also be split
into three segments: the first part is from its start si to the firstsk+1 , the second part is from the first sk+1 to the last sk+1 ,and the third one is from the last sk+1 to its end sj . Also thesecond part is split into at least one segments, each of whichstarts in sk+1 , ends in sk+1 , and has no states with subscripts
larger than k in between.
Finally we can obtain REi,j (|Sτ |) for each pair of states(si , sj ), which expresses all the possible traces of runs fromsi to sj .
After regular expressions have been obtained, it is necessary
to transform them into appropriate durations, i.e., subsets ofR≥0 . For the base clause, ∅ is transformed into the empty set ∅,ε into the set {0}, and Λ into the set Λ itself. For the inductive
clause, if r, r1 , r2 are regular expressions transformed into Λ,Λ1 , Λ2 respectively, then r1 ·r2 is transformed into Λ1 +Λ2 :=8{λ1 + λ2 | λ1 ∈ Λ1 ∧ λ2 ∈ Λ2 }, r1 + r2 into
S Λ1 ∪ Λ2 :={λ | λ ∈ Λ1 ∨ λ ∈ Λ2 }, and r∗ into Λ∗ := k∈N kΛ, where0Λ = {0} and (k + 1)Λ = kΛ + Λ.
In conclusion, for each pair of states (si , sj ) ∈ Initτ × Fτ ,we can obtain Λsi ,sj from REi,j (|Sτ |), so as to determinei) whether si can reach sj via unobservable transitions bychecking whether Λsi ,sj is nonempty; ii) the time durationfrom si to sj if it is reachable. In this step the complexity isO(|Sτ |3 ).
2) Merging unobservable durations into observable transitions: After the analysis of all the uj above, we would like toconsider wj by merging the duration on uj into the observable(aj , Λj ) so as to build the automaton B ↑Σo = (Sp , Σp , δp ,Initp , Fp ).
The states and initial states of B ↑Σo can be set to be thesame as those of the original B.
Transitions of B ↑Σo are all of the form (si , (a, Λnew ), sk ).
A new transition (si , (a, Λnew ), sk ) should be included if there(a,Λ)

exists sj and Λ such that sk −−−→ sj , si can reach sj via
unobservable transitions in B, and Λnew = Λ+Λsi ,sj . Formallyδp is defined such that δp (si , (a, Λnew )) = {sk| ∃sj ∃Λ sk ∈δ(sj , (a, Λ)) ∧ Λsi ,sj 6= ∅ ∧ Λnew = Λ + Λsi ,sj }.
And the alphabet can be derived from the transitions. Thatis, Σp = {(a, Λ) | ∃s δp (s, (a, Λ)) 6= ∅ }.
The accepting states needs special attention. sk is an accepting state if and only if i) sk is an initial state or the
post-state of some observable transition, and ii) sk can reachan accepting state via zero or more unobservable transitions.

Formally, letSFreach = {sk | ∃sf ∈ F Λsk ,sf 6= ∅ }, so
Fp = (Init ∪ a∈Σo Posta ) ∩ Freach .
Thus, the construction of B ↑Σo is done. B ↑Σo has thesame number of states as the original B and the unobservable
Bτ , and at most |δo | ∗ |Sτ |2 transitions, where δo stands for
restricting δ, the set of transitions of B, to the observable set.
Theorem 4.1: The accepting language of B ↑Σo is exactly
the projection language P↑Σo (Lf (B)).
Proof: Follows from the construction in this section.
Note that the proposed scheme in our work of projection issimilar to [14] in that the Floyd-Warshall algorithm is utilized
in both work to compute the “sum” of a sequel of nonnegative(resp. positive) sets.
Besides, as there is no special constraints on the timelabelling function in our definition of RTA, i.e., any nonempty
subset of R≥0 is allowed, so normal form of sets in K(Int)can be circumvented in our theoretical analysis. But in our
implementation, we utilize normal forms to obtain a finite
subset of 2R≥0 for any regular expression over finite subsets
of 2R≥0 .
V. D ECIDABILITY
Now let’s come back to the language-opacity and initialopacity problems for RTA, and fix an RTA A with an alphabet
Σ.
First we focus on language-opacity. Let a “secret” RTA
Asecret accept the secret language. A and Asecret are assumed
to share a common alphabet Σ, as we can always expand theA. A simple example of language-opacity
TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS,
VOL. ?,
NO.method?, ?? ???? with a simple example.
We illustrateouralphabet to the union of their alphabets. We need to determine
whether PΣo ,t (L(A)) ⊆ PΣo ,t (L(A) \L(Asecret )).
The following theorem indicates that the language-opacity
problem of RTA is decidable.
Theorem 5.1: The language-opacity problem of RTA isdecidable.
Proof: Consider an RTA A and a “secret” RTA Asecretacceptingthe tosecretlanguage.
AccordingSection
III, two
two FA,FA, saysay BB andand BBnsns, , cancan bebe
Accordingto Section
III,
AccordingtoSectionIII,
two FA, accept
say B languages
and Bns , canbeconstructed
such
that
they
respectively
traceconstructed such that they respectively accept languages traceconstructed
such
that
they
respectively
acceptlanguages
traceequivalent toto L(A)
L(A) andand L(A)L(A)\\L(A
L(Asecret).
secret).
equivalentequivalentto L(A)and L(A)\ L(Asecret ). to obtain B ↑Σ
AccordingtoSectionIV,
itisnaturalAccording to Section IV, it is natural to obtain B ↑Σoo
to Sectionit (Lis fnatural
to Pobtain
B(Bns
↑Σ))o
andAccording
which
acceptIV,(B)) and(Lff(B
↑Σo(L
↑Σo(L
and
BBnsns ↑↑ΣΣoo which
acceptPP↑Σf (B)) and P↑Σ
ns ))
o
o
and
B
↑
which
accept
P
(L
(B))
and
P
(L
(B
ns Σo
↑Σo
f
↑Σo
f
ns ))
respectively.
respectively.
respectively.
Finally,we
wecan
canapply
applythethecomplementation
complementationand
andproductproductopopFinally,
Finally,wecanagain,apply andthe complementation
andproduct
operationsonthemobtain
B
=
B
↑
×(B
↑
final
Σ
ns
erations on them again, and obtain Bfinal = B ↑Σoo ×(Bns ↑ΣΣoo
comperations
on
them
again,
andobtain
B
=
B
↑
×(B
↑
Σo to AΣo
Clearly, AA isis language-opaquelanguage-opaquefinal
with respect
respect
secret))comp. . Clearly,
withto Anssecret)compΣ
. oClearly,A
is iflanguage-opaquewith respect
to Asecret
and
if
and
only
L
(B
)
is
empty.
Itiswell-knownffinal
and Σo if and only if Lf (Bfinal ) is empty. It is well-known
and theΣ latter
if andis only
if Lf (Bfinal ) is empty. It is well-known
that
decidable
[15].
that
theo latteris decidable
[15].
that
the
latterisdecidable[15].
In thethe following
following theoreticaltheoretical complexity
complexity inin thethe worst
worst case
case
In
In
the following
theoreticalcomplexityin Σ
thecomprises
worst casel
isdiscussed.
Supposethecommonalphabet
is discussed. Suppose the common alphabet Σ comprises lis discussed.
thealphabet
Σcomprisesforl
events,A has
has Suppose
states andand common
m transitionstransitions(kσσ transitionstransitions
events,A
nn states
m
(k
for
0
events,σ),A andhas A
n secretstateshas
andn0 0mstatestransitions(ktransitions (kfor
0 0 σ transitions
each
and
m
each σ), and Asecret has n 0 states and m 0 transitions (kσ0σ0
each σ), andAsecretσ).has n states and m transitions (kσtransitions
for eacheachtransitionsforσ).
transitions
forhaseach
σ).
FirstlyBstates andand mm transitions,transitions, while
while BBnsns has
hasFirstly B has nn states0+k0σFirstly
has andn statesandmtransitions,
while
B
has
ns
0 0 + 1) B
00 +kkσσ+kn(nstatesn(n1)2σ-transitionsforeach
n(n 0+ 1) states and n(n 0+ 1)2 kσ +kσ0 σ-transitions for eachn(nSecondly,+ 1) statesandn(n+ 1)2 Bσ ↑σ-transitions
for
each
σ.
for
their
projections,hasnstatesandσ. Secondly,
for their projections, B ↑ΣΣoo has n states and0kσ +k0 σ
σ.2 Secondly,
for their projections,statesandσ-transitions
for eacheach σσ B∈∈ ↑ΣΣΣooo, , has
andnBBsecret
σ0 σ-transitions
secret ↑↑ΣΣonn2222kkσσ+k
for
and
0
o
+k0σ
3 okk, σ+k+k0 σn 2 n(nσ-transitionsfor (n(neach0 0 σ+ ∈andB↑secret
Σo
0 +
3Σ
has
1)
statesand1))2transitions
σhas n(n 0 + 1) states and (n(n 0 + 1)) 32 kσ +kσ0 transitions
σhas eachn(n + 1) statesWhen
and we(n(nunify
+ 1))
2
for
alphabets
oftransitions
the twotwoforeach σσ ∈∈ ΣΣoo. . When
we unifyalphabetsofthefor each σ it’s
∈ Σ
weunifytwoalphabets
of wethemusttwoo . Whenprojections,
possibletoobtainNFA,soprojections, it’s possible to obtain two NFA, so we must
projections,it’spossibletoobtain
two
NFA,
so
we
must
transform
B
↑
into
DFA,
whose
numberofstatesbecomestransformB ↑ΣΣoo into DFA, whose number of states
becomes00n(n0 +1)+1) B ↑Σn(n+1)
transform
into
numberof0 +1)statesbecomes.Thus
ThusthethefinalDFA,
resultwhose
Bfinalhasn(2n(n+1)states,ofinal has
22n(n
.
final
resultBn(2+1)
states,00n(n +1) 4 04 kσ +k0 0
n(n +1)
σ)
2
Thus
the
final
result
B
has
n(2
+1)
O(n
4. n
04 2
kσ +k
final
σ
and22O(n 4n 042 kσ +k0) transitionstransitionsfor
foreacheachσσ ∈∈ΣΣoo. .The
Thelastlaststates,
thing
and
thing
σ)
O(n n 2and
2transitions
for
each
σ
∈
Σ
.
The
last thingowith respect
check emptinessemptiness ofof BBfinal
in linearlinear time
time withfinal, , inisis toto check
respect toto
is final
to .S|
checkof Bfinal , in linear time with respect to|B· |Bemptiness.δ|.
final.δ|.
|B
final .S| · |Bfinal
|BIn
.S|
·
|B
.δ|.
finalpractisefinal
the numbers
numbers ofof states
states andand transitionstransitions areare muchmuch
Inpractise theIn practise
the cannumbersof thestatesand transitions
are prune
much
smaller,since
we
simplify
resulted
automata
andsmaller, since we can simplify the resulted automata and prune
smaller,
since
we
can
simplify
theresulted
automata
andpruneuseless statesstates andand transitions.
transitions.
useless
useless
statesandtransitions.
Then
we
turn
to
initial-opacity. Let
Let SSsecretbe aa secretsecret set
set ofofsecret be
Then we turn to initial-opacity.
Then
we
turn
to
initial-opacity.
Let Sassecretbea secret set ofofstates,
and
we
use
L
(A)
and
L
(A)
the
abbreviationssnsstates, and we use Ls (A) and Lns (A) as the abbreviations ofstates,
and
we
use
L
(A)
and
L
(A)
as
the
abbreviationsofsTr(Init \ Ssecretns ) respectively.
Tr(Init∩∩SSsecretand Tr(Initsecret)) andTr(Init\ Ssecret) respectively.
Tr(Init∩S)
and
Tr(Init\S)
respectively.
secretsecret
Let LLsecret
L(A)\\LLnsns(A).
(A). Then
Then AA isis initial-state
initial-state opaque
opaquesecretLet==L(A)
Letrespect
Lsecret to= SL(A)\ LnsΣ(A).
Then
A
is
initial-state
opaque
with
and
iff
P
(L(A))⊆P(L(A)\
secretoΣ,tΣ,twith respect to Ssecret and Σo iff PΣoo,t (L(A)) ⊆ PΣoo,t (L(A)\withrespect
to language-opaqueSsecret and Σo iff withPΣo ,trespect(L(A))to⊆LPsecret
Σo ,t (L(A)\
L
)
iff
A
is
and
secretLsecret ) iff A is language-opaque with respect to Lsecret and ΣΣoo. .
Lsecret ) iff theA isinitial-opacity
language-opaquewithofrespect
Lsecretand Σo .
Therefore
problem
RTAisistoalso
also
decidable.
Therefore
the initial-opacity
problemof RTAdecidable.
Therefore
theinitial-opacity
problem
of
RTA
is
also
decidable.
Theorem 5.2:
5.2: The
The initial-state
initial-state opacity
opacity problem
problem forfor RTA
RTA isis
Theorem
Theorem 5.2: The initial-state opacity problem for RTA isdecidable.
decidable.
decidable.

b[2, 4]
a[2, 5]s1s2

b[3, 4]
a[1, 3]

9

s3

(a)AA
(a)

99

a
b
s01
s02
s03
[4,
5]
[3,
5]
The two
two RTA
RTA under
under study
study areare asas inin Figure
Figure 2(a)2(a) andand Figure
Figure
The
2(b).
L(A)
is
{ε
}
∪
{(a,
t
)
|
t
∈
[2,
5]}
∪
{(b,
t
)
t
1
1
1
2(b). L(A) is {εt } ∪ {(a, (b)t(b)|secrett1 ∈ [2, 5]} ∪ {(b, t1 ) || tt11 ∈∈secret
1 )AA
[2,
4]}
∪
{(a,
t
)(a,
t
)
|
t
∈
[2,5]5]∧∧(t(t22 −−tt11)) ∈∈ [1,[1,3]}
3]}∪∪
1
2
1[2, 4]} ∪ {(a, t1 )(a, t2 ) | t1 ∈ [2,
{(a,
t
)(b,
t
)
|
t
∈
[2,
5]∧(t
−t
)
∈
[3,
4]}∪{(b,
t
)(a,
Fig.
2:
A
and
A
1
2
1
2
1
1
Fig.
2:
A
and
A
secretsecret{(a, t1 )(b, t2 ) | t1 ∈ [2, 5]∧(t2 −t1 ) ∈ [3, 4]}∪{(b, t1 )(a, tt22))||[2,4]4]∧∧(t(t22−−tt11)) ∈∈ [1,[1,3]}
3]}∪∪{(b,{(b,tt11)(b,)(b,tt22)) || tt11 ∈∈ [2,[2,4]4]∧∧
tt11 ∈∈ [2,
(t
−
t
)
∈
[3,
4]}.
And
L
=
L
(A
)
is
{(a,
t
)(b,
2
1
secretfsecret1(t2 − t1 ) ∈ [3, 4]}. And Lsecret = Lf (Asecret ) is {(a, t1 )(b, tt22))||t15])5]∈∧∧[3,
L[3,
[4,
∈[3,
5]}.= Lf (Asecret ) is {(a, t1 )(b, t2 ) |2∈−secret1))∈
tt1(t1 ∈[4,(t(t224]}.
−−tt1And
5]}.
t1The
∈ [4,
5]
∧
(t
−
t
)
∈
[3,
5]}.
The
whole
processisasfollows.
2
1
whole process is as follows.
The whole
process
is B
as andfollows. which accept languages
Firstly
weconstruct
Firstly we construct B and BBnsns which
accept languages
Firstly we constructBandandBns \which
acceptlanguages
trace-equivalent
to
L(A)
L(A)
L(Asecretrespectively.
secret)) respectively.
trace-equivalent to L(A) and L(A)\ L(Atrace-equivalent
to
L(A)
and
L(A)
\
L(A
)
respectively.
secret(1) Construct
Construct B.
B.
(1)(1) ConstructB.done directly, and the resulting B is
This
can
be
This can be done directly, and the resulting B is
This canbedone 3(a).
directly,
and thealphabet
resulting B is
depicted
FigureIts timed
timed
depictedinin Figure3(a). Its
alphabet ΣΣt1t1 isis
depictedinFigure
3(a).
Its
timed
alphabet
Σt1 is{(a,[1,[1,3]),3]),(a,(a,[2,[2,5]),5]),(b,(b,[2,[2,4]),4]), (b,(b,[3,[3,4])}.
4])}.
{(a,{(a, [1, 3]), (a, [2, 5]), (b, [2, 4]), (b, [3, 4])}.
(b,[2,[2,4])
4])(b,(b,[3,[3,4])
4])(b,

ss11 (a, [2, 5]) ss22 (a, [1, 3]) ss33
(a, [2, 5])(a, [1, 3])
(a)
(a)
(a)BB
B

(a, [4, 5])(b, [3, 5])
0 (a, [4, 5])0 (b, [3, 5])
0
ss011
ss022
ss033
(b) BBsecret(b)(b) BsecretsecretFig.
FA
directly
derived
from
A
and
A
secretFig.
Fig.3:3:
3:FA
FAdirectly
directlyderived
derivedfrom
fromA
Aand
andA
Asecretsecretcomp
compcomp .
(2)
Construct
secret(2)(2)Construct
ConstructBB
Bsecretsecret. .
We
firstconstruct
as in
Figure
3(b).
Then
we
refinesecret as
We
BB
Wefirstfirstconstructconstruct
BsecretinFigure
Figure3(b).
3(b).Then
Thenwewerefine
refinesecret asin
0
0
0
B
into
B
,
which
looks
the
same
as
B
,
whose
secret into
secret, , whose
secretBBsecret
,
which
looks
the
same
as
B
,
which
looks
the
same
as
B
whose
secretsecretsecret into BB
secretsecrettimedalphabetis {(a,
[4,
5]),
(a,
[0,
4)
(5,
+∞))}
timed
∪∪
timedalphabetalphabetisis
isΣΣ
Σt2t2
{(a,[4,[4,5]),5]),(a,(a,[0,
[0,4)
4)∪∪
∪(5,
(5,+∞))}+∞))}∪
t2 isis{(a,
comp
comp
comp
{(b,
[3,
5]),
(b,
[0,
3)
∪
(5,
+∞))}
instead.
Hence
B
can
secret can{(b,{(b,[3,[3,5]),5]),(b,(b,[0,[0,3)3)∪∪(5,(5,+∞))}+∞))} instead.
instead. Hence
Hence BBsecretcansecretbeconstructed,
asshown
FigureElements
are
be
inin
be constructed,
constructed, as
as shown
shown
in Figure
Figure 4.4.
4. Elements
Elements inin
in ΣΣ
Σt2t2
are
t2 are000
000
0 0, a0000, b0 0, b0000 respectively.
abbreviatedtoaabbreviatedabbreviatedtotoaa, ,aa , ,bb, ,bb respectively.
respectively.

0
ss011
00 0 00
aa00 ,,bb0 ,,bb00

0
aa0

0
ss022
0 00 00
aa0 ,,aa00 ,,bb00

a ,b ,b

0
bb0

0
ss033
0 00 0 00
aa0 ,,aa00 ,,bb0 ,,bb00

0
ss044

A. AA simple
simple example
example ofof language-opacity
language-opacityA.
0 00 0 00
A. A simple example of language-opacity
aa0 ,,aa00 ,,bb0 ,,bb00
We illustrate
illustrate ourour method
method with
with aa simple
simple example.
example.
We
comp
0
comp
We illustrate our method with a simple example.
Fig. 4:
4: Bcomp
the complement
complement ofof B0 0secretsecret,, theFig.
secretsecretFig.
4: BBsecret, the complementof BBsecret
The two RTA under study
are as in Figure 2(a) and Figure
bb t ) | t ∈ [2,bb5]} ∪ {(b, t ) | t ∈2(b). L(A) is {εt } ∪ {(a,(3) Construct
Construct Bns .
1
1
1
1
(3)
(3)
Construct BBnsns. .
comp[3,(t4]4] − t s)3 ∈ [1, 3]} ∪s11 t2[2,[3,comp[2, 4]} ∪ {(a, t1s)(a,)[2,|4]4]
t1 ∈ ss[2,5]∧We
first refinerefine B
B and
and B
Bcomp
by thethe partitioned
partitioned timed
timed alphabetalphabet2
2
1s3
secret by2
Wefirstfirst
secretaaWe
refine
B
and
B
by
the
partitioned
timed
alphabet∪
secretaa{(a, t1 )(b, t2 ) | t1 ∈ [2, 5]∧(t
−t
)
∈
[3,
4]}∪{(b,
t
)(a,
t
)
|
{(a,
[1,
2)),
(a,
[2,
3]),
(a,
(3,
4)),
(a,
[4,
5]),
(a,
[0,
1)
2
1
1
2
{(a,[1,[1,2)),
2)),(a,(a,[2,[2,3]),3]),(a,(a,(3,(3,4)),
4)),(a,(a,[4,[4,5]),5]),(a,(a,[0,
[0,1)
1)
∪
[2,
5] 3]} ∪ {(b,[1,t1 ∈ [2, 4] ∧ (t2 − t1 )[2,
∈ 5]
[1,
t[1,
(5, +∞)),+∞)),(b, [2,[2, 3)),
3)), (b,(b, [3,[3, 4]),4]), (b,(b, (4,(4, 5]),5]), (b,(b, [0,[0, 2)2) ∪∪∪3]3] t2 ) | t1 ∈ [2, 4] ∧ {(a,1 )(b,(5,(b,(5, +∞)),(b, [2, 3)), (b, [3, 4]), (b, (4, 5]), (b, [0, 2)∪(a) AA(5,+∞))}+∞))} obtained
obtained fromfrom ΣΣt1t1 andand ΣΣt2t2. . We
We useuse aa11, , aa22, ,
(a)
(5,
a
,
a
,
a
,
b
,
b
,
b
,
b
as
abbreviationsforthenine labels
labelsa33, a44, a55, b11, b22, b33, b44 as abbreviations for the nine
0
0
0
aa
bb
in
order.
And
theresultingautomataarein
Figure
5(a)
and
ss011
ss022
ss033
in order. And the resulting automata are in Figure 5(a) and(3) ConWe first{(a, [1, 2))(5, +∞)),(5, +∞))}
a3 , a4 , a5in order. A
Figure 5(bBy cons
FA B p , assimplifyin

Specially,others are equal to {0}. Then in our B ↑Σo , the transitions are V-A is in(s1 , (a, [2, 5]), s2 ), (s2 , (a, [1, 3]), s3 ) and (s1 , (a, [3, 7]), s3 ).
S=
Fp = {s, s3?,},??and1, s
TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND
SYSTEMS,VOL.
?,2NO.
???? Initp = {s1 }.
10
1(5, +∞))} obtained from Σt1 and Σt2 . We use a1 , a2 ,
a3 , a4 , a5 , b1 , b2 , b3 , b4 as abbreviations for the nine labels
in order. And the resulting automata are in Figure 5(a) and
Figure 5(b).
ss1 1
s1

aa2 2, ,aa3 3, ,aa4 4
ab21b,1,a,b32b,2a4

ss2 2

aa1 1, ,aa2 2
ab12b,2a2

ss3 3

s2
s3
0 00
(a)BB
B
(a)
b1 , b2(a)b2a2 , a3 , a4 b0 b2, ,bb3a1 , a2(a) Bs aa4 4s3
0 0 s22 300
ss01 01 1
b1 , b2ss2 2
b2ss3 3b2 , b3
a4
s01 aa1 1, ,aa2 2, ,aa3(a)s3,02,aBa404, ,aa5 5, ,s03
aa1 1, ,aa2 2, ,aa3 3, ,aa4 4, ,aa5 5, ,aa1 1, ,aa2 2, ,aa3 3, ,aa5 5, ,bb, ,bb
b1b1, ,b2b2, ,bs3b0 3, ,b4b4 a41 , a2 ,1 1sa034, 4a4b,2a,5b,3b1b1, ,bs2b02, ,b3b3, ,b4b4
2
a1 , a32 , a3 , a4 , a5 ,
a1 , a2 , a31, a5 ,bs1s0,04b4
b1 , b2 , b3 , b44
b1 , b2 , b3 , b4
a1 , a2 , a30, a4 , a5 ,s4
a1 , a2 , a3 , a4 , a5 ,
a1 , a2 , a3 , a5 ,b ,bb1 , b2 , ba3 ,,ba4 , a , a 1, a 4, b , b ,bb1 ,,bb2 , b3 , b4
a1 1, a2 2, a3 3, a4 4, a5 5, b1 1, b2 2, b3 3, b4 4
s04Bcomp
compcomp0 00(b)(b)
BB
a1 , a2 , a3 , a(b),,secretb1 , b2 , b3 , b4
secret4 a
5secret2(a, [3, 7])3s1(a, [2, 5])s2(a, [1, 3])

s3

4
1010
5
6
10

Fig.
Fig.7:7:BB↑↑ΣΣoo, ,thetheprojection
projectionFA
FAfromfromBB7(a,[4,[4,5])
5])
(a,
8
0
0
ss11110ss2222010(5) Construct Bns ↑Σ9o.
(a, [4, 5])
The construction is ssimilar
to that ofsB
110
220↑Σo , shown in Figure10(a,[3,[3,7])
7])
(a,
11
8.
(a,[2,[2,4))
4))(a,[1,[1,3])
3])
(a,
(a,
(a,
[4,
5])
(a,
[3,
7])
s 0
s220
(a, [2, 4))11(a, [1, 3])
ss24240 0
ss34340 0(a,(a,[3,[1,7])
3])(a, [2, 4))s240 (a, [1, 3]) s34(a,[1, 3])
0
(a,
[1,
3])
Fig.
8:
B
↑
,
the
projection
FA
fromBBnsns
Fig. 8: Bnsns↑ΣΣo o, the projection FA from0s340 FA from Bns
Fig. 8: Bns s↑24
Σoo , the projection(a, [1,0 3])
comp
0 0 ↑ comp(6)Construct
Constructanother
anotherFAFA(B(B0 ↑↑ΣΣo o) )××(B
(Bns
order
(6)
) ) ininorderns↑ΣΣoocomparelanguages
accepted
by
B
↑
and
B
↑
.
This
Fig.
8: Bns ↑Σaccepted,theprojection
FA
from
B
totocompare
languages
by
B
↑
and
B
↑
.
This
isis
Σ
ns
Σ
comp
ns
o
o
Σo 00
ns comp
Σo
o
00 Σ
Σoo )
(6) ConstructanotherFA(3),
(B
↑so
order
ns ↑
o ) × (BnsΣwe
Σosimilarthesteps
steps(2)andand(3),soweomitomit
thedetailsinhere.
here.
similartotothe(2)
thedetails
comp by B ↑Σns ↑Σ
Σoo . This is
comp
toAs
compareo and Bns
0 0 acceptedoAs(B(B0 0↑↑ΣΣolanguages(Bns
acceptsΣ
nothing,
theRTA
RTAAAisis) )××(B) ) accepts
nothing,
the
ns↑↑
o
ΣΣ
oo
comp
comp
similar
to
the
steps
(2)
and
(3),
comp 00 so we omit
0 the details
comp
comp
(b)
B
(6)
Constructanother
FA
(B
↑
)
×
(B
↑
)
in here.
order
Fig.
refinedFA
andlanguage-opaquewithrespect
to
L(A
)
and
Σ
.
Σ
Σ
language-opaquewithrespect
to
L(A
)
and
Σ
.
ns
secretooFig.5:5:
5:refinedrefinedFA
FAsecret
ofBB
Band
andBB
Bsecretsecret
o
comp
Fig.
ofof
secretosecret
comp
00 Σ
00
Σoo )
↑Σ
accepts
nothing,
the
RTA
A is
is
As (B ↑Σlanguages
ns acceptedo ) × (Bns
a1 , a2 , a3 , a4 , a5 , b1 , b2 , b3 , b4
tocompare
by
B
↑
and
B
↑
.
This
o
Σ
ns
Σ
o
o
comp
Fig. 5: refined FAcompof0 0B and comp
Bsecretsecretolanguage-opaquewithrespect
to
L(A
)
and
Σ
.
secreto(2) Iand(3), so we omit the details here.
VI.
I MPLEMENTATION
By constructing the productof B and bBsecret , we can obtain similar to0 the stepsVI.
MPLEMENTATION
comp0
aa4 4(b) Bsecret 0
b2 2
As (B ↑Σo ) × (Bns↑Σo )accepts nothing, the RTA A is
0 Figure 6(a).
ss11110inss22220Then Bns is constructed,
ss33330 0
FA B p , as shownby
Based onon thethe withtheorypart above,
above,
we)havehavedeveloped
comp
Based
theorypart
wedevelopedaa
VI.respect
IMPLEMENTATION
MPLEMENTATION
language-opaqueto
L(Asecret
and Σ
p
VI.
I
5: refined
FA
of
B
and
B
o.
ain
b
secretsimplifying BFig.
, depicted
Figure
6(b).
4
2, a
a
a
,
a
prototypicaltool
for
decidingthelanguage-opacity
problem
prototypical tool for deciding the language-opacity problem
s110
s220
1 1 2 2 s330
Based onon thetheory
theoryreportedpart above,wehavedeveloped
Based
above,
wehaveanddevelopedaa
RTA.TheThethetoolisisimplemented
implemented
withPython
PythonandthuscancanofofRTA.
tool
with
thus
aa2 2, ,aa3 3, ,b1b1, ,b2b2a,aprototypicaltool
for
decidingthelanguage-opacity
problem
12
VI.
I
MPLEMENTATION
prototypicaltool
for deciding
the language-opacity
problem ofa4
aa1 1, ,aa2 2, ,b2bb22
runon
onLinux,
Linux,
Window
andMACMAC
smoothly.
run
Windowandsmoothly.
ss24240 0 s220
ss34340 0 s330
ofBased
RTA.
The
tool
is implemented
withPythonandthus
cana2 , a3s,11b10 , b2
RTA.
The
tool
is
implemented
withPythonandthus
cansysrunonthetheorypart
above,
wehavedeveloped
a
The
tool
needs
two
input
files:
oneisthesysThe tool needs two input files: one is thea1 , a2 , b2
runonLinux,
WindowandMAC
smoothly.
a,aonLinux,
WindowandMAC
smoothly.
prototypicaltool
for
deciding
language-opacity
problem
0
0
1
2
s
s
tem
model
(a.json)
and
the
other
is
the
secret
one
24
34
comp
tem model (a.json) and the other is the secret onecomppp
0 0and(a)BB
theproductproductofofBB
andBB
(a)
, ,the
The
tool
needs
two input
input withfiles:Python
one andis thethesyssecretsecret
The
needs
two
one
is
sysof
RTA. tool
The toolis implemented
thus
can(a_secret.json).
Both models
modelsfiles:
are jsonjson
files
of RTA
RTA(a_secret.json).
Both
are
files
of
a2 , a3 , b1 , b2
tem
model
(a.json)
and
the
other
is
the
secretone
compaof1 ,Ba02and, b2 Btem
model(a.json)
and
the
other
is
the
secretone
runonLinux,
WindowandMAC
smoothly.
[4,5])(a) Bp(a,, (a,the[4,
product
5])models.
models.
secrets240 ss220 0
s340(a_secret.json).
Bothmodels
are
json
files
of
RTA
ss11110 022(a_secret.json).
Bothmodelsareofofjson
files
of RTA
needs
two
input
files:
one
isparts:thesysAjsonjsontool
fileofof
anRTA
RTA
model
consistssevenparts:
AThe
file
an
model
consistsseven(a, [4, 5])models.
models.
(a,
[1,
3])
tem
model
(a.json)
and
the
other
is
the
secret
one
(a,
[1,
3])
comp
0p
p
s11
s BB000 andcomp• “name”“name”
the
nameofofthe
theRTA
RTAmodel,model,•A(a)
B,, the(a)B4))
the productproduct of
of 22
and B
Bsecret(a,[2,4))
json file
fileisisofthe
annameRTA
model
consists
ofjsonsevenparts:
secret
(a,
[2,
A
json
of
an
RTA
model
consistsofsevenparts:(a_secret.json).
Bothmodels
are
files
of
RTA
“s”isisthe
thelistlistofofstates’
states’names,
names,(b,[2,[2,4])
4])• • “s”(b,(a, [1, 3])• “name” is the name of the RTA model,(a,[1,[1,3])
3])(a, [4, 5]) (a,models.
•• “sigma”“name”
is
the
name
of
the
RTA model,(a,s[2,0 4))“sigma”isthealphabet,•isthealphabet,
00sss34340220• json“s” isisfiletheoflist
list
ofstates’names,(b, 11[2, 4]) s24240 s(b,AanlistRTA
model
consists
ofRTA
seven
parts:where
“s”
the
of
states’names,“tran”
thelist
oftransitionstransitions
the
RTA
model,
where
(3,
4))
••• “tran”
isistheofofofthemodel,(b,(a,(3,[1,4))
3])(a, s[1,3])• “sigma” is the alphabet,0s240“sigma”isthealphabet,34•• each“name”
is
the
name
of
the
RTA
model,
eachtransition
is
of
the
key-valueform“id:[source,label,
transition
is
of
the
key-valueform“id:[source,label,(a, [2, 4))(b)BB• “tran” is the list of transitions of the RTA model, where(b)nsns(b, (3, 4))“tran”
is theofkeytransitionsof indexthe
RTA
model,
where•• guard,“s”
is target]”.
thelist listofstates’names,(b, [2, 4])
guard,
target]”.
The
key“id”isisthe
the
index
ofthe
thetransition,transition,
The
“id”
of
(a, [1, 3])each transitiontransitionisof thethe key-value
key-value form
form “id: [source, label,
each
is
of
• and
“sigma”
is theconsists
alphabet,
andthethevaluevalue
consists
fourparts:
parts: “id: [source, label,ofoffournsFig.6:6:s(b)Bpp0Band
andBBnsns s340
Fig.
B24
guard,
target]”.
The
key
“id”
is
the
index
of model,the transition,transition,
guard,
target]”.
The
key
“id”
is
the
index
of
the
• “tran”
is the islist
ofnametransitions
ofpre-state
the
RTA
where
(b, (3, 4))“source”
isconsiststhenamethepre-state
thetransition,transition,–– “source”
the
ofof
the
ofofthe
and
the
value
of
four
parts:
Fig. 6: B p and Bns
and
the
value
consistsoffourparts:
eachtransition
is
of
the
key-valueform“id:[source,label,–“target”
is
the
name
of
the
post-stateofthetransition,– “target” is the name of the post-state of the transition,
(b) B
Bns
ns
(b)
– “source”“source”
isThe
the name
nameof thethepre-stateof thethe transition,transition,
guard,
target]”.
key
“id”
is
the
index
of
–
is
the
of
pre-stateofthetransition,“label”
is
one
of
the
lettersinthealphabet,
andSecondlywe
wecomputecomputethe
theprojection
projectionofofBBand
andBBnsns, ,denoted
denoted– “label” is one of the letters in the alphabet, andSecondly– the“target”
isconsists
the name
nameoffourthe parts:
post-state ofof thethe transition,transition,
andvalueisis
ofof“target”
theof
the
post-state
Fig.
6: B
Bpp and
and
Bns
6:
B
nsrespect“guard”
isthe
union
ofthe
thetimetimeintervals,
intervals,
represented
andBBnsns↑↑ΣΣo oFig.
respectively,
withrespecttotoΣΣo o=={b}.
{b}.
–– “guard”
union
represented
asasBB↑↑ΣΣo oandrespectively,
with–“label”
is
one
of
the
lettersinthealphabet,
andSecondly we compute the projection of B and Bns , denoted“label”
isisnormal
one
thein the alphabet,
and
–– in
“source”
the ofnameoflettersthepre-stateof the transition,
inDima’s
Dima’snormalforms[14],(4)Construct
Construct B↑↑ΣΣo o. .
forms
[14],
–
“guard”
is
the
union
of
the
time
intervals,
representedas(4)B ↑Σo and BB↑
respectively,
withrespect
to
Σ
=
{b}.
Σo
“guard”isthe ofunionofthepost-state
timeintervals,–– “target”
is
the
name
of
the
of therepresented
transition,
Secondly
we ns
computethe twoprojectionof B(s(sandB4],, osdenoted
We firstconstructconstruct
B withtransitions:[2,s2 2) )andand
”init”
thename
name
ofthe
the
initialstate,
andWe
transitions:, ,[2,
ns4],• • ”init”
theinitialstate,
and11
inisisDima’s
Dima’snormalforms[14],(4)first
Construct
B ↑BΣτoτwith. thetwoinnormal
forms
[14],
–
“label”
is
one
of
the
lettersinthealphabet,
Secondly
wecomputeprojection
of
B
and
B
,
denoted
as
↑4],
and
with
respecttons
Σ(s2 2,B,[3,[3,s3 3).).BAll
thethreestatesstatesareareinitial
initialand
accepting.
”observable”isisthe
thelistlistofofobservable
observableletters.
letters. and
(s
All
three
and
accepting.
Σ4],
ns ↑theΣo = {b}.
• • ”observable”
o so respectively,We
firstconstruct
B
with
two
transitions:
(s
,
[2,
4],
s
)
and
• ”init”
is
the
name
of
the
initialstate,
andτ
1
2–“guard”
is
the
union
of
the
time
intervals,
represented
as
B
↑
and
B
↑
respectively,
withrespecttoΣ
={b}.
• ”init” is the name of the initial state, andΣ=[2,4],
4],nsΛBΛs2s↑Σs2Σ3os3o .== [3,[3,4],
4], ΛΛss13s3 == [5,[5,8],
8], and
ando all
all thethe Specially,o [2,ConstructΛΛs1s(4)s12s2 =
thejsonjsonfile
filethetheof
systemmodelletters.
Subsection
theofofthesystemmodel
AAininSubsection(s(4)
4], s3 ). All
the. three statess1 are
initial and accepting. Specially,• ”observable”
islist
observable
2 , [3,inDima’snormalforms[14],
Construct
B↑• ”observable” is the list of observable letters.
Σothersareequalequaltoto{0}.
{0}.
Thentwo
ourBB↑↑ΣΣo o, ,thethe1transitions
are V-A
We arefirst
construct
Boτ Thenwithtransitions:(s,transitions[2, 4], s2 ) areandothersininour
V-A
isin
Listing1
below.
is in Listing 1 below.
Λ 1 s2 first= [2,4], Λs2Bs3 with
= [3,4],transitions:Λ 1 s3 = [5,
8],
and
all
the Specially,
json
file
systemmodel
Subsection
two
(s
,and
[2,[3,
4],
s7]),• ”init” the
isthe
the
name
andA
ofofthethe(a,[2,[2,5]),
5]),(s2τ2, ,(a,(a,[1,[1,3]),ss3s3)are
) and
and
(a,
[3,
s3 3).). Specifically,2 )sand(s1s2We[3,
4],
sconstruct
the
three
statesinitialaccepting.
(s, ,(a,),), (s3]),(s(s,1,(a,
7]),json
fileoftheinitialsystemstate,
model
A in
in Subsection
123 ).ss2All
11others
are
equal
to
{0}.
Then
in
our
B
↑
,
the
transitions
are
Σo
V-A
is
in
Listing1
below.
(s
,
[3,
4],
s
).
All
the
three
statesare
initialand
accepting.
• ”observable”
isbelow.
thelist
observableletters.
S=
F ==[2,{sand[3,Init
Listing1:
Thejsonjsonoffile
file(a.json)
2=F
3 4],
=
4], =
Λ {s1}.}.= [5, 8], and all the V-ASΛ, ,ss2Λ
, ,sss323},
The
ofofAA(a.json)
is in Listing
Listing
11:2s},
2 p p= {s1 1
3 and Initp p= {s(ss11,s(a,[2, 5]),), (s[1, 3]),Λss31)s13and(s18],, (a,and[3, 7]),
2 , (a,[3,3 ).
Λ
4],s2Λ
all sthes1 s2 =s3 =s3 ↑=othersare [2,equal
tos2{0}.
Then 4],in ours1B
the transitionsareFirstly,
we
load
the
json
files
of
two
RTA
models A
Specially,
the
json
file
of
the
systemmodel
A
in Subsection
Σo , [5,1{
1 {S = Fp =equal{s , s2 , {0}.
s3 }, andInit
= {sListing 1: The json file of A (a.json)pour1↑}. , the transitions areothersinBΣo (s1 , (a, [3, 7]), s3 ). 2 V-A(s1 , (a,are[2, 5]),1 s2to), (s(a, [1,
3]),
s
)
and
and
A
,
and
transform
them
into
two
FA
B
and BnsisinListing1
below.
2 , Then3"name":"A",
secret2"name": "A",(a,[3,[3,7])
7])
(a,
{
(s
, (a,
3]),
s3{s
) 1and2 , (a,S 1=
Fp[2,= 5]),{s1s, 2s),and[1,Init}. (s1 , (a, [3, 7]), s3 ).3 13 respectively.
These
two
FA
acceptlanguages
trace-equivalent
2 , s(s
3 },
p =
"s":
["s1","s2","s3"],"s": ["s1", "s2", "s3"],2"name":
S=
s3↑(a,}, oand
Init
=7])
{s
Listing
1: \Thejson
file of A (a.json)(a,p[3,p = {s1 , s2B, ns
1 }.
(5)FConstruct
. 5])
L(A)
and
L"A",
(A)
L(A
"sigma":
["a",
"b"],
f["a",
secret ) respectively.
[2,
5])
(a,
[1,3])
3])
4 4 to "sigma":"b"],(a,Σ[2,
(a,
[1,
3
"s":
["s1","s2","s3"],sss
s1 1 is similar tosthat
s3 3 in Figure515 { "tran":
2 2 of B ↑Σo , shown
Secondly,
The construction"tran":we{{ obtain B ↑Σo and Bns ↑Σo which are the4"sigma":
["a",
"b"],
(a, [2, 5])(a, [1, 3])projections
B
and
B"b",
based
on the observable8.
2"name":"A",
6"0":["s1","b","[2,4]","s2"],
ns respectively(a, [3,
6"0": ["s1","[2,4]","s2"],
s1s2 7])
s3
5"tran":{
Fig.7:7:BB↑↑ΣΣo o, ,thetheprojection
projectionFA
FAfromfromBB3"s":["s1","s2","s3"],
Fig.
7"1":["s1","a","[2,5]","s2"],
7"1": ["s1", "a", "[2,5]", "s2"],
6"0": ["s1","b","[2,4]", "s2"],"sigma":
["a",
"b"],
(a, [2, 5])(a, [1, 3])"2": ["s2",["s2","b","[3,4]", "s3"],"s3"],
848
"2":
"b",
"[3,4]",
Fig. 7:B ↑Σo , the projection
FA fromB7"1":["s1","a","[2,5]", "s2"],
s
s
s
1
2
3
5
"tran":{(5)
Construct
B
↑
.
9
"3":
["s2","a","[1,3]","s3"](5) Construct Bnsns↑ΣΣo o.
9"3": ["s2", "a", "[1,3]", "s3"]8"2": ["s2", "b", "[3,4]", "s3"],

{

"name
"s":
"sigm
"tran
"0":
"1":
"2":
"3":
},
"init

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

action set Σo , by constructing Bτ and calculating the regularexpressions REs corresponding to traces in Bτ . Union, intersection, complement, addition and Kleene star operationsof Dima’s normal forms are implemented according to [14].
The well-known Floyd-Warshall-Kleene Algorithm [16]–[18]is utilized to construct the matrix of regular expressions REi,j .
For calculating and simplifying the k + 1 round formula
REi,j (k + 1) = REi,j (k) + REi,k+1 (k) · REk+1,k+1 (k)∗ ·REk+1,j (k), the Horner’s Rule [19] is applied where theaddition operation, union operation, {0} and ∅ in Dima’s
normal forms are treated as the production operation, addition
operation, 1 and 0 in the polynomials in rational number
domain respectively.
Finally, after transforming the two finite automata into DFA,
we apply the complement and production operations on themagain, and obtain B ↑Σo ×(Bns ↑Σo )comp . Clearly, A is
language-opaque with respect to Asecret and Σo if and only
if Lf (B ↑Σo ×(Bns ↑Σo )comp ) is empty.
The output of the tool is as follows: it returns “languageopaque: true” if the RTA A is language-opaque with respect to
Lf (Asecret ) and Σo ; otherwise, it returns “language-opaque:false”. Intermediate automata during the computation are also
printed, including A, Asecret , B, Bns , B ↑Σo , Bns ↑Σo andthe final automaton B ↑Σo ×(Bns ↑Σo )comp . Besides, after
the deciding procedure, the total elapsed time will be given(in seconds).
The simple example of language-opacity in Subsection V-A
is as a demo in the tool and the result of the example islanguage-opaque with taking 1.67 seconds in our test environment (Inter Core i3-5005U at 2.0GHz and 4GB DDR3L1600MHz RAM). The prototypical tool and its information
can be found at https://github.com/Leslieaj/RTAOpacity.

1
2

{

3
4
5
6
7
8
9
10
11
12
13
14

Listing 1: The json file of A (a.json)"name": "A","s": ["s1", "s2", "s3"],"sigma": ["a", "b"],"tran": {"0": ["s1", "b", "[2,4]", "s2"],"1": ["s1", "a", "[2,5]", "s2"],"2": ["s2", "b", "[3,4]", "s3"],"3": ["s2", "a", "[1,3]", "s3"]},"init": "s1","accept": ["s3"],"observable": ["a"]}VII. C ONCLUSION
In this paper we investigate the opacity problems of RTA,
including language opacity and initial-state opacity. We prove
the two opacity problems both are decidable by reduction to
the language inclusion problem of FA. To this end, we firsttranslate a given RTA into an FA with the corresponding timedalphabet, such that the language accepted by the FA and that11

generated by the RTA are equivalent in the sense of traceequivalence proposed in this paper. Then, in order to guarantee
trace-equivalence relation is preserved by the complement andproduct operation over translated FA, we propose the notionsof partitioned timed alphabet and partitioned language. Basedon them, we further refine the translated FA to an FA withpartitioned timed alphabet, of which the accepted language isstill trace-equivalent to the generated language of the original
RTA. Then, we define a projection operation on refined FA
with partitioned timed alphabets onto the given observable set
by removing all unobservable transitions and merging theirtime durations into the subsequent observable transition. With
such projection, we can show that the accepted language ofthe projection of the refined FA onto the observable set is still
trace-equivalent to the projection of the language generated by
the original RTA onto the same set. Thus, the decidability of
the language and initial-state opacity problems of RTA can be
reduced to the regular language inclusion problem.
Applicability: In [4], Bryans et al. investigated how toformalize security properties like anonymity, non-interference,
etc., which can be essentially reduced to opacity problems,
using labelled transition systems. In [20], Gardey, Mullins andRoux generalized these notions to timed setting in the formalism of timed automata, and proved that non-interference is still
decidable. However, unlike in untimed setting, Cassez provedthat for the very restrictive class of event recording timed
automata (ERA), the language opacity problem is alreadyundecidable in [13], that leaves little hope for an algorithmic
solution to the opacity problem in dense-time. In [14], Dima
pointed out that ERA is incomparable with RTA. Fortunately,in this paper, we prove that the language and initial-stateopacity problems of RTA both are decidable, which reembarks
the hope to automatically verify security properties in timed
settings. Actually, many commonly used communication protocols with time can be modeled using RTA, for example, in[21], Denning and Sacco extended Needham and Schroeder’s
key distribution protocols for both single key and public
key systems with timestamps in order to avoid replays. It
is not hard to model the extended protocols with RTA as
all timing constraints are of the form |clock − T | ∈ [a, b],
where clock stands for a local clock, and T is the given
timestamp. Furthermore, it is possible to model the commonlyused authentication technology Kerberos [22] using RTA, as
its timing part is essentially based on the extended Needham
and Schroeder’s protocols. As one of major future work, wewill investigate how to apply RTA to model more security
protocols.
Another interesting future work is to extend HCSP [23]–[25] and HHL [25], [26] to security for modeling and reasoning about more general security properties, and to investigate
automatic verification techniques for them based on the work
reported in this paper.
R EFERENCES[1] R. Bailliage and L. Mazaré, “Using unification for opacity properties,”in Proceedings of the Workshop on Issues in the Theory of Security(WITS’04), 2004, pp. 165–176.

TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, VOL. ?, NO. ?, ?? ????

[2] J. Bryans, M. Kounty, and P. Ryan, “Modelling opacity using petri nets,”
Electronic Notes in Theoretical Computer Science, vol. 121, pp. 101–
115, 2005.
[3] Y. Tong, Z. Li, C. Seatzu, and A. Giua, “Verification of state-based
opacity using petri nets,” IEEE Transactions on Automatic Control,
vol. 62, no. 6, pp. 2823–2837, 2017.
[4] J. Bryans, M. Koutny, L. Mazaré, and P. Ryan, “Opacity generalised totransition systems,” International Journal of Information Security, vol. 7,
no. 6, pp. 421–435, 2008.
[5] A. Saboori and C. N. Hadjicostis, “Verification of infinite-step opacity
and complexity considerations,” IEEE Transactions on Automatic Control, vol. 57, no. 5, pp. 1265–1269, 2012.
[6] A. Saboori and C. N. Hadjicostis, “Verification of initial-state opacity insecurity applications of discrete event systems,” Information Sciences,vol. 246, pp. 115–132, 2013.
[7] A. Saboori and C. N. Hadjicostis, “Verification of k-step opacity andanalysis of its complexity,” in Proceedings of the 48h IEEE Conferenceon Decision and Control (CDC) held jointly with 2009 28th ChineseControl Conference, 2009, pp. 205–210.
[8] A. Saboori and C. N. Hadjicostis, “Opacity-enforcing supervisory strategies via state estimator constructions,” IEEE Transactions on AutomaticControl, vol. 57, no. 5, pp. 1155–1165, 2012.
[9] C. Keroglou and C. Hadjicostis, “Initial state opacity in stochastic
des,” 2013 IEEE 18th Conference on Emerging Technologies & Factory
Automation (ETFA), pp. 1–8, 2013.
[10] B. Bérard, K. Chatterjee, and N. Sznajder, “Probabilistic opacity formarkov decision processes,” Information Processing Letters, vol. 115,
no. 1, pp. 52–59, 2015.
[11] B. Bérard, J. Mullins, and M. Sassolas, “Quantifying opacity,” 2010
Seventh International Conference on the Quantitative Evaluation of
Systems, pp. 263–272, 2010.
[12] M. Ibrahim, J. Chen, and R. Kumar, “Secrecy in stochastic discrete event
systems,” in Proceedings of the 11th IEEE International Conference on
Networking, Sensing and Control, 2014, pp. 48–53.
[13] F. Cassez, “The dark side of timed opacity,” in Advances in Information
Security and Assurance, 2009.
[14] C. Dima, “Real-time automata,” Journal of Automata, Languages andCombinatorics, vol. 6, no. 1, pp. 3–24, 2001.
[15] J. Hopcroft, R. Motwani, and J. Ullman, Introduction to automata theory,
languages, and computation - international edition (2. ed). AddisonWesley, 2003.
[16] S. C. Kleene, “Representation of events in nerve nets and finite automata,” in Automata Studies. Princeton, NJ: Princeton University Press,
1956, pp. 3–41.
[17] R. W. Floyd, “Algorithm 97: Shortest path,” Communications of theACM, vol. 5, no. 6, p. 345, 1962.
[18] S. Warshall, “A theorem on boolean matrices,” Journal of the ACM,
vol. 9, no. 1, pp. 11–12, 1962.
[19] P. Borwein and T. Erdélyi, Polynomials and Polynomial Inequalities.
Springer-Verlag, 1995.
[20] G. Gardey, J. Mullins, and O. Roux, “Non-interference control synthesis
for security timed automata,” Electr. Notes Theor. Comput. Sci., vol. 180,
no. 1, pp. 35–53, 2007.
[21] D. Denning and G. Sacco, “Timestamps in key distribution protocols,”
Commun. ACM, vol. 24, no. 8, pp. 533–536, 1981.
[22] J. Kohl and B. C. Neuman, “The Kerberos network authentication
service (V5),” RFC, vol. 1510, pp. 1–112, 1993.
[23] J. He, “From CSP to hybrid systems,” in A Classical Mind, Essays in
Honour of C.A.R. Hoare. Prentice Hall International (UK) Ltd., 1994,
pp. 171–189.
[24] C. Zhou, J. Wang, and A. P. Ravn, “A formal description of hybrid
systems,” in Hybrid systems, LNCS 1066, 1996, pp. 511–530.
[25] N. Zhan, S. Wang, and H. Zhao, Formal Verification of Simulink/Stateflow Diagrams, 2017.
[26] J. Liu, J. Lv, Z. Quan, N. Zhan, H. Zhao, C. Zhou, and L. Zou, “Acalculus for hybrid CSP,” in APLAS’10, ser. LNCS, vol. 6461, 2010,
pp. 1–15.

12Lingtai Wang received her B.Sc. degree in information and computation sciences from Peking
University in 2015. Currently, she is a Ph.D student
at the Institute of Software Chinese Academy of
Sciences, and University of Chinese Academy of
Sciences. Her research interests include modelingand verification of hybrid systems.

Naijun Zhan received his B.Sc. in mathematics
and M.Sc. in computer science both from Nanjing
University, Nanjing, China, in 1993 and in 1996
respectively, and Ph.D. degree in computer sciencefrom Institute of Software, Chinese Academy of
Sciences, Beijing, China.
He worked at Faculty of Mathematics and Information, University of Mannheim, Mannheim, Germany, as a research fellow, from 2001 to 2004.
Since then he joined Institute of Software, Chinese
Academy of Sciences, Beijing, China, as an associate research professor, and was promoted to be a full research professor in2008. His research interests include real-time, embedded and hybrid systems,
program verification, concurrent computation models, and modal and temporal
logics.

Jie An received his Bachelor degree in software
engineering from Tongji University in 2012, andhis Master degree in software engineering from
Tongji University in 2015. Currently, he is a PhD
Candidate in School of Software Engineering, Tongji
University. From 2016 to now, he is also an intern
PhD student in State Key Laboratory for Computer
Science, Institute of Software Chinese Academy of
Sciences. His research interests include formal verification, embedded software verification and model
learning.