K-corruption intermittent attacks for violating the codiagnosability

1
K-Co up ion In e mi en A acks o Viola ing he
Codiagnosabili y
Ruo ian Liu, Membe , IEEE, Yihui Hu, Agos ino Ma cello Mangini, Senio Membe , IEEE, and
Ma ia Pia Fan i, Fellow, IEEE
Abs ac —In his wo k, we add ess he codiagnosabili y analy-
sis p oblem o a ne wo ked disc e e e en sys em unde malicious
a acks. The conside ed sys em is modeled by a labeled Pe i ne
and is moni o ed by a se ies o si es, in which each si e possesses
i s own se o senso s, wi hou equi ing communica ion among
si es o o any coo dina o s. A ne is said o be codiagnosable wi h
espec o a aul i a leas one si e could deduce he occu ence
o his aul wi hin ini e s eps. In his con ex , we ocus on
a ype o malicious a ack ha is called s eal hy in e mi en
eplacemen a ack. The s eal hiness demands ha he co up ed
obse a ions should be consis en wi h he sys em’s no mal
beha io , while he in e mi en eplacemen se ing en ails ha
he eplaced ansi ion labels mus be eco e ed wi hin a bounded
o consecu i e co up ed obse a ions (called as K-co up ion
in e mi en a ack). Pa icula ly, he e exis s a coo dina ion
be ween a acke s ha a e sepa a ely e ec ed on di e en si es,
which holds he same co up ed obse a ion o each common
ansi ion unde a acks. F om an a acke iewpoin , his wo k
aims o design K-co up ion in e mi en a acks o iola ing
he codiagnosabili y o sys ems. Fo his pu pose, we p opose an
a ack au oma on o analyze K-co up ion in e mi en a ack o
each si e, and build a new s uc u e called comple e a ack g aph
ha is used o analyze all he po en ial a acked pa hs. Finally,
an algo i hm is in e ed o ob ain he K-co up ion in e mi en
a acks, and examples a e gi en o show he p oposed a ack
s a egy.
Index Te ms—Disc e e e en sys em, decen alized s uc u e,
Pe i ne , in e mi en a ack, codiagnosabili y.
NOMENCLATURE
NPe i ne .
M0Ini ial ma king o a Pe i ne .
NLabeled Pe i ne (LPN).
TuSe o unobse able ansi ions.
ToSe o obse able ansi ions.
T Se o aul ansi ions.
T eg Se o egula unobse able ansi ions.
T ,a Se o egula unobse able ansi ions ha can be
a acked.
This wo k was suppo ed in pa by he IN2CCAM p ojec ha has
ecei ed unding om he Eu opean Union’s Ho izon Eu ope esea ch and
inno a ion p og amme unde g an ag eemen No 101076791, and he Na u al
Science Basic Resea ch P og am o Shaanxi P o ince unde G an 2024JC-
YBQN-0669. This manusc ip e lec s only he au ho s’ iews and opinions,
nei he he Eu opean Union no he Eu opean Commission can be conside ed
esponsible o hem. (Co esponding au ho : Ruo ian Liu.)
Ruo ian Liu, Agos ino Ma cello Mangini, and Ma ia Pia Fan i a e wi h he
Depa men o Elec ical and In o ma ion Enginee ing, Poly echnic Uni e si y
o Ba i, 70125 Ba i, I aly (e-mails: { uo ian.liu, agos inoma cello.mangini,
ma iapia. an i}@poliba.i ).
Yihui Hu is wi h he School o Au oma ion, Xi’an Uni e si y o Pos s and
Telecommunica ions, 710121 Xi’an, China (e-mail: [email p o ec ed]).
T ,u Se o egula unobse able ansi ions ha canno be
a acked.
π(σ)Pa ikh ec o o σ.
lLabeling unc ion.
ljLabeling unc ion o si e j.
ΣE en se .
ΣjE en se o si e j.
P ,u(σ)P ojec ion o σo e T ,u.
GeEx ended basis eachabili y g aph (EBRG).
JSe o si es in LPN sys em.
MdDead ma king.
Gεε-BRG: enhanced e sion o EBRG.
Gj
ε,n Non ailu e ε-BRG o si e j.
Uεε-un olded e i ie .
AA ack s uc u e.
AjA ack s uc u e o si e j.
ΣAj( )Se o eplaced labels associa ed wi h in e ms o
Aj.
Tj
a,s A ackable ansi ions wi h espec o Aj.
lj
aModi ied labeling unc ion o si e j.
AjReplacemen a ack o si e j.
AA ack uple.
KjMaximum alue o consecu i e co up ed obse a ion
o si e j.
KRow ec o whose j- h elemen is Kj.
Tj
aSe o a ackable ansi ions ha a e associa ed wi h
di e en labels wi h espec o si e j.
Tj
na Se o a ackable ansi ions ha hold hei o iginal
labels wi h espec o si e j.
IjInse ion unc ion o si e j.
I−1
jIn e se o inse ion unc ion.
Pj
a,na P ojec ion o e Tj
a∪Tj
na.
P ,j
a,na P ojec ion o e Tj
a∪Tj
na ∪T .
ΦjK-co up ion in e mi en a ack unc ion o si e j.
∆jA ack au oma on o si e j.
UcComple e a ack g aph.
Pj
a,na P ojec ion o e T∪Tj
a∪Tj
na o si e j.
P
a,na P ojec ion o e T∪Ta∪Tna.
lAj( )Se o obse a ions when i es wi h espec o Aj.
I. INTRODUCTION
Cybe physical sys ems (CPSs) in eg a e sensing, con ol
and ne wo king in o physical p ocesses, in which ne wo k
communica ion makes he sys em ulne able o a ious ne -
wo k a acks, such as senso eading co up ion and ac ua o
command al e a ion [1]–[4]. Such a ack scena ios o CPSs
2
ha e a ac ed much a en ion in he communi y o disc e e
e en sys ems (DESs): mainly conce ning he p oblems o
a ack de ec ion [5]–[7], a ack syn hesis [8]–[13], s a e es-
ima ion [14], [15]. This wo k ocuses on he a ack syn hesis
p oblem o iola ing he codiagnosabili y in DESs.
Diagnosabili y is a sys em p ope y de e mining whe he
he occu ence o a aul can be de ec ed wi hin ini e s eps,
and has been s udied in he amewo k o au oma a [16]–
[18] and Pe i ne s [19]–[24]. In p ac ice, many la ge complex
sys ems a e moni o ed by a se o si es ha conside a iable
communica ion delays and e o s when ansmi ing diagnos ic
in o ma ion om di e en si es o a coo dina o . I is impossi-
ble o e y cos ly o collec all da a a a cen al s a ion. Thus,
he in o ma ion s uc u e o he sys em is na u ally conside ed
o be decen alized, and in p ac ice, he e exis wo main
aspec s o he decen alized se ing. One is abou he no ion o
decen alized diagnosis in ol ing communica ion among si es,
such as [25]–[27]. The o he is he concep o decen alized
diagnosis, which does no in ol e communica ion among si es.
The no ion o codiagnosabili y equi es ha he occu ence o
any aul can be de ec ed by a leas one si e using i s own
obse a ions o he sys em execu ion wi hin a bounded delay
[28]–[31]. To in es iga e he codiagnosabili y o he sys em,
his wo k conside s he P o ocol 3 in [32] ha does no equi e
any coo dina ion be ween si es.
The idea o his wo k is inspi ed by ecen s udies [29], [33]
ha deal wi h he codiagnosabili y analysis o opaci y en o ce-
men p oblem by elabeling ansi ions o inse ing ansi ion
labels when no ac i e a ack exis s. Meanwhile, some s ud-
ies [34], [35] ackle he p oblem o obus codiagnosabili y
agains senso ailu es, gua an eeing he sa e y and eliabili y
o he sys ems. He e, we in es iga e he con a y aspec s o
codiagnosabili y en o cemen [29] and obus codiagnosabili y
[34]–[36] om an a acke iewpoin . I is mo i a ed by he
necessi y o design wi h an a ack policy o iola ing he
codiagnosabili y, which conceals he occu ence o c i ical
aul s o comp omise he sys ems. Fo ins ance, an in ude a -
emp s o dis up he bank secu i y sys em by manipula ing he
senso eadings in he ne wo k communica ion componen s.
This manipula ion is in ended o e ade he sys em’s abili y o
de ec aul s o igge ale s, hus ende ing he sys em non-
diagnosable unde such an a ack. As we know, o he wo ks
in es iga ing he a ack syn hesis p oblem ocus on di e en
a ack objec i es. Fo example, he iola ion o sa e y, i.e., all
in e nal s ings gene a ed by he sys em a e legal, is conside ed
in [8], [12], while he iola ion o opaci y is s udied in [13].
In he a o emen ioned a ack s udies, he sys em obse a ion
may be co up ed by he a acke s con inuously o comp omise
he sys em, whe e he p oblem o in e mi en co up ion is
no conside ed in DESs. In ac , in e mi en a acks [37]
equi e lowe ene gy cos compa ed o con inuous a acks. On
he o he hand, a acke s exploi in e mi en ulne abili ies o
he sys ems, like came a down ime du ing secu i y pe sonnel
shi s o main enance pe iods. These in e mi en ulne abili-
ies esul in dis up ions in he digi al ail, making de ec ion
mo e challenging. In his wo k, we o mula e in e mi en
a ack syn hesis p oblem in DESs unde he decen alized
amewo k, whe e he conside ed a ack could las o a mos
a ce ain pe iod o ime. To do so, we assume ha a e a
bounded numbe o consecu i e co up ed obse a ions unde
he in e mi en a acks, he eplaced ansi ion label mus
be eco e ed, which leads o a new no ion o K-co up ion
in e mi en a ack. Pa icula ly, in a decen alized s uc u e,
gi en a ansi ion sequence and a si e j, i he ansi ions ha e
been eplaced a gi en ce ain Kj imes consecu i ely unde
he a acks, hen he nex occu ence o a ansi ion ha can
be a acked should hold i s o iginal label.
No e ha ou in e mi en se ing is inspi ed by he wo k
[35] ha ocuses on he obus codiagnosabili y e i ica ion
agains in e mi en o ansien senso ailu es. Howe e , wo
main di e ences exis be ween ou s udy and he wo k [35]:
i) in e ms o p oblem o mula ion and solu ion, we aim o
syn hesize an in e mi en a ack s a egy o iola ing he
codiagnosabili y, while pape [35] in es iga es he p oblem o
obus codiagnosabili y e i ica ion, hus yielding o di e en
solu ions; ii) in e ms o o malism, he p oposed p oblem is
newly add essed in he labeled Pe i ne (LPN) o malism,
whe e he echniques o basis ma king and linea algeb a a e
used o a oid an exhaus i e compu a ion o all ma kings.
In addi ion, wo k [36] p oposes a uni o m app oach o
diagnosis in DESs subjec o un eliable senso s, employing
linea empo al logic echniques. Such a amewo k allows
o he o mula ion and inclusion o diagnosabili y e i ica ion
p oblems in e ms o K-loss obse a ion se ing, bu i is no
applied o he en o cemen o iola ion o diagnosabili y. I is
no ewo hy ha he conside ed a ack scena io may comp o-
mise obse a ions by inse ing, eplacing, o emo ing pa ial
obse a ions wi hin he sys em. Senso ailu e ypically esul s
in inco ec o missing obse a ions. Ou wo k complemen s
exis ing esea ch on a ack syn hesis p oblems in DESs, wi h
a pa icula emphasis on add essing in e mi en a acks. By
de ising such an a ack s a egy, ou aim is o enable enginee s
o de ec po en ial ulne abili ies om he pe spec i e o an
a acke .
To ackle he a ack syn hesis p oblem, he e a e mainly se -
e al app oaches in he li e a u e. The i s ype o app oaches
[12], [13] employs a disc e e s uc u e o model he game-like
in e ac ion be ween he supe iso and he a acke . Such a
game s uc u e inco po a es all possible a acks. The second
ype o app oaches ans o ms he a ack syn hesis p oblem
in o he supe iso syn hesis p oblem [8], [9]. Unlike exis ing
app oaches, we in oduce a labeling unc ion o model an
a ack, o making a sys em non-codiagnosable by using an
ε-un olded e i ie s uc u e. Speci ically, an a ack syn hesis
equi es he exis ence o a ype o pa h called elemen a y
unsound pa h ha iola es he codiagnosabili y. The classic
e i ie [29] can only upda e s a es when consecu i e ansi ion
pai s ha e he same obse a ion, hus i is unable o gene a e
elemen a y unsound pa hs. In addi ion, he classic e i ie
canno be applied o in e mi en a ack syn hesis. To sol e
hese issues, we de elop a new s uc u e called comple e
a ack g aph wi h he ollowing ad an ages: (i) i emo es
he same obse a ion condi ion o he consecu i e ansi ion
pai ; (ii) i in eg a es he p oposed a ack au oma on, such
ha all he po en ial a acked pa hs limi ed o Kconsecu i e
co up ions a e lis ed. Mo eo e , unlike he app oach in [12],
3
which achie es s eal hiness h ough s a e p uning, his s udy
iden i ies s eal hy a acks by analyzing he co up ed beha io .
La e on, o apply he concep o codiagnosabili y wi hou
deadlock- eeness assump ion, we add a sel -loop labeled wi h
he emp y s ing ε o each de e mined dead ma king. The
o igin o his concep is de i ed om he esea ch [31] whe e
a e i ie s uc u e is p oposed o de e mine he diagnosabili y
o a sys em wi h deadlocks. Howe e , unlike he wo k in [31],
his s udy p ima ily ocuses on he design o an a ack s a egy
iola ing he codiagnosabili y. The main con ibu ion o his
pape is summa ized as ollows:
•We i s o mula e he K-co up ion in e mi en a ack
syn hesis p oblem o a sys em modeled by LPN in he
decen alized amewo k. To ou knowledge, his issue
has no been p e iously conside ed in DESs.
•We de elop a new s uc u e called a comple e a ack
g aph ha con ains all he a acked pa hs limi ed o
Kconsecu i e co up ions, based on he no ion o ex-
ended basis ma king and a ack au oma on. Then some
condi ions a e gi en o de e mine he po en ial a acked
pa h ha could be a acked in o a p ede ined elemen a y
unsound pa h leading o he iola ion o codiagnosabili y.
•We p opose an algo i hm o ob ain K-co up ion in e -
mi en a acks o iola ing he codiagnosabili y. Pa icu-
la ly, a coo dina ion be ween a acke s sepa a ely e ec ed
on di e en si es holds he same co up ed obse a ion
o each common ansi ion. Mo eo e , we gua an ee
he s eal hiness o a acks, i.e., i s occu ence canno
be dis inguished om he sys em beha io . To his aim,
i is equi ed ha he se o co up ed obse a ions is
con ained in he se o obse a ions wi hou a acks.
The emainde o his wo k is o ganized as ollows. Sec ion
II p esen s basic de ini ions o LPNs as well as he no ion o
ex ended basis eachabili y g aph. In Sec ion III, we p opose
an ex ended un olded e i ie o codiagnosabili y analysis,
and hen de ine he s eal hy eplacemen and in e mi en (in
e ms o Kconsecu i e co up ed obse a ions) a ack. The
add essed codiagnosabili y analysis p oblem is o mula ed in
he LPNs unde he K-in e mi en a ack. Sec ion IV p oposes
an app oach o ob ain a acks o iola ing he codiagnosabil-
i y. Finally, conclusions a e summa ized in Sec ion V.
II. PRELIMINARIES
A. Pe i ne
Le Nbe he se o non-nega i e in ege s. A Pe i ne is
de ined as a ou - uple N= (P, T, P e, Pos ), whe e P=
{p1, ..., pm}is a se o m∈Nplaces, T={ 1, ..., n}is a
se o n∈N ansi ions wi h P∪T=∅and P∩T=∅,
P e :P×T→Nand Pos :P×T→Na e he p e- and
pos -incidence ma ices, espec i ely, deno ing he weigh s o
he a cs om places o ansi ions and ansi ions o places,
which ix he s uc u e o a ne and a e ep esen ed as ma ices
in Nm×n. The incidence ma ix o a ne is de ined by C=
Pos −P e. A Pe i ne is said o be acyclic i he e is no
di ec ed cycle.
A ma king is a mapping M:P→N ha assigns o a place
o a Pe i ne a non-nega i e in ege o okens, g aphically
deno ed by black do s. M(pi)is he numbe o okens in place
pia a ma king M. A Pe i ne sys em ⟨N, M0⟩is a ne N
wi h an ini ial ma king M0. A ansi ion ∈Tis enabled
a a ma king Mi M≥P e(·, )and may i e yielding a
ma king M′=M+C(·, ). We w i e M[σ⟩ o deno e ha
a ansi ion sequence σ= 1 2· · · i∈T∗is enabled a M,
and M[σ⟩M′ o deno e ha he i ing o σyields M′. When
σand σ′a e wo sequences, σσ′s ands o he conca ena ion
o σand σ′. The Pa ikh ec o o σis deno ed by π(σ)and
maps a ansi ion ∈T o he numbe o occu ences o in
σ. The ca dinali y o he se (·)is deno ed by |(·)|.
A ma king Mis eachable in ⟨N, M0⟩i he e exis s a
i ing sequence σ∈T∗such ha M0[σ⟩M. The se o all
ma kings eachable om M0, deno ed by R(N, M0), de ines
he eachabili y se o ⟨N, M0⟩, i.e., R(N, M0) = {M∈Nm|
M0[σ⟩M}. The se o ansi ion sequences enabled a he ini-
ial ma king M0is de ined as L(N, M0) = {σ∈T∗|M0[σ⟩}.
Gi en a ansi ion sequence se H⊆L(N, M0),we deno e by
H/σ he pos ansi ion sequence o a sequence σ∈H, i.e.,
H/σ ={σ′∈L(N, M0)|σσ′∈H}. A ma king Mis dead i
he e is no any ansi ion enabled a M. A ne sys em ⟨N, M0⟩
is said o be: bounded i he e exis s an in ege k∈Nsuch
ha o all M∈R(N, M0)and o all pi∈P, M(pi)≤k
holds; deadlock- ee i o all M∈R(N, M0),Mis no dead.
Gi en a Pe i ne N= (P, T, P e, Pos )and a subse o
ansi ions T′⊆T, he T′-induced subne o Nis a Pe i
ne N′= (P, T′, P e′, Pos ′), whe e P e′and Pos ′a e he
es ic ions o P e and Pos o P×T′, espec i ely, i.e., he
ne N′is ob ained by emo ing all he ansi ions in T T′
om N.
B. Labeled Pe i ne
Gi en a Pe i ne N= (P, T, P e, Pos )and an e en
se Σ, a labeling unc ion l:T→Σ∪ {ε}= Σεassigns
o a ansi ion ei he a symbol om he e en se Σo he
emp y s ing symbol ε. A labeled Pe i ne (LPN) sys em
S=⟨N, Σ, l, M0⟩is a Pe i ne sys em ⟨N, M0⟩wi h a
labeling unc ion land an e en se Σ. A ansi ion is said
o be unobse able o silen i i is associa ed wi h he emp y
s ing ε, i.e., l( ) = ε. The se o unobse able ansi ions is
deno ed by Tu={ ∈T|l( ) = ε}. The o he ansi ions
labeled wi h e en s om Σa e called obse able ansi ions,
deno ed as To={ ∈T|l( )∈Σ}. Hence, he se o
ansi ions Tcan be di ided in o wo disjoin se s Toand Tu
wi h T=To∪Tu. Fu he mo e, he se Tucan be di ided
in o wo disjoin se s T and T eg wi h Tu=T ∪T eg,
whe e T and T eg deno e he se s o aul ansi ions and
egula unobse able ansi ions, espec i ely. The se T can
be u he pa i ioned in o classes Ti
, whe e i= 1, . . . , .
Fo simplici y, his wo k conside s an LPN wi h a single aul
class, i.e., T =T1
. Ne e heless, he p oposed app oach
could be easily ex ended o he ne s wi h mul iple aul classes
as p esen ed in [29]. In addi ion, om a p ac ical poin o iew,
we pa i ion he se T eg in o wo disjoin se s T ,a and T ,u
wi h T eg =T ,a ∪T ,u, whe e T ,a ( esp., T ,u) deno es he
se o egula unobse able ansi ions ha can ( esp. canno )
be a acked.
4
The labeling unc ion could be ex ended o a ansi ion
sequence σ= 1 2. . . isuch ha ω=l(σ) = l( 1)l( 2)
. . . l( i),which is called an obse a ion co esponding o he
sequence σ. Gi en an LPN sys em ⟨N, Σ, l, M0⟩, we de ine
l−1(ω)as he se o all ansi ion sequences consis en wi h
ω∈Σ∗
ε,i.e., l−1(ω) = {σ∈L(N, M0)|l(σ) = ω}. No e ha
he obse a ion ω=ε·εh=ε, h ∈N. The language gene a ed
by an LPN sys em Sis de ined as L(N, M0) = {ω∈Σ∗
ε|
∃σ∈L(N, M0) : ω=l(σ)},i.e., he language L(N, M0)is a
se o obse a ions co esponding o he ansi ion sequences
in L(N, M0).
C. Ex ended basis eachabili y g aph
In his subsec ion, we ecall necessa y no ions o he ex-
ended basis ma kings in [38]. Gi e a ansi ion sequence
σ∈T∗, we deno e by P ,u(σ) he p ojec ion o σo e T ,u.
Mo eo e , he es ic ion o incidence ma ix Co an LPN
sys em o T ,u is deno ed by C ,u.
De ini ion 2.1 ( [38]): Gi en a ma king M∈R(N, M0)
and a ansi ion ∈To∪T ∪T ,a o an LPN sys em
S=⟨N, Σ, l, M0⟩, he se o explana ions o a Mis
de ined by Σ(M, ) = {σ∈T∗
,u |M[σ⟩M′, M′[ ⟩},and
he se o explana ion ec o s o a Mis deno ed as
Y(M, ) = {π(σ)∈N|T ,u||σ∈Σ(M, )}. In addi ion,
he minimal explana ion ec o is de ined as Ymin(M, ) =
{π(σ)∈Y(M, )|∄π(σ′)∈Y(M, ) : π(σ′)⪇π(σ)}.♢
The se o ex ended basis ma kings, deno ed as Xe, is
ecu si ely compu ed as ollows:
•M0∈Xe;
•I M∈Xe, hen o each ∈To∪T ,a ∪T , y =π(σ)∈
Ymin(M, ),
(M′=M+C ,u ·y+C(·, )) ⇒(M′∈Xe).
Gi en an LPN sys em S=⟨N, Σ, l, M0⟩, he ex ended basis
eachabili y g aph (EBRG) o Sis a nonde e minis ic ini e
s a e au oma on Ge= (Xe, E, δ, M0), whe e Xeis he se o
s a es (i.e., ex ended basis ma kings); E⊆(To×Σ) ∪[(T ∪
T ,a)×ε]is he se o e en labels; δ⊆Xe×Σε×Xeis he
ansi ion ela ion; and M0is he ini ial s a e. In pa icula ,
he ansi ion ela ion (M, e, M′)∈δwhe e e= (l( )) ∈
To×Σo e= (ε)∈(T ∪T ,a)×εi and only i ∃y∈
Ymin(M, ), M′=M+C ,u ·y+C(·, ).
III. CODIAGNOSABILITY ANALYSIS PROBLEM UNDER
MALICIOUS ATTACKS
In his wo k, we conside ha he sys em is moni o ed by
a se o si es J={1,2, . . . , ξ}associa ed wi h hei own
obse able e en se s, whe e ξis equal o he numbe o si es.
Each ansi ion in Tois assumed o be obse able by a leas
one si e, i.e., To=Sj∈J Tj
o, whe e Tj
o⊆Tois he se o
ansi ions ha a e obse able by si e j. The e en se o si e
jis Σj⊆Σ, and
lj( ) = l( )i l( )∈Σj,
εo he wise.(1)
deno es he labeling unc ion o si e j.
A. Codiagnosabili y analysis based on ε-un olded e i ie
The codiagnosabili y analysis app oach p oposed in [29]
elies on he assump ion ha he ne sys em is deadlock-
ee when using he un olded e i ie . Ne e heless, his wo k
elimina es he assump ion by in oducing a sel -loop encoded
wi h an addi ional unobse able ansi ion u(labeled by
he emp y s ing εand canno be a acked) o each dead
ma king. Consequen ly, he esul ing ansi ion sequence se
could be de ined as Lω(N, M0) = L(N, M0)∪ {σ ∗
u| ∃Md∈
R(N, M0),∄ ∈T, Md[ ⟩, M0[σ⟩Md}. In he ollowing i is
assumed ha uis included in he se T, i.e., u∈T. The
de ini ion o codiagnosabili y in LPN sys ems wi hou he
deadlock- eeness assump ion can be gi en in he ollowing
pa . He e, we deno e by ψ(T ) = {σ ∈Lω(N, M0)|
σ∈T∗, ∈T } he se o i ing ansi ion sequences in
Lω(N, M0) ha end wi h a aul ansi ion ∈T .
De ini ion 3.1 (Codiagnosabili y): An LPN sys em ⟨N, Σ,
l, M0⟩, ha is moni o ed by a se o si es J={1,2, . . . , ξ},
is codiagnosable wi h espec o he se o aul ansi ions T
i and only i
∀σ′∈ψ(T ),∃h∈N,∀σ′′ ∈Lω(N, M0)/σ′,|σ′′| ≥ h
=⇒ ∃j∈ J ,∀σ∈l−1
j(lj(σ′σ′′)),∃ ∈T : ∈σ.
♢
This de ini ion implies ha an LPN sys em is codiagnosable
conce ning T i each aul in T can be de ec ed by a leas
one si e j∈ J .
To de e mine he dead ma kings o he LPN sys em based
on EBRG, we should i s e i y i each ex ended basis
ma king is dead o each ma king subse , eached by i ing
he unobse able ansi ions ∈T ,u om an ex ended basis
ma king, con ains dead ma kings. This e i ica ion me hod is
simila o he one s a ed by p oposi ion in [39] ia eplacing
he T eg as T ,u. He e we deno e by R ,u(M) = {M′|
M[σ ,u⟩M′, σ ,u ∈T∗
,u}as he se o ma kings ob ained
by i ing unobse able sequences whose ansi ions belong o
T ,u.
P oposi ion 3.2 ( [39]): Gi en an LPN sys em ⟨N, Σ, l, M0⟩
and a ma king M, he e exis s a leas one dead ma king in
R ,u(M)i and only i he ollowing linea in ege cons ain
D(M)is easible:
D(M) = 


Md=M+C ,u ·y≥0,
y∈NT ,u ,
ρ(Md).
(2)
whe e ρ(Md) : V ∈T(Wp∈• Md(p)≤P e(p, )−1).♢
In plain wo ds, ρ(Md)is used o deno e he se o dead
ma kings ha can be desc ibed by a se o linea equali ies
cha ac e izing he enabling condi ions o ansi ions. Mo e-
o e , ema k ha he dead ma kings in R ,u(Mi)may no be
unique. Subsequen ly, we p esen a new s uc u e called ε-
BRG ha is an augmen ed basis eachabili y g aph whe e a
sel -loop labeled wi h u(ε)is added o each ma king Md
a which some unobse able ansi ions can i e such ha
a dead ma king is eached. We deno e by ⟨N′,Σ, l′, M0⟩
he non ailu e subse o ⟨N, Σ, l, M0⟩(o T′-induced subne
o N), whe e T′=T T .L(N′, M0)is he ansi ion
5
sequences o med wi h he sequences o L(N, M0)wi hou
aul ansi ions, and l′is equal o l es ic ed o T T .
Then wo eachabili y g aphs a e illus a ed using he no ion
o ex ended basis ma kings.
De ini ion 3.3: Gi en an LPN sys em S=⟨N, Σ, l, M0⟩, le
Ge= (Xe, E, δ, M0)be he EBRG. The ε-BRG o Sis a non-
de e minis ic ini e s a e au oma on Gε= (Xε, Eε, δε, M0),
whe e:
•Xε=Xeis he se o s a es.
•Eε⊆E∪ { u(ε)}is he e en labels.
• he ansi ion ela ion δεis de ined as ollows:
δε=δ∪ {(Mi, u(ε), Mi)|D(Mi)is easible}.
•M0is he ini ial s a e. ♢
A non ailu e ε-BRG wi h espec o si e j∈ J , deno ed
by Gj
ε,n = (Xj
ε,n, Ej
ε,n, δj
ε,n, M0), is he ε-BRG de i ed
om ⟨N′,Σ, l′, M0⟩ ollowing he assump ion ha he se o
obse able ansi ions is equal o Tj
o∪T ,a.
Rema k 3.4: Wi h a sligh modi ica ion o q-BRG de ini ion
in [39] ha in oduces an obse able quiescen e en q o
cha ac e ize he exis ence o deadlocks in he sys em, we use
unobse able s ing ε o ep esen ha he sys em may each a
dead ma king wi hou any ou pu obse a ion. Based on he ε-
BRG s uc u e, an a ack s a egy is hen de eloped o iola e
he codiagnosabili y.
Example 1: Gi en an LPN sys em Sas depic ed in Fig. 1,
i s ex ended basis ma kings a e lis ed in Table I. Pa icula ly,
he e exis s a dead ma king Md=M3, whe e he oken en e s
place p7such ha no ansi ion is enabled.
!1"
#2
%1
!2!3!4
#(
#1
)
#*
+
#,
#-
#.
#//
#/0 #1
#/2 #/*
#/(
"
3"
!11 !12
!.
!1
#4
!4
!/0
!,
!-
Fig. 1. LPN sys em S=⟨N, Σ, l, M0⟩wi h a dead ma king.
TABLE I
THE EXTENDED BASIS MARKING OF LPN SYSTEM IN FIG.1.
M0[100000000000]T
M1[001000000000]T
M2[000010000000]T
M3[000000100000]T
M4[000000010000]T
M5[000000001000]T
M6[000000000100]T
M7[000000000010]T
M8[000000000001]T
Assume ha he LPN sys em Sis moni o ed by wo si es
wi h Σ1={a, b, d}and Σ2={a, c, d}. By De ini ion 3.3,
i s ε-BRG and he non ailu e ε-BRGs a e shown in Fig. 2. As
depic ed in Fig.2, once a dead ma king M3is eached, we add
a sel -loop encoded wi h an unobse able ansi ion u ha is
labeled wi h ε.♢
!"
!#
!$
!%
&%(() &*(+)
!,!*
&#%(-)
&##(.) &/(.)
&0(()
!1
!2!/
&#$(()
&#*(.)
&3(.)
&*(+)
&%(()
&2(4)
(a)
!"
!#
!$
%$(')
%)(*)
!)
%+(,)
%-(')
!.
%)(*)
%$(')
%+(,)
!/
%0(,)
%1(2)
%1(2)
(b)
!"
!#
!$
!%
&'())
&+(,)
&-())
&.(/)
&0(,)
&0(,)
&.(/)
!1
&'())
(c)
Fig. 2. (a) ε-BRG o LPN sys em as shown in Fig. 1. (b) non ailu e ε-BRG
o si e 1. (c) non ailu e ε-BRG o si e 2.
The un olded e i ie p oposed in [29] is used o codi-
agnosabili y analysis in a decen alized amewo k, which is
cons uc ed by he pa allel composi ion [40] o he EBRG
and all he non ailu e EBRGs. In he ollowing, an ex ended
un olded e i ie applying o a mo e gene al ne ha con ains
deadlocks is de ined based on he no ion o he ε-BRGs.
De ini ion 3.5: Gi en an LPN sys em S ha is moni o ed
by a se o si es J={1,2, . . . , ξ}, i s ε-BRG is Gεand
he j- h non ailu e ε-BRG is Gj
ε,n. The ε-un olded e i ie
(ε-UV) Uε= (XU
ε, EU
ε, δU
ε, MU
0)is a ini e s a e au oma on
cons uc ed by he pa allel composi ion o he ε-BRG and all
he non ailu e ε-BRGs. ♢
Fo he sake o simplici y, only wo local si es moni o ing
he LPN sys em a e conside ed in he ollowing discussion. In
de ail, a node (M, α;M′, M′′)in he ε-UV is called an α-s a e,
in which αcan be ei he N o ep esen he no mal beha io
o sys em wi hou he occu ence o aul om he ini ial s a e
o his one, o F o deno e he occu ence o aul y beha io
o sys em. Fu he mo e, in a pa h o Uε, he s a e is agged as
“duplica e” i i al eady exis s om he oo o Uε, and i is
called a duplica e α-s a e. The ansi ions o ε-UV a e uples
(γ, γ1, γ2)whe e: (1) γei he co esponds o a ansi ion in
he ε-BRG Gεo o ε(i.e., ε ep esen s he emp y s ing);
(2) γ1(γ2) ei he co esponds o a ansi ion in he non ailu e
ε-BRG G1
ε,n (G2
ε,n) o o ε.
The ollowing de ini ion p esen s he no ion o elemen a y

6
unsound pa h ha leads o he iola ion o codiagnosabili y.
P ecisely, he exis ence o his ype o pa h shows ha , o
each si e, wo a bi a ily long ansi ion sequences o LPN
sys em ha e he same obse a ion and one o hem con ains
he aul ansi ion, such ha he occu ence o he aul canno
be de ec ed in a ini e numbe o s eps. Gi en an au oma on
G, we w i e Mσ
−→
GM′ o deno e ha M′is eached in G
om Mwi h a sequence σ.
De ini ion 3.6: Gi en an ε-un olded e i ie Uε= (XU
ε, EU
ε,
δU
ε, MU
0), a sequence eσ= (γ1, γ1
1, γ2
1)(γ2, γ1
2, γ2
2)· · · (γθ, γ1
θ,
γ2
θ)wi h σ′
α=γ1· · · γq, σ′
β=γq+1 · · · γθ, σj
α=γj
1· · · γj
q,
and σj
β=γj
q+1 · · · γj
θwi h j= 1,2, is said o be elemen a y
unsound pa h i he e exis s M, Mj∈Xεsa is ying he
ollowing condi ions: 1) M0
σ′
α
−−→
G′
e
Mσ′
β
−−→
G′
e
M; 2) M0
σj
α
−−−→
G′
e,n
Mjσj
β
−−−→
G′
e,n
Mj,∀j∈ J ; 3) ∈σ′
ασ′
β; 4) lj(σ′
α,k) = lj(σj
α,k)
and lj(σj
β,k) = lj(σ′
β,k); 5) no p e ix o eσsa is ies condi ions
(1)–(4).
P oposi ion 3.7: An LPN sys em ⟨N, Σ, l, M0⟩is codiag-
nosable i and only i he e exis no elemen a y unsound pa hs
in he co esponding ε-UV.
P oo : I he LPN sys em is deadlock- ee, he p oo
p ocedu e is same as he one in [29]. Once he LPN sys em
con ains he deadlock, a sel -loop encoded wi h an unobse -
able ansi ion u( ha is no obse ed by sys em and labeled
wi h he emp y s ing ε) is added o each dead ma king, hen
he ne sys em becomes deadlock- ee.
Example 2: The ε-UV, as displayed in Fig. 3, is cons uc ed
by he pa allel composi ion o all he ε-BRGs. We deduce ha
he LPN sys em is codiagnosable since i s si e 2 wi h e en se
Σ2={a, c, d}is codiagnosable wi h espec o aul ansi ion
11. P ecisely, he occu ence o aul 11 can be de ec ed by
obse ing he e en label ca si e 2. In o he wo ds, a his
si e we canno ind wo a bi a ily long sequences ha hold
same obse a ion, and one con ains aul while he o he no ,
i.e., he e is no elemen a y unsound pa h in he ε-UV. ♢
!", $; !"; !"
('(, '(, '()
!*, $; !*; !*
('+, '+, ,)
!-, .; !*; !*
('**, ,, ,)
!/, $; !*; !/
F-s a e
('0, ,, '0)
!/, $; !*; !/
('1, ,, '1)
Duplica e
N-s a e
!+, $; !+; !+
('2, '2, '2)
!3, $; !3; !+
('4, '4, ,)
!*, $; !*; !*
('(, '(, '()
Duplica e
N-s a e
Fig. 3. Pa o he ε-UV.
B. Replacemen and s eal hy a ack
The a chi ec u e o codiagnosabili y analysis unde a acks
is p esen ed in Fig. 4. To in es iga e he codiagnosabili y o
he LPN sys em, we conside he P o ocol 3 in [32] ha does
no equi e any coo dina ion be ween si es, i.e., each si e has
i s own e en se , such ha a ne is said o be codiagnosable
wi h espec o a aul i a leas one si e could deduce
he occu ence o he aul wi hin ini e s eps. In e ms o
a ack p ocess o comp omising he codiagnosabili y o LPN
sys ems in his decen alized se ing, a acke s a e designed
o execu e hei co up ion ac ions sepa a ely a each si e such
ha no si e can de ec any aul in he sys em. Speci ically, we
ocus on he ollowing case: i) an a acke co up s he sys em
obse a ion based on he labeling unc ion o i s loca ed si e;
ii) a coo dina ion be ween a acke s is applied o achie e he
a acke ’s goal. Elabo a ely, o any common ansi ion ha
belongs o di e en si es, once i s ansi ion label is eplaced
by one a acke in a si e, i has he same co up ed obse a ion
a o he si es when exis ing.
LPN sys em ! = ⟨ $, Σ, ', ()⟩
Labeling unc ion '+
A acke 1 A acke 2
Coo dina o
Codiagnosbili y
Labeling unc ion ',
-+= '+(/) -,= ',(/)
-′+= '2
+(/) -′,= '2
,(/)
Fig. 4. Decen alized a chi ec u e o codiagnosabili y unde a acke s.
To cha ac e ize he capabili y o an a acke o in ude ha
masks he ansi ion labels a each si e, a eplacemen a ack
s uc u e (a ack s uc u e o sho ) is p esen ed as ollows.
To make he exposi ion clea , we deno e by Σj
ε= Σj∪ {ε}
he e en se o si e jcon aining emp y s ing.
De ini ion 3.8 (A ack s uc u e): Le S=⟨N, Σ, l, M0⟩
be an LPN sys em moni o ed by a se o si es J={1,
2, . . . , ξ}. An a ack s uc u e is de ined as he se A ∈
2((To∪T ,a)×Σε)×((To∪T ,a)×Σε), i.e., Ais a se o ansi ion
pai s, each associa ed o i s label: he i s ansi ion is asso-
cia ed o he o iginal label while he second one is associa ed
o he eplaced label. Fo each si e jand o any ansi ion
∈Tj
o∪T ,a wi h l( ) = e∈Σj
ε, he co esponding a ack
s uc u e o si e jis
Aj={( (e), (e′)) |( (e), (e′)) ∈ A, e′∈Σj
ε}
{( (e), (ε)) |( (e), (e′)) ∈ A, e′/∈Σj
ε}.
♢
In plain wo ds, conce ning each pai ( (e), (e′)) ∈ A, i
he eplaced ansi ion label e′belongs o he e en se Σj
εo
si e j, hen i holds he label e′in he a ack s uc u e o si e j
as ( (e), (e′)) ∈ Aj. O he wise, i holds he emp y s ing εas
( (e), (ε)) ∈ Ajsince he si e jcanno obse e he eplaced
7
ansi ion label e′, i.e, e′/∈Σj
ε. Rema k ha each ansi ion
wi h espec o he a ack s uc u e may be eplaced wi h one
o se e al di e en labels o emp y s ing. Fo ins ance, an
a ack s uc u e is Aj={( k(a), k(b)),( k(a), k(ε)),( i(c),
i(d))}, wi h espec o si e j∈ J , ha assigns o ansi ion
kei he a label bo ε om he o iginal label a, and ansi ion
ia label d om he o iginal label cunde he co esponding
a acks. Fo he sake o cla i y, we deno e by Tj
as ={ ∈
Tj
o∪T ,a | ∃e′∈Σj
ε,( (e), (e′)) ∈ Aj} he se o a ackable
ansi ions wi h espec o he a ack s uc u e Aj, and deno e
by ΣAj( ) = {e′∈Σj
ε|( (e), (e′)) ∈ Aj, ∈Tj
as, e =lj( )}
he se o eplaced labels associa ed wi h ansi ion while
aking in o accoun he a ack s uc u e Aj.
In his wo k, an a ack is modeled by a unc ion ha
associa es a ansi ion wi h a unique obse a ion, i.e., o iginal
o eplaced label, which is o mally de ined in he ollowing
pa . Pa icula ly, a each si e j, a e he occu ence o a
ansi ion in Tj
as, i is possible o obse e i s o iginal label
o a eplaced label, such ha he gi en a ack s uc u e Aj
may cause mul iple a ack op ions.
De ini ion 3.9 (Replacemen a ack uple): Le S=⟨N, Σ,
l, M0⟩be an LPN sys em ha is moni o ed by si es J=
{1,2, . . . , ξ}and Abe an a ack s uc u e. A eplacemen
a ack uple is deno ed by A= (A1, A2, . . . , Aξ), whe e a
eplacemen a ack Aj(a ack o sho ) is a modi ied labeling
unc ion ha is he mapping lj
a:T∗→Σj
ε
∗whe e
lj
a(ε) = ε,
lj
a( ) = lj( )i ∈T Tj
as,
lj( )o e′∈ΣAj( )i ∈Tj
as,
lj
a(σ ) = lj
a(σ)lj
a( ), σ ∈T∗, ∈T. ♢
No e ha each ansi ion ∈Tj
as, unde he a ack Aj, is
ei he associa ed wi h he o iginal label lj( )o a eplaced
label e′∈ΣAj( )in e m o a ack s uc u e Aj.
One ema k is ha he conside ed eplacemen a ack con-
ains some pa icula inse ion and emo al cases. Fo ins ance,
i an unobse able ansi ion is associa ed o a label unde he
a ack, i is an inse ion a ack; I an obse able ansi ion is
associa ed wi h an emp y s ing, his eplacemen could be
ega ded as a emo al a ack.
De ini ion 3.10 (S eal hy a ack): Gi en an LPN sys em ⟨N,
Σ, l, M0⟩ ha is moni o ed by a se o si es J={1,2, . . . , ξ}
unde a eplacemen a ack uple A, he a ack uple Ais said
o be s eal hy i o any ansi ion sequence σ, i s co up ed
obse a ions a e con ained in he language o LPN sys em,
i.e., ∀σ∈Lω(N, M0),∀j∈ J , lj
a(σ)∈ L(N, M0).♢
P ecisely, s eal hiness equi es ha , o each si e, he se o
co up ed obse a ions is con ained in he se o obse a ions
wi hou a acks. This gua an ees ha he occu ence o a acks
canno be dis inguished om he sys em beha io .
C. K-co up ion in e mi en a ack
Compa ed wi h con inuous o pe manen a acks, in e mi -
en a acks a e mo e p ac ical as hey conside limi ed a ack
ene gy and limi ed a ack pe iod. He e we conside a scena io
ha a ack could las o a mos a ce ain pe iod o ime. To
do so, we assume ha a e a bounded numbe o consec-
u i e co up ed obse a ions unde he a acks, he eplaced
ansi ion label mus be eco e ed, which leads o a new
no ion o K-co up ion in e mi en a ack. Mo e p ecisely, in
a decen alized s uc u e, gi en a ansi ion sequence σ∈T∗
and si e j∈ J ={1,2, . . . , ξ}, i he ansi ions ∈Tj
as ha e
been eplaced Kj∈N imes consecu i ely in σunde he
a acks, hen hei (Kj+1) h occu ence mus hold i s o iginal
label. He e we de ine a ec o K= [K1, . . . , Kj, . . . , Kξ]
whe e ξis he numbe o si es ha moni o he sys em. The
ollowing example is used o illus a e a scena io abou K-
co up ion in e mi en a ack.
Example 3: Le us conside again he LPN sys em as de-
pic ed in Fig. 1 ha is ulne able o he gi en a ack s uc u e
A={( 8(ε), 8(d)),( 12(c), 12(ε)),( 13(a), 13(ε)),( 13(a),
13(d)),( 14(ε), 14(d))}and is moni o ed by wo si es, whe e
Σ1={a, b, d}and Σ2={a, c, d}. By De ini ion 3.8, i
holds A1={( 8(ε), 8(d)),( 13(a), 13(ε)),( 13(a), 13(d)),
( 14(ε), 14(d))}, and A2={( 8(ε), 8(d)),( 12(c), 12(ε)),
( 13(a), 13(ε)),( 13(a), 13(d)),( 14(ε), 14(d))}. In addi ion,
we ge he se s o a ackable ansi ions wi h espec o A1
and A2as T1
as ={ 8, 13, 14}and T2
as ={ 8, 12, 13, 14},
espec i ely. The LPN sys em execu es a sequence σ=
1 2 11 12 13 14. We assume ha he maximum consecu i e
co up ion ec o is K= [1 2] whe e K1= 1 and K2= 2.
Fo si e j= 1 wi h Σ1={a, b, d}, and i has he
o iginal obse a ion l1(σ) = aa and all he possible co up ed
obse a ions a e {a, ad, add}. Speci ically, he unobse able
ansi ions 1, 11 and he obse able ansi ions 2, 12 canno
be a acked since 1, 2, 11, 12 /∈T1
as and holds l1( 1) =
l1( 11) = l1( 12) = ε, l1( 2) = a. The wo d “aa”is obse ed
i he e is no any a ack; “a”is obse ed i he label o
ansi ion 13 is eplaced by he emp y s ing ε. In pa icula ,
he obse a ion “add”is ob ained i bo h labels o ansi ions
13 and 14 a e eplaced by d. Howe e , he consecu i e
co up ion K1′= 2 exceeds he maximum one K1= 1,
hus his case wi h he obse a ion add canno exis in he
K-co up ion in e mi en a ack se ing bu could exis in he
pe manen a ack se ing. ♢
A each si e j, o dis inguish he occu ence o a ansi ion
∈Tj
as ha is associa ed wi h i s o iginal label om he
eplaced one, we deno e by a he ansi ion whose label is
eplaced unde an a ack, and by na he ansi ion ha holds
i s o iginal obse a ion, espec i ely. Gi en an LPN sys em
and a si e j, unde an a ack Aj, le Tj
a={ a
i: i∈Tj
as |
lj
a( i)=lj( i)}be he se o a ackable ansi ions ha a e
associa ed wi h o he labels, and le Tj
na ={ na
i: i∈Tj
as |
lj
a( i) = lj( i)}be he se o a ackable ansi ions ha hold
hei o iginal labels.
Inspi ed om he app oach in [35], o ob ain all he co -
up ed possibili ies o a ansi ion sequence unde an a ack
o each si e j, we de ine an inse ion unc ion Ij:T∗→
2(T∪Tj
a∪Tj
na)∗
, whe e Ij(ε) = ε, Ij( ) = { a, na}, i ∈
Tj
as, o he wise Ij( ) = . Mo eo e , Ij(σ ) = Ij(σ)Ij( ) o
all σ∈T∗and ∈T. The in e se o inse unc ion is de ined
as I−1
j: (T∪Tj
a∪Tj
na)∗→T∗, whe e I−1
j(ε) = ε, I−1
j( a) =
, I−1
j( na) = , i ∈Tj
as, o he wise I−1
j( ) = . Mo eo e ,
I−1
j(σ ) = I−1
j(σ)I−1
j( ) o all σ∈(T∪Tj
a∪Tj
na)∗and
∈(T∪Tj
a∪Tj
na). We deno e by Pj
a,na : (T∪Tj
a∪Tj
na)∗→
8
(Tj
a∪Tj
na)∗ he p ojec ion o e Tj
a∪Tj
na, and deno e by
P ,j
a,na : (T∪Tj
a∪Tj
na)∗→(Tj
a∪Tj
na ∪T )∗ he p ojec ion
o e Tj
a∪Tj
na ∪T . In he ollowing, we o mally p esen
K-co up ion in e mi en a acks in he LPN sys em.
De ini ion 3.11 (K-co up ion in e mi en a ack): Le ⟨N,
Σ, l, M0⟩be an LPN sys em ha is moni o ed by a se o si es
J={1,2, . . . , ξ}and is ulne able o he a ack s uc u e A.
Gi en a ansi ion sequence σ∈T∗and a si e j, a unc ion ha
models he in e mi en a ack, such ha he maximum numbe
o consecu i e co up ed obse a ions is Kj, is a mapping
Φj:T∗→2(T∪Tj
a∪Tj
na)∗
whe e a sequence σ+∈Φj(σ), i σ+sa is ies he ollowing
condi ions:
(i) σ+∈Ij(σ);
(ii) o all µ′, µ′′′ ∈(Tj
a∪Tj
na)∗and µ′′ ∈Tj
a
∗, such ha
Pj
a,na(σ+) = µ′µ′′µ′′′, hen |µ′′| ≤ Kj.♢
Condi ion (i) ensu es ha he sequence σ+is ob ained om
he inse ion unc ion Ij(σ). Condi ion (ii) gua an ees ha he
maximum numbe o consecu i e co up ed obse a ions o σ
is Kjin he si e j.
Rema k 3.12: Fo scena ios whe e a acks can only las o
a limi ed pe iod, such as came a down ime du ing secu i y
pe sonnel shi s o main enance pe iods, o due o limi ed
a ack ene gy, he in e mi en a ack model wi h a speci ied
K alue can be used. This K alue ep esen s he maximum
numbe o consecu i e co up ed labels allowed du ing an
a ack. I K→+∞, he a ack model esembles a con inuous
o pe manen a ack, as i emo es cons ain s on he maximum
consecu i e co up ed labels. Con e sely, i K= 0, i indica es
a sa e en i onmen o he sys ems whe e no ansi ion labels
can be a acked.
Rema k 3.13: The wo k [35] ouches upon he K-loss obse -
a ion ha could be ega ded as a special case in his wo k, i.e.,
he loss obse a ions implies ha some obse able ansi ions
a e eplaced in o emp y s ing unde a acks. Howe e , he
p oposed a ack model is mo e lexible o cha ac e ize di e en
a ack cases, o ins ance, he i s case is he ansi ion label
could be eplaced in o di e en labels no only he emp y
s ing; he second case is ha an unobse able ansi ion
associa ed wi h a candida e senso could also be a acked, such
as es a ing he senso o ob ain a new obse a ion.
Example 4: Le he LPN sys em Sbe moni o ed by wo
si es and he e en se s be Σ1={a, b, d}and Σ2={a, c, d}.
Assume ha he sys em execu es a ansi ion sequence σ=
1 2 11 12 13 14 and K= [1 2], acco ding o De ini ion 3.11,
he ollowing sequences can be gene a ed since K-co up ion
in e mi en a acks.
•Fo si e j= 1, i has Φ1(σ) = { 1 2 11 12 13 na
13 14 na
14 ,
1 2 11 12 13 a
13 14 na
14 , 1 2 11 12 13 na
13 14 a
14}whose
p ojec ion o e (T1
a∪T1
na)∗is P1
a,na(σ+) = { na
13 na
14 ,
a
13 na
14 , na
13 a
14}.
•Fo si e j= 2, i has Φ2(σ) = { 1 2 11 12 a
12 13 a
13
14 na
14 , . . . , 1 2 11 12 na
12 13 a
13 14 na
14 }whose p ojec ion
o e (T2
a∪T2
na)∗is P2
a,na(σ+) = { a
12 a
13 na
14 ,...,
na
12 a
13 na
14 }.♢
D. P oblem s a emen
In p ac ice, many cybe physical sys ems can be e icien ly
modeled by Pe i ne s o LPN, such as au oma ed manu-
ac u ing p ocesses [41], esou ce alloca ion sys ems [42],
and in elligen anspo a ion ne wo ks [43], [44]. F om an
a acke iewpoin , he iola ion o sys em secu i y p ope ies,
such as opaci y and diagnosabili y, can lead o po en ial
damage in pu sui o he a acke ’s objec i es. Meanwhile, he
K-co up ion in e mi en a ack is conside ed in his pape
o add ess a ack scena ios wi h cons ain s such as limi ed
a ack ene gy o limi ed a ack pe iods. In he ollowing, we
o mula e he add essed p oblem in his wo k.
P oblem 1: Gi en an LPN sys em ⟨N, Σ, l, M0⟩ ha is
moni o ed by a se o si es J={1,2, . . . , ξ}and ulne able
o an a ack s uc u e A, he aim is o design he s eal hy K-
co up ion in e mi en a acks such ha he codiagnosabili y
o he sys em is iola ed.
The ollowing assump ions hold o he codiagnosabili y
analysis unde he a acks in he LPN sys ems.
(A1) The LPN sys em is bounded.
(A2) The (T Tj
o)-induced subne is acyclic o all j∈ J .
The wo assump ions a e common o he diagnosabili y o
codiagnosabili y analysis in he LPN sys ems, as he wo ks in
[20], [29], [39]. Speci ically, assump ion (A1) ensu es ha ε-
BRG o he LPN sys em is always ini e while assump ion
(A2) allows o use he s a e equa ion o cha ac e ize he
ma kings ha a e eached by i ing unobse able ansi ions
om an ex ended basis ma king, and gua an ees ha an ε-BRG
con ains a co ec abs ac ep esen a ion o a ne eachabili y
se .
IV. K-CORRUPTION INTERMITTENT ATTACKS FOR
VIOLATING THE CODIAGNOSABILITY
A. K-co up ion In e mi en a ack au oma on
In his pa , we p esen an algo i hm o cons uc a Kj-
co up ion in e mi en a ack au oma on o each si e j∈ J ,
which models he a acked beha io conside ing he maximum
consecu i e numbe o Kjco up ed obse a ions.
Algo i hm 1 lis s all he possible a acked sequences wi hin
Kjconsecu i e co up ed obse a ions in he a ack au oma-
on, whe e Qjis he se o s a es, T∪Tj
a∪Tj
na is he se o
ansi ions, δjis he ansi ion ela ion, and Qj
0is he ini ial
s a e. Each s a e o Qjis a uple o med by he occu ence
o a acked ansi ion a(o he occu ence o each ansi ion
∈Tj
as) and a coun e wi h he numbe o co up ed obse a-
ions o , i.e., ( a, i)∈Qjand ( , i)∈Qj. Mo e p ecisely,
line 1ini ializes he s a e se , he ini ial s a e, and wo indexes.
The ini ial s a e Qj
0= ( a,0) implies ha he numbe o
consecu i e co up ed obse a ions ais 0. In he lines 2–
11, he occu ence o a ansi ion ∈Tj
as gene a es a new
s a e ( , i)and a ansi ion om ( a, i) o s a e ( , i), while he
occu ence o a ansi ion ∈T Tj
as emains he s a e ( a, i)
and displays as a sel -loop ansi ion. I a ansi ion in he
s a e ( , i)is no a acked, i.e., ∈Tj
na, he s a e ( , i) eaches
( a,0). In o he wo ds, he occu ence o na ese s he coun e
as 0. Lines 12–15 p esen ha he occu ence o ansi ion a
( he label o ansi ion is eplaced by o he s unde he a ack)
9
Algo i hm 1: Cons uc ion o an a ack au oma on ∆j
o a si e j
Inpu : Kj,⟨N, Σ, l, M0⟩, Tj
a,Tj
na
Ou pu : ∆j= (Qj, T ∪Tj
a∪Tj
na, δj, Qj
0)
1Le Qj
0= ( a,0), Qj=∅, i = 0, q = 0;
2while i≤Kjdo
3Qj=Qj∪ {( a, i)};
4 o ∈Tdo
5i ∈Tj
as hen
6Qj=Qj∪ {( , i)};
7δj(( a, i), )=( , i);
8δj(( , i), na)=( a,0);
9i ∈T Tj
as hen
10 δj(( a, i), )=( a, i);
11 i=i+ 1;
12 while q < Kjdo
13 o ∈Tj
as do
14 δj(( , q), a) = ( a, q + 1);
15 q=q+ 1;
inc eases he coun e and c ea es he ansi ion om s a e
( a, q) o s a e ( a, q+1). Consequen ly, he maximum numbe
o consecu i e occu ences o a, wi hou he occu ence o
na, is equal o Kj.
Example 5: Conside he LPN sys em Sin Example 3
and K= [1 2], by using Algo i hm 1, he K-co up ion
in e mi en a ack au oma on ∆j o each si e jis gi en as
shown in Fig. 5. Fo he sake o simplici y, we deno e by
Tj
,u =T Tj
as o j= 1,2.♢
!"
(!$, 0) (!", 0)
!"
($
!"
$
(!", 1)
!"
(!$, 1)
!"
($
*+,,
-*+,,
-
(a)
!",$
%
&'
(&), 0) (&', 0)
&'
,)
&'
)
(&', 1)
&'
(&), 1)
&'
,)
(&', 2) &'(&), 2) &'
)
&'
,)
!",$
%
!",$
%
(b)
Fig. 5. (a) A ack au oma on ∆1wi h i∈T1
as and K1= 1. (b) A ack
au oma on ∆2wi h i∈T2
as and K2= 2.
Fo any si e j, he LPN sys em unde Kj-co up ion in-
e mi en a acks can be cha ac e ized by he pa allel com-
posi ion o he ε-BRG Geand all he au oma a ∆jo
he non ailu e ε-BRG Gj
e,n and he au oma on ∆j, such
ha G′
e=Ge||∆1||...||∆ξand Gj′
e,n =Gj
e,n||∆j. No e
ha “||”deno es he ope a ion o pa allel composi ion. To
make he exposi ion clea , in he ollowing le us deno e by
L(Ge), L(G′
e), L(Gj′
e,n), L(Gj
e,n) he languages gene a ed by
he g aphs Ge, G′
e, Gj′
e,n, Gj
e,n ha con ain he se o i ing
ansi ion sequences, espec i ely.
Lemma 4.1: Fo all ansi ion sequences σ∈L(G′
e)( esp.,
σ∈L(Gj′
e,n)), i holds I−1
j(σ)∈L(Ge)( esp., I−1
j(σ)∈
L(Gj
e,n)), and ha hei maximum consecu i e co up ion is
equal o o less han Kj.
P oo : Conside a sequence σ∈L(G′
e), whe e G′
e
is ob ained by he pa allel composi ion o Geand all he
a ack au oma a wi h espec o di e en si es ∆1, ..., ∆ξ. By
using he in e se o inse unc ion I−1
j, all he ansi ions
belonging o Tj
a∪Tj
na will be emo ed, such ha i holds
I−1
j(σ)∈L(Ge). Simila ly, o a sequence σ∈L(Gj′
e,n), i
holds I−1
j(σ)∈L(Gj
e,n). The pa o ha hei maximum
consecu i e co up ion is equal o o less han Kj o each
sequence in G′
eand Gj′
e,n is simila o he p oo in [35] wi hou
he conside a ion o he communica ion channel.
Example 6: Con inue he Example 3, he pa ial pa s o
G′
e=Ge||∆1||∆2and Gj′
e,n =Gj
e,n||∆j o si e j=1, 2, a e
gene a ed as shown in Figs. 6 and 7. In de ail, he s a e o
G′
eand G′
e,n is a uple o med by he ex ended basis ma king
and i s co esponding s a e o a ack au oma on. ♢
B. Comple e a ack g aph
In his pa , we p esen an app oach o he cons uc ion o
a comple e a ack g aph ha gene a es all he po en ial pa hs
o be a acked, possibly leading o an elemen a y unsound
pa h ha iola es he codiagnosabili y in he sys em, which
is shown in he ollowing algo i hm.
Algo i hm 2 ou pu s a comple e a ack g aph Uc= (Xu
c,
Eu
c, δu
c, xu
0), whe e Xu
cis he se o s a es, Eu
cis he e en
se , δu
cis he ansi ion ela ion, and xu
0is he ini ial s a e.
In con as o he classic e i ie app oaches in [29], [31] ha
a e ob ained by using he pa allel composi ion o ailu e g aph
and non ailu e g aphs, a s a e o he p oposed comple e a ack
g aph is upda ed e en hough o a ansi ion ( , 1, 2), i holds
l( )=l1( 1)and l( )=l2( 2). In addi ion, such a comple e
a ack g aph in eg a es he p oposed a ack au oma on, such
ha all he po en ial a acked pa hs limi ed o Kconsecu i e
co up ions a e lis ed. Gi en he a ack s uc u e wi h espec
o each si e, i is possible ei he o associa e ansi ion
wi h a label e∈Σo o eplace he label o ansi ion
as emp y s ing ε. Then he obse a ion o ansi ions in he
uple ( , 1, 2)becomes same o he ansi ion sequence in
he consecu i e uples has he same obse a ion, such ha he
pa h con aining ( , 1, 2)is possible o be a acked in o an
elemen a y unsound pa h.
P ecisely, line 1 ini ializes he s a e se , he ini ial s a e
and ou indices q, k, β, γ. The ini ial s a e xu
0= [M0,
( a,0),( a,0), N;M1
0,( a,0); M2
0,( a,0)] implies ha he e
is no aul a ini ial s a e wi h Nsymbol and he numbe
o consecu i e co up ed obse a ions ais 0 wi h ( a,0).
Lines 2–23, a each un agged s a e, i e a i ely gene a e all he
o he s a es by enume a ing he consecu i e ansi ion pai s
wha e e he obse a ion o ansi ions in he pai is same
o no . In de ails, lines 4–18 conside all he possibili ies o