Tes ing Iden i iable Ke nel P Sys ems Using an
X-machine App oach
Ma ian Gheo ghe1, Flo en in Ipa e2, Raluca Le ica u1,2, Ana T¸u lea2
1School o Elec ical Enginee ing and Compu e Science,
Uni e si y o B ad o d, Wes Yo kshi e, B ad o d BD7 1DP, UK
{m.gheo ghe, .le ica u}@b ad o d.ac.uk
2Depa men o Compu e Science,
Facul y o Ma hema ics and Compu e Science and ICUB
Uni e si y o Bucha es ,
S . Academiei n . 14, 010014, Bucha es , Romania
[email p o ec ed],[email p o ec ed]
Summa y. This pape p esen s a es ing app oach o ke nel P sys ems (kP sys ems),
based on he X-machine es ing amewo k and he concep o co e au oma on. The
es ing me hodology ensu es ha he implemen a ion con o ms he speci ica ions, unde
ce ain condi ions, such as he iden i iably concep in he con ex o ke nel P sys ems.
Keywo ds: memb ane compu ing; ke nel P sys ems; X-machines; co e au oma a;
es ing.
1 In oduc ion
Memb ane compu ing [19] is a esea ch ield ini ia ed wen y yea s ago [17, 18] by
Gheo ghe P˘aun. Ini ially inspi ed by he s uc u e and unc ioning o he li ing
cells, he ield has known a as de elopmen , di e en ypes o memb ane sys ems
(o P sys ems) being in es iga ed.
Ha ing so many compu a ional models (cell-like, issue-like P sys ems, P
colonies, ke nel P sys ems) and also di e en so wa e implemen a ions o hese
models, i is impo an o de ise es ing me hodologies ha ensu e ha he imple-
men a ion con o ms wi h he speci ica ion. The es ing ask is no i ial, gi en he
ac ha he models a e pa allel and non-de e minis ic. P e ious wo ks on P sys-
ems es ing include es ing cell-like P sys ems wi h me hods like ini e s a e-based
inspi ed [13], s eam X-machine based es ing [14], mu a ion es ing o e alua ing
he e iciency o he es se s [16], model-checking based es ing [15].
In his pape we will p esen a es ing app oach o ke nel P sys ems, which is
based on he X-machine es ing app oach and has as co e concep he iden i iabili y
o mul ise s o ules. Ke nel P sys ems a e a model in oduced in [9], which can be
simula ed using a so wa e amewo k, called kPWo kbench [5] o some ea lie
80 M. Gheo ghe e al.
a ian s (so called simple kP sys ems) using P-Lingua and he MeCoSim simula o
[11].
This pape is s uc u ed as ollows: Sec ion 2 p esen s he p elimina ies ega d-
ing kP sys ems and heo e ical backg ound ega ding au oma a and X-machine
based es ing. Sec ion 3 in oduces he concep o iden i iable ke nel P sys ems,
while Sec ion 4 illus a es ou es ing app oach o kP sys ems. Finally, conclusions
a e p esen ed in Sec ion 5.
2 P elimina ies
This sec ion b ie ly p esen s he no a ions used, hen gi es he basic de ini ions
ega ding ke nel P sys ems [9] and p esen s he p e ious es ing app oaches o
au oma a and X-machines, ha ha e been applied also o es ing simple cell-like
P sys ems.
In he ollowing we in oduce he no a ions used in he pape . Fo a ini e
alphabe A={a1, ..., ap},A∗ ep esen s he se o all s ings (sequences) o e A.
The emp y s ing is deno ed by λand A+=A∗ {λ}deno es he se o non-emp y
s ings. Andeno es he se o all s ings o leng h n,n≥0, wi h membe s in he
alphabe A, and A[n] = S0≤i≤nAideno es he se o all s ings o leng h a mos
n.
Fo a s ing u∈A∗,|u|adeno es he numbe o occu ences o ain u, whe e
a∈A. Fo a subse S⊆A,|u|Sdeno es he numbe o occu ences o he symbols
om Sin u. The leng h o a s ing uis gi en by Pai∈A|u|ai. The leng h o he
emp y s ing is 0, i.e. |λ|= 0.
A mul ise o e Ais a mapping :A→N. Conside ing only he elemen s
om he suppo o (whe e (aij)>0, o some j, 1 ≤j≤p), he mul ise is
ep esen ed as a s ing a (ai1)
i1. . . a (aip)
ip, whe e he o de is no impo an . In he
sequel mul ise s will be ep esen ed by such s ings.
2.1 Ke nel P sys ems
In he ollowing we will gi e a o mal de ini ion o ke nel P sys ems (o kP sys-
ems) [9]. We s a by in oducing he concep o a compa men ype u ilised la e
in de ining he compa men s o a ke nel P sys em (kP sys em).
De ini ion 1. Tis a se o compa men ypes,T={ 1, . . . , s},whe e i=
(Ri, σi),1≤i≤s, consis s o a se o ules, Ri, and an execu ion s a egy, σi,
de ined o e Lab(Ri), he labels o he ules o Ri.
Ke nel P sys ems ha e ea u es inspi ed by objec -o ien ed p og amming, o
example one compa men ype can ha e one o mo e ins ances. These ins ances
sha e he same se o ules and execu ion s a egies (so will deli e he same
unc ionali y), bu hey may con ain di e en mul ise s o objec s and di e en
neighbou s acco ding o he g aph ela ion speci ied.
Tes ing Iden i iable Ke nel P Sys ems 81
De ini ion 2. AkP sys em o deg ee nis a uple kΠ = (A, µ, C1, . . . , Cn, i0),
whe e
•Ais a ini e se o elemen s called objec s;
•µde ines he memb ane s uc u e, which is a g aph, (V, E), whe e Vis a se
o e ices ep esen ing componen s (compa men s), and Eis a se o edges,
i. e., links be ween componen s;
•Ci= ( i, wi,0),1≤i≤n, is a compa men o he sys em consis ing o a
compa men ype, i, om a se Tand an ini ial mul ise , wi,0o e A; he
ype i= (Ri, σi)consis s o a se o e olu ion ules, Ri, and an execu ion
s a egy, σi;
•i0is he ou pu compa men whe e he esul is ob ained.
In his pape we will only deal wi h a simpli ied e sion o kP sys ems ha ing
one single compa men as his does no a ec he gene al me hod in oduced he e
and makes he p esen a ion easie o ollow. Fo de ails ega ding he ways o
la ening an a bi a y P sys em, including he kP sys em discussed in his pape ,
we e e mainly o [7], bu simila app oaches a e also p esen ed in o he pape s
([20], [1]). The kP sys em will be deno ed kΠ = (A, µ1, C1,1),whe e µ1deno es
he g aph wi h one node.
Wi hin he gene al kP sys ems amewo k, he ollowing ypes o e olu ion
ules ha e been conside ed so a :
• ew i ing and communica ion ule: x→y{g}, whe e g ep esen s a gua d (will
be o mally explained in De . 4), x∈A+and y∈A∗, whe e yis a mul ise wi h
po en ial di e en compa men ype a ge s (each symbol om he igh side o
he ule can be sen o a di e en compa men , speci ied by i s ype; i mul iple
compa men s o he same ype a e linked o he cu en compa men , hen
one is andomly chosen o be he a ge ). Unlike cell-like P sys ems, he a ge s
in kP sys ems indica e only he ypes o compa men s o which he objec s will
be sen , no pa icula ins ances ( o example, y= (a1, 1). . . (ah, h), whe e
h≥0, and o each 1 ≤j≤h,aj∈Aand jindica es a compa men ype
om T).
•s uc u e changing ules: memb ane di ision, memb ane dissolu ion, link c e-
a ion and link des uc ion ules, which all may also inco po a e complex gua ds
and ha a e co e ed in de ail in [9]. Howe e , his ype o ules will no be
conside ed in he ollowing discussion.
Rema k 1. In he con ex o one compa men kP sys ems, he e will be no need o
speci y he a ge compa men , so he ules will be simple communica ion ules,
which in addi ion can ha e gua ds. Each ule occu ing in he ollowing discussion
has he o m :x→y{g}, whe e iden i ies he ule and is called label,x→y
is he ule i sel and gis i s gua d. The pa x→yis also called he body o
he ule, deno ed also b( ). The gua ds a e cons uc ed using mul ise s o e A, as
ope ands, and ela ional o Boolean ope a o s. The de ini ion o he gua ds is now
in oduced. We s a wi h some no a ions.
82 M. Gheo ghe e al.
Fo a mul ise wo e Aand an elemen a∈A, we deno e by |w|a he numbe
o objec s aoccu ing in w. Le us deno e Rel ={<, ≤,=,6=,≥, >}, he se o
ela ional ope a o s, γ∈Rel, a ela ional ope a o , and ana mul ise , consis ing
o ncopies o a. We i s in oduce an abs ac ela ional exp ession.
De ini ion 3. I gis he abs ac ela ional exp ession deno ing γanand wa
mul ise , hen he gua d gapplied o wdeno es he ela ional exp ession |w|aγn.
The abs ac ela ional exp ession gis ue o he mul ise w, i |w|aγn is ue.
We conside now he ollowing Boolean ope a o s ¬(nega ion), ∧(conjunc-
ion) and ∨(disjunc ion). An abs ac Boolean exp ession is de ined by one o he
ollowing condi ions:
•any abs ac ela ional exp ession is an abs ac Boolean exp ession;
•i gand ha e abs ac Boolean exp essions hen ¬g,g∧hand g∨ha e abs ac
Boolean exp essions.
The concep o a gua d, in oduced o kP sys ems, is a gene alisa ion o he
p omo e and inhibi o concep s u ilised by some a ian s o P sys ems.
De ini ion 4. I gis an abs ac Boolean exp ession con aining gi,1≤i≤q,
abs ac ela ional exp essions and wa mul ise , hen gapplied o wmeans he
Boolean exp ession ob ained om gby applying gi o w o any i, 1≤i≤q.
As in he case o an abs ac ela ional exp ession, he gua d gis ue wi h
espec o he mul ise w, i he abs ac Boolean exp ession gapplied o wis ue.
Example 1. I gis he gua d de ined by he abs ac Boolean exp ession ≥a4∧<
b2∨ ¬ > c and wa mul ise , hen gapplied o wis ue i i has a leas 4 a0s and
less han 2 b0s o no mo e han one c.
In addi ion o i s e olu ion ules, each compa men ype in a kP sys em has
an associa ed execu ion s a egy. The ules co esponding o a compa men can
be g ouped in blocks, each ha ing one o he ollowing s a egies:
In kP sys ems he way in which ules a e execu ed is de ined o each compa -
men ype om T– see De . 1. As in De . 1, Lab(R) is he se o labels o he
ules R.
De ini ion 5. Fo a compa men ype = (R, σ) om Tand ∈Lab(R),
1, . . . , s∈Lab(R), he execu ion s a egy,σ, is de ined by he ollowing
•σ=λ, means no ule om he cu en compa men will be execu ed;
•σ={ }– he ule is execu ed;
•σ={ 1, . . . , s}– one o he ules labelled 1, . . . , swill be non-de e min-
is ically chosen and execu ed; i none is applicable hen no hing is execu ed;
his is called al e na i e o choice;
•σ={ 1, . . . , s}∗– he ules a e applied an a bi a y numbe o imes ( a bi a y
pa allelism);
Tes ing Iden i iable Ke nel P Sys ems 83
•σ={ 1, . . . , s}>– he ules a e execu ed acco ding o he maximal pa allelism
s a egy;
•σ=σ1&. . . &σs, means execu ing sequen ially σ1, . . . , σs, whe e σi,1≤i≤s,
desc ibes any o he abo e cases; i one o σi ails o be execu ed hen he es
is no longe execu ed.
These execu ion s a egies and he ac ha in any compa men se e al blocks
wi h di e en s a egies can be composed and execu ed o e a lo o lexibili y o
he kP sys em designe , simila ly o p ocedu al p og amming.
De ini ion 6. Acon igu a ion o a kP sys em, kΠ, wi h ncompa men s, is a
uple c= (c1, . . . , cn), whe e ci∈A∗,1≤i≤n, is he mul ise om compa men
i. The ini ial con igu a ion is (w1, . . . , wn), whe e wi∈A∗is he ini ial mul ise
o he compa men i,1≤i≤n.
A ansi ion (o compu a ion s ep), in oduced by he nex de ini ion, is he
p ocess o passing om one con igu a ion o ano he .
De ini ion 7. Gi en wo con igu a ions c= (c1, . . . , cn)and c0= (c0
1, . . . , c0
n)o a
kP sys em, kΠ, wi h ncompa men s, whe e o any i, 1≤i≤n,ui∈A∗, and a
mul ise o ules Mi= n1,i
1,i . . . nki,i
ki,i ,nj,i ≥0,1≤j≤ki, ki≥0, a ansi ion o
acompu a ion s ep is he p ocess o ob aining c0 om cby using he mul ise s o
ules Mi,1≤i≤n, deno ed by c=⇒(M1,...,Mn)c0, such ha o each i,1≤i≤n,
c0
iis he mul ise ob ained om ciby i s ex ac ing all he objec s ha a e in he
le -hand side o each ule o Mi om ciand hen adding all he objec s a ha a e
in he igh -hand side o each ule o Mi ep esen ed as (a, i)and all he objec s b
ha a e in he igh -hand side o each ule o Mj,j6=i, such ha bis ep esen ed
as (b, i).
In he heo y o kP sys ems, each compa men migh ha e i s own execu ion
s a egy. In he sequel we ocus on h ee such execu ion s a egies, namely max-
imal pa allelism, a bi a y pa allelism (also called asynch onous execu ion) and
sequen ial execu ion. These will be deno ed by max, async and seq, espec i ely.
When in a ansi ion om c o c0using (M1, . . . , Mm), we in end o e e o a
speci ic ansi ion mode m, m ∈ {max, async, seq}, hen his will be deno ed by
c=⇒(M1,...,Mm)
m c0.
Acompu a ion in a P sys em is a sequence o ansi ions (compu a ion s eps).
A con igu a ion is called inal con igu a ion, i no ule can be applied o i . In
a inal con igu a ion he compu a ion s ops.
As usual in P sys ems, we only conside e minal compu a ions, i.e., hose
a i ing in a inal con igu a ion and using one o he abo e men ioned ansi ion
modes. We a e now eady o de ine he esul o a compu a ion.
De ini ion 8. Fo a kP sys em kΠ using he ansi ion mode m, m ∈ {max,
async, seq}, in each compa men , we deno e by N m(Π) he numbe o objec s
appea ing in he ou pu compa men o a inal con igu a ion.

84 M. Gheo ghe e al.
Two kP sys ems kΠ and kΠ0a e called equi alen wi h espec o he ansi ion
mode m, m ∈ {max, async, seq}, i N m(kΠ) = N m(kΠ0).
In his pape we will only deal wi h kP sys ems ha ing one single compa men
as his does no a ec he gene al me hod in oduced he e and makes he p esen-
a ion easie o ollow. Indeed, limi ing he in es iga ion o one compa men kP
sys ems does no a ec he gene ali y o i due o he ac ha he e a e ways o
la ening an a bi a y P sys em, including he kP sys em discussed in his pape ,
in o a P sys em wi h one single compa men . Fo de ails ega ding he la ening
o a P sys em we e e mainly o [7], bu simila app oaches a e also p esen ed
in o he pape s ([20], [1]). Such a kP sys em will be deno ed kΠ = (A, µ1, C1,1),
whe e µ1deno es he g aph wi h one node. The ules on he igh -hand side will
ha e mul ise s o e A, as in he case o one single compa men he e is no need
o indica e whe e objec s a e sen o.
2.2 The W-me hod o es ing ini e co e au oma a
In he ollowing subsec ion we in oduce he basic ini e co e au oma a concep s
[3, 12] and he W-me hod o gene a ing es sui es om ini e co e au oma a
[13]. We will conside only de e minis ic ini e au oma a.
Fini e Co e Au oma a
De ini ion 9. A ini e au oma on (abb e ia ed FA) is a uple A= (V, Q, q0, F, h),
whe e:
•Vis he ini e inpu alphabe ;
•Qis he ini e se o s a es;
•q0∈Qis he ini ial s a e;
•F⊆Qis he se o inal s a es;
•h:Q×V→Qis he nex -s a e unc ion.
De ini ion 10. Le A= (V, Q, q0, F, h)be a FA, U⊆V∗a ini e language and l
he leng h o he longes sequence(s) in U. Then Ais called a de e minis ic ini e
co e au oma on (DFCA) o Ui LA∩V[l] = U. A minimal DFCA o Uis a
DFCA o Uha ing he leas numbe o s a es.
The concep o DFCA was in oduced by Cˆampeanu e al. [2], [3]. A minimal
DFCA ha e conside ably ewe s a es han he minimal FA ha accep s U.
The W-me hod
In con o mance es ing he e is a o mal speci ica ion o he sys em ( o example a
FA) and he aim is o gene a e a es sui e such ha whene e he implemen a ion
unde es (IUT) passes all es s, i is gua an eed o con o m o he speci ica ion.
The IUT is unknown bu i is assumed o beha e like some elemen om a se o
Tes ing Iden i iable Ke nel P Sys ems 85
models, called aul model. In he case o he W-me hod, he aul model consis s o
all FAs A0wi h he same inpu alphabe Vas he speci ica ion A, whose numbe o
s a es m0does no exceed he numbe o s a es mo Aby mo e han k(m0−m≤k),
whe e k≥0 is a p ede e mined in ege ha mus be es ima ed by he es e .
The W-me hod was o iginally de ised o when he con o mance ela ion is
au oma a equi alence [4], bu in his pape we a e in e es ed in con o mance o
bounded sequences. This p oblem is desc ibed in [10] as ollows: gi en an FA
speci ica ion Aand an in ege l≥1 ( he uppe bound) such ha LAcon ains a
leas one sequence o leng h l, we wan o cons uc a se o sequences o leng h
less han o equal o l ha can es ablish whe he he implemen a ion beha es as
speci ied o all sequences in V[l]. Since LAcon ains a leas one sequence o leng h
l,Ais a DFCA o LA∩V[l] and so he es sui e will check whe he he IUT
model A0is also a DFCA o LA∩V[l].
A es sui e will be a ini e se Yk⊆V[l] o inpu sequences ha , o e e y
A0in he aul model ha is no V[l]-equi alen o A, will p oduce a leas one
e oneous ou pu . Tha is, Aand A0a e V[l]-equi alen whene e Aand A0a e
Yk-equi alen .
Suppose he speci ica ion Aused o es gene a ion is a minimal DFCA o
LA∩V[l]. The W-me hod o bounded sequences, as de eloped in [12], in ol es
he selec ion o wo se s o inpu sequences, Sand W, as ollows:
De ini ion 11. S⊆V∗is called a p ope s a e co e o Ai o e e y s a e qo
A he e exis s s∈Ssuch ha h(q0, s) = qand |s|=le el(q).
De ini ion 12. W⊆V∗is called a s ong cha ac e isa ion se o Ai o e e y
wo s a es q1and q2o Aand e e y j≥0, i q1and q2a e V[j]-dis inguishable
hen q1and q2a e (W∩V[j])-dis inguishable.
Na u ally, in he abo e de ini ion, i is su icien o q1and q2 o be (W∩V[j])-
dis inguishable when jis he leng h o he sho es sequences ha dis inguish
be ween q1and q2.
Once Sand Wha e been selec ed, he es sui e is ob ained using he o mula:
Yk=SV [k+ 1](W∪ {λ})∩V[l] {λ}[12].
2.3 X-machine based es ing
This subsec ion p esen s he X-machine based es ing me hodology, gi ing he
o mal de ini ions o X-machines, he es ans o ma ion o an X-machine and
l-bounded con o mance es sui es. Fo mo e de ails and comple e p oo s [10] can
be consul ed, he e only he main esul s a e gi en.
An X-machine is a ini e au oma on in which ansi ions a e labelled by pa ial
unc ions on a da a se X ins ead o me e symbols [6].
De ini ion 13. An X-machine (XM) is a uple Z= (Q, X, Φ, H, q0, x0)whe e:
•Qis a ini e se o s a es;
86 M. Gheo ghe e al.
•Xis he (possible in ini e) da a se ;
•Φis a ini e se o dis inc p ocessing unc ions; a p ocessing unc ion is a
non-emp y (pa ial) unc ion o ype X→X;
•His he (pa ial) nex -s a e unc ion, H:Q×Φ→Q;
•q0∈Qis he ini ial s a e;
•x0∈Xis he ini ial da a alue.
We ega d an X-machine as a ini e au oma on wi h he a cs labelled by
unc ions om he se Φ, which is o en called he ype o Z. The au oma on
AZ= (Φ, Q, H, q0) o e he alphabe Φis called he associa ed ini e au oma on
(FA) o Z. The language accep ed by he au oma on is deno ed by LAZ.
De ini ion 14. Acompu a ion o Z is a sequence x0,...xn, wi h xi∈X, 1≤
i≤n, such ha he e exis φ1, . . . , φn∈Φwi h φi(xi−1) = xi,1≤i≤nand
φ1. . . φn∈LAZ. The se o compu a ions o Z is deno ed by Comp(Z).
A sequence o p ocessing unc ions ha can be applied in he ini ial da a alue
x0is said o be con ollable.
De ini ion 15. A sequence φ1, . . . , φn∈Φ∗, wi h φi∈Φ, 1≤i≤n, is said o be
con ollable i he e exis x1,...xn∈Xsuch ha φi(xi−1) = xi,1≤i≤n. A se
P⊆Φ∗is called con ollable i o e e y p∈P,pis con ollable.
Le us assume we ha e an X-machine speci ica ion Zand an (unknown) IUT
ha beha es like an elemen Z0o a aul model. In his case, he aul model
will be a se o X-machines wi h he same da a se X, ype Φand ini ial da a
alue x0as he speci ica ion. The idea o es gene a ion om an X-machine is o
educe checking ha he IUT Z0con o ms o he speci ica ion Z o checking ha
he associa ed au oma on o he IUT con o ms o he associa ed au oma on o he
X-machine speci ica ion.
De ini ion 16. The es ans o ma ion o Zis he (pa ial) unc ion :Φ∗→X∗
de ined by:
• (λ) = x0.(1)
•Le p∈Φ∗and φ∈Φ.
– Suppose (p)is de ined. Le (p) = x0. . . xn.
·I xn∈domφ hen:
·I p∈LAZ hen (pφ) = (p)φ(xn).(2)
·Else (pφ) = (p).(3)
·Else (pφ)is unde ined. (4)
– O he wise, (pφ)is unde ined. (5)
Lemma 1. Le be a es ans o ma ion o Zand p=φ1. . . φn, wi h φ1, . . . , φn∈
Φ.
•Suppose pis con ollable and le x1, . . . , xn∈Xsuch ha φi(xi−1) = xi,1≤
i≤n.
Tes ing Iden i iable Ke nel P Sys ems 87
– I p∈LAZ, hen (p) = x0. . . xn.
– I p /∈LAZ, hen (p) = x0. . . xk+1, whe e 0≤k≤n−1, is such ha
φ1. . . φk∈LAZand φ1. . . φkφk+1 /∈LAZ.
•I p is no con ollable, hen (p) is no de ined.
In o de o es ablish ha he associa ed au oma on o he IUT Z0con o ms
o he associa ed au oma on o he X-machine speci ica ion Z, we ha e o be able
o iden i y he p ocessing unc ions ha a e applied when he compu a ions o Z
and Z0a e examined.
De ini ion 17. Φis called iden i iable i o all φ1, φ2∈Φ, whene e he e exis s
x∈Xsuch ha φ1(x) = φ2(x),φ1=φ2.
I Φis iden i iable, hen we a e able o es ablish i a con ollable sequence o
p ocessing unc ions is co ec ly implemen ed by examining he compu a ions o
he speci ica ion Zand he implemen a ion Z0, as shown by he ollowing lemma.
Lemma 2. Le Zand Z0be XMs wi h ype Φ. Suppose Φis iden i iable. Le p=
φ1. . . φn∈Φ∗, wi h φi∈Φ,1≤i≤n, be a con ollable sequence. Suppose (p)is
a compu a ion o Zi and only i (p)is a compu a ion o Z0. Then p∈LAZi
and only i p∈LA0
Z.
De ini ion 18. Le Z be an X-machine and C a aul model o Z. An l-bounded
con o mance es sui e o Z w. . . C, l > 0, is a se T⊆X[l+ 1] such ha
o e e y Z0∈C he ollowing holds: i T∩Comp(Z) = T∩Comp(Z0) hen
Comp(Z)∩X[l+ 1] = Comp(Z0)∩X[l+ 1].
Tha is, whene e any elemen o Tis a compu a ion o Zi and only i i is a
compu a ion o Z0,Z0con o ms o Z o sequences o leng h up o l. The ollowing
heo em shows ha he es ans o ma ion de ined ea lie p o ides a mechanism
o con e ing es sui es o ini e au oma a in o se sui es o X-machines.
Theo em 1. Le Zbe an XM wi h ype Φ, da a se Xand ini ial da a alue x0.
Suppose Φis iden i iable and LAZ∪Φ[l]is con ollable. Le Cbe a se o XMs such
ha o e e y Z0∈C,LA0
Z∩Φ[l]is con ollable. Le P⊆Φ[l], such ha , o e e y
Z0∈C, whene e P∩LAZ=P∩LA0
Zwe ha e LAZ∩Φ[l] = LA0
Z∩Φ[l]. Then
(P)is an l-bounded con o mance es sui e o Zw. . . C.
Le l > 0 be a p ede ined uppe bound. We assume ha Φis iden i iable and
LAZ∩Φ[l] is con ollable. We assume ha AZ, he associa ed au oma on o Z, is
a minimal DFCA o LAZ∪Φ[l] (i no , his is minimised 3). Suppose he aul
model Cis he se o X-machines Z0wi h he same da a se X, ype Φand ini ial
da a alue x0as Zsuch ha LAZ0∩Φ[l] is con ollable, whose numbe o s a es
m0does no exceed he numbe o s a es mo Zby mo e han k(m0−m≤k),
k≤0. Then an l-bounded con o mance es sui e o Zw. . . Cis
3The minimisa ion p ese es he con olabili y equi emen s as he se LAZ∩Φ[l] e-
mains unchanged.
94 M. Gheo ghe e al.
Conside again he P sys em kΠ1as in Example 3. Then ab =⇒ 2bc and
bc =⇒ 4bc2, bu bc2=⇒ 4bc3does no hold since he ules o kΠ1mus
be applied in he maximally pa allel mode. Howe e , i we conside ha in
he aul model o he IUT ules may be applied in he asynch onous mode,
he sequence 2 4 4is con ollable. The aul model is also de e mined by
he maximum numbe o s a es m+k ha he IUT may ha e, whe e mis
he numbe o s a es o he X-machine Zand k≥0 is a non-nega i e in ege
es ima ed by he es e .
3. Cons uc an l-bounded con o mance es sui e.
This is Tk= (Yk), whe e Yk=SΦ[k+ 1](W∪ {λ})∩Φ[l] {λ}and is a es
ans o ma ion o Z.
Acco ding o [4], he uppe bound o he numbe o sequences in SΦ[k+ 1]W
is m2· k+1 and he o al leng h o all sequences is no g ea e ha m2·(m+
k)· k+1,whe e is he numbe o elemen s o Φ. In pa icula , o k= 0,
he espec i e bounds a e m2· and m3· . The inc ease in size p oduced by
eplacing Wwi h W∪ {λ}in he abo e o mula is negligible. No e ha hese
bounds e e o he wo s case; in an a e age case, he size o Ykis much lowe .
Fu he mo e, he size o (Yk) is no mally signi ican ly lowe han he size o
Yksince only he con ollable sequences a e in he domain o .
The cons uc ion o Ykis s aigh o wa d, so we illus a e only he cons uc ion
o he es ans o ma ion wi h an example. Conside again ule applica ion
mode is maximal pa allelism o kΦ and he asynch onous mode o he aul
model. Conside he sequences s0=λ,s1= 2,s2=s1 4,s3=s2 4,s4=
s3 4,s5=s4 1and s6=s5 1. By ule (1) o De ini ion 16, (s0) = x0=ab.
As ab =⇒ 2bc, by ule (2) (s1) = ab bc. Simila ly, as bc =⇒ 4bc2, by ule
(2) (s2) = ab bc bc2. On he o he hand 4canno be applied in con igu a ion
bc2in he maximally pa allel mode, bu bc2=⇒ 4
F M bc3(in he asynch onous
mode) and so, by ule (2), (s3) = ab bc bc2bc3. Fu he mo e, bc3=⇒ 4
F M bc4
and so, by ule (3) o De ini ion 16, (s4) = (s3) = ab bc bc2bc3. As 1canno
be applied in bc4, by ule (4) (s5) is unde ined. Fu he mo e, by ule (5), (s6)
is also unde ined, so no es sequences will be gene a ed o s5and s6.
5 Conclusions
This pape p esen s a es ing app oach o ke nel P sys ems ha , unde ce ain
condi ions, ensu es ha he implemen a ion con o ms o he speci ica ion. The
me hodology is based on he iden i iable ke nel P sys ems concep , which is es-
sen ial o es ing, and has been in oduced o one-compa men kP sys ems wi h
ew i ing ules, bu could be ex ended.

Tes ing Iden i iable Ke nel P Sys ems 95
Acknowledgemen s
This wo k is suppo ed by a g an o he Romanian Na ional Au ho i y o Scien-
i ic Resea ch, CNCS-UEFISCDI, p ojec numbe PN-III-P4-ID-PCE-2016-0210.
Re e ences
1. Ag igo oaiei, O., Ciobanu, G.: Fla ening he ansi ion P sys ems wi h dissolu ion.
In: Gheo ghe, M., Hinze, T., Paun, G., Rozenbe g, G., Salomaa, A. (eds.) Memb ane
Compu ing - 11 h In e na ional Con e ence, CMC 2010, Jena, Ge many, Augus 24-
27, 2010. Re ised Selec ed Pape s. Lec u e No es in Compu e Science, ol. 6501,
pp. 53–64. Sp inge (2010), h ps://doi.o g/10.1007/978-3-642-18123-8_7
2. Cˆampeanu, C., Sˆan ean, N., Yu, S.: Minimal co e -au oma a o ini e languages.
In: In e na ional Wo kshop on Implemen ing Au oma a. pp. 43–56. Sp inge (1998),
h ps://doi.o g/10.1007/3-540-48057-9_4
3. Cˆampeanu, C., San ean, N., Yu, S.: Minimal co e -au oma a o ini e languages.
Theo e ical Compu e Science 267(1-2), 3–16 (2001), h ps://doi.o g/10.1016/
S0304-3975(00)00292-9
4. Chow, T.S.: Tes ing so wa e design modeled by ini e-s a e machines. IEEE T ans-
ac ions on So wa e Enginee ing 4(3), 178–187 (1978), h ps://doi.o g/10.1109/
TSE.1978.231496
5. D agomi , C., Ipa e, F., Konu , S., Le ica u, R., Mie la, L.: Model checking ke nel p
sys ems. In: Alhazo , A., Cojoca u, S., Gheo ghe, M., Rogozhin, Y., Rozenbe g, G.,
Salomaa, A. (eds.) Memb ane Compu ing. Lec u e No es in Compu e Science, ol.
8340, pp. 151–172. Sp inge Be lin Heidelbe g (2014), h ps://doi.o g/10.1007/
978-3-642-54239-8_12
6. Eilenbe g, S.: Au oma a, languages, and machines. Academic p ess (1974)
7. F eund, R., Lepo a i, A., Mau i, G., Po eca, A.E., Ve lan, S., Zand on, C.: Fla -
ening in ( issue) P sys ems. In: Alhazo , A., Cojoca u, S., Gheo ghe, M., Ro-
gozhin, Y., Rozenbe g, G., Salomaa, A. (eds.) Memb ane Compu ing. Lec u e No es
in Compu e Science, ol. 8340, pp. 173–188. Sp inge Be lin Heidelbe g (2014),
h ps://doi.o g/10.1007/978-3-642-54239-8_13
8. Gheo ghe, M., Ipa e, F.: Iden i iable ke nel P sys ems. Submi ed (2018)
9. Gheo ghe, M., Ipa e, F., D agomi , C., Mie la, L., Valencia-Cab e a, L., Ga c´ıa-
Quismondo, M., P´e ez-Jim´enez, M.J.: Ke nel P Sys ems - Ve sion I. Ele en h B ain-
s o ming Week on Memb ane Compu ing (11BWMC) pp. 97–124 (2013), h p:
//www.gcn.us.es/ iles/11bwmc/097_gheo ghe_ipa e.pd
10. Gheo ghe, M., Ipa e, F., Konu , S.: Tes ing based on iden i iable P sys ems using
co e au oma a and X-machines. In o ma ion Sciences 372, 565–578 (2016), h ps:
//doi.o g/10.1016/j.ins.2016.08.028
11. Gheo ghe, M., Ipa e, F., Le ica u, R., P´e ez-Jim´enez, M.J., Tu canu, A., Valencia-
Cab e a, L., Ga c´ıa-Quismondo, M., Mie la, L.: 3-col p oblem modelling using simple
ke nel P sys ems. In e na ional Jou nal o Compu e Ma hema ics 90(4), 816–830
(2013), h ps://doi.o g/10.1080/00207160.2012.743712
12. Ipa e, F.: Bounded sequence es ing om de e minis ic ini e s a e machines. Theo-
e ical Compu e Science 411(16-18), 1770–1784 (2010), h ps://doi.o g/10.1016/
j. cs.2010.01.030
96 M. Gheo ghe e al.
13. Ipa e, F., Gheo ghe, M.: Fini e s a e based es ing o P sys ems. Na u al Compu ing
8(4), 833 (2009), h ps://doi.o g/10.1007/s11047-008-9099-3
14. Ipa e, F., Gheo ghe, M.: Tes ing non-de e minis ic s eam X-machine models and
P sys ems. Elec onic No es in Theo e ical Compu e Science 227, 113–126 (2009),
h ps://doi.o g/10.1016/j.en cs.2008.12.107
15. Ipa e, F., Gheo ghe, M., Le ica u, R.: Tes gene a ion om P sys ems using model
checking. Jou nal o Logic and Algeb aic P og amming 79(6), 350–362 (2010), h ps:
//doi.o g/10.1016/j.jlap.2010.03.007
16. Le ica u, R., Gheo ghe, M., Ipa e, F.: An empi ical e alua ion o P sys em es ing
echniques. Na u al Compu ing 10(1), 151–165 (2011), h ps://doi.o g/10.1007/
s11047-010-9188-y
17. P˘aun, G.: Compu ing wi h memb anes. Tech. ep., Tu ku Cen e o Compu e Sci-
ence (1998), h p:// ucs. i/publica ions/ iew/?pub_id= Paun98a
18. P˘aun, G.: Compu ing wi h memb anes. Jou nal o Compu e and Sys em Sciences
61(1), 108–143 (2000), h ps://doi.o g/10.1006/jcss.1999.1693
19. The P sys ems websi e. h p://ppage.psys ems.eu, [Online; accessed 12/05/2018]
20. Ve lan, S.: Using he o mal amewo k o P sys ems. In: Alhazo , A., Cojoca u,
S., Gheo ghe, M., Rogozhin, Y., Rozenbe g, G., Salomaa, A. (eds.) Memb ane Com-
pu ing. Lec u e No es in Compu e Science, ol. 8340, pp. 56–79. Sp inge Be lin
Heidelbe g (2014), h ps://doi.o g/10.1007/978-3-642-54239-8_6