Elektrotehniški vestnik 84(5): 268-276, 2017 Original scientific paper
Formalna specifikacija in verifikacija lastnosti uravnavanja laktoznega operona z orodjem EST
Rok Vogrin, Robert Meolic, Tatjana Kapus
Univerza v Mariboru, Fakulteta za elektrotehniko, računalništvo in informatiko, Koroška c. 46, 2000 Maribor, Slovenija
E-pošta: rok.vogrin@student.um.si, robert.meolic@um.si, tatjana.kapus@um.si
Povzetek. Zaradi velike kompleksnosti bioloških sistemov potekajo intenzivne raziskave uporabnosti formalnih metod za modeliranje in analizo reakcij v njih. Eden najpreprostejših organizmov, ki jih lahko proučujemo, je bakterija Escherichia coli. V zvezi z njo je bilo prvič uporabljeno poimenovanje operon za osnovno enoto prepisovanja genov. Eden najbolj raziskanih operonov je laktozni operon pri tej bakteriji. V članku je predstavljena uporaba orodja EST za formalno specifikacijo in verifikacijo kvalitativnih lastnosti sistema uravnavanja laktoznega operona. Sistem smo specificirali s procesno algebro. Glavni prispevek je specifikacija lastnosti s temporalno logiko ACTLW in njihova verifikacija z metodo preverjanja modelov.
Ključne besede: sistemska biologija, uravnavanje izrazanja genov, formalne metode, procesna algebra, temporalna logika, preverjanje modelov
Formal specification and verification of properties of lactose operon regulation by using the EST toolbox
The growing interest in understanding biological systems has led to intensive research of the applicability of formal methods for modelling and analysis of reactions in these systems. One of the simplest organisms that can be investigated is bacterium Escherichia coli, in connection to which the term operon has first been coined to describe the basic unit of the gene transcription. One of the best-understood operons is the lactose operon of that bacterium. In this paper, a formal specification and verification of qualitative properties of the lactose-operon regulation system by using the EST toolbox are presented. The system is specified with a process algebra. The main contribution of this paper are the specification of the properties with temporal logic ACTLW and their verification by using model checking.
Keywords: systems biology, gene expression regulation, formal methods, process algebra, temporal logic, model checking
1 UVOD
Sistemska biologija obravnava biološke sisteme kot skupke komponent, ki med seboj komunicirajo, in raziskuje interakcije med komponentami ter njihov vpliv na lastnosti sistemov. V bioloških sistemih tipično opazimo verige socasnih procesov in podprocesov. Zaradi kompleksnosti zahtevajo posebne metode za modeliranje in analizo [1]. Razvite so bile metode matematicnega modeliranja v obliki sistemov diferencialnih enacb, v katerih so sestavni deli procesov opisani s spremenljivkami [2]. V [3] navajajo, daje z modeli z enacbami tezko
ugotavljati lastnosti bioloških sistemov in primerjati razlicne sisteme med seboj.
Formalne metode za preverjanje pravilnosti obnašanja sistemov s socasnostjo predpisujejo strogo matematicno definiran jezik za specifikacijo sistema, prav tako strogo definiran jezik za specifikacijo pricakovanih lastnosti sistema in nacin preverjanja, ali specificirani sistem ima pricakovane lastnosti. Veliko formalnih metod temelji na modalnih in temporalnih logikah ter razlicšnih procesnih algebrah [4]. V preteklosti so se uporabljale vecinoma za verifikacijo racunalniških programskih in strojnih sistemov, zdaj pa se uporabljajo tudi na netehnicnih podrocšjih, kot je modeliranje in analiza biolosških sistemov. Raziskovalci pricakujejo, da bo delo na tem podrocju pripeljalo do razvoja tehnik, ki bodo robu-stnejše, ucinkovitejše in zanesljivejše [1]. V nasprotju z matematicšnimi modeli z diferencialnimi enacšbami, ki so v osnovi namenjeni analizi kvantitativnih lastnosti bi-olosških sistemov, so formalne metode posebej primerne za analizo kvalitativnih lastnosti le-teh [2]. Ena najbolj uveljavljenih formalnih metod za analizo kvalitativnih lastnosti sistemov s socasnostjo je preverjanje modelov. Uporabljena je tudi v pricujocem clanku. Ta metoda avtomaticšno preveri, ali sistem s koncšnim sštevilom stanj ima lastnosti, podane v obliki formul temporalne logike.
EST (Efficient Symbolic Tools, http://est. meolic.com/) [5] je orodje za formalno specifikacijo in verifikacijo sistemov. Omogoca formalno verifikacijo sistemov z metodo preverjanja ekvivalence in z metodo preverjanja modelov. Algoritmi za verifikacijo so sim-bolicni in delujejo s pomocjo binarnih odlocitvenih grafov [4]. Zapis specifikacije sistema je mogoc z jezikom, podobnim procesni algebri Calculus of Communicating
Systems (CCS) [6], za specifikacijo lastnosti pa sta na voljo temporalni logiki ACTL (Action-based Computation Tree Logic - akcijska logika dreves izvajanj) in ACTLW (ACTL with Unless operator - ACTL z operatorjem unless) [7].
Bakterija E. coli (Escherichia coli) je eden najbolj raziskanih organizmov v biologiji, zato je postala model za preskušanje novih tehnologij [8]. V zvezi z njo je bilo prvic uporabljeno poimenovanje operon za osnovno enoto prepisovanja genov [3]. Za proučevanje novih metod modeliranja bioloških sistemov se pogosto uporablja uravnavanje laktoznega operona pri tej bakteriji. Za preskus metode preverjanja modelov je ze bilo uporabljeno v [3], kjer je sistem specificiran v jeziku CCS, lastnosti pa z razlicico ^-racuna, obogateno z operatorji CTL (Computation Tree Logic - logika dreves izvajanj), vendar je dvomljiva predvsem popolnost specifikacije nekaterih lastnosti. Cilj našega dela je bil za specifikacijo in verifikacijo uporabiti orodje EST in za specifikacijo lastnosti ACTLW. Skušali smo napisati popolne specifikacije lastnosti, predlaganih v [3], dodali pa smo tudi nove.
S problemom uravnavanja laktoznega operona pri bakteriji E. coli so se na podoben nacin ukvarjali tudi avtorji clanka [9], ki so definirali nekoliko manjši model in zgolj nekaj lastnosti. Za specifikacijo lastnosti so uporabljali formule temporalne logike CTL z nekaterimi omejitvami v sintaksi. V [10] je predlagan spet drugacen kvalitativen model in izrazšenih je nekaj lastnosti z logiko CTL. V [11] je specificiran kvantitativen model uravnavanja z jezikom Stochastic CLS in opisana analiza dveh kvantitativnih lastnosti, izrazšenih z linearno temporalno logiko (LTL - Linear Temporal Logic), po prevodu modela v Real-Time Maude.
(Članek je v nadaljevanju razdeljen takole. V razdelku 2 je okviren besedni opis delovanja uravnavanja laktoznega operona, privzetega v [3] in v tem clanku. V razdelku 3 je predstavljena formalna specifikacija sistema uravnavanja. V razdelku 4 je najprej predstavljena logika ACTLW, nato pa specifikacija lastnosti in rezultati verifikacije. Razdelek 5 vsebuje komentar rezultatov in predloge za nadaljnje delo.
2 Uravnavanje laktoznega operona
Bakterija E. coli dobro raste na gojišcu z glukozo [3]. Vzemimo, daje na gojišcu samo laktoza. V tem primeru bakterija tvori glukozo iz laktoze.
Laktozni operon bakterije E. coli sestavljajo geni Y, Z in A, laktozni promotor ter primarni operator in dva sekundarna [3]. Gen Y nosi zapis za encim galaktozid permeaza, gen Z pa za encim p-galaktozidaza. Prvi encim omogoca, da laktoza iz okolja prehaja v celico, drugi pa skrbi, da se iz laktoze tvorijo izomer laktoze alolaktoza ter glukoza in galaktoza. Promotor je del, ki lahko spodbudi prepisovanje genov, operatorji pa so segmenti, na katere se lahko vezše laktozni represor.
Pri uravnavanju laktoznega operona sodeluje se ciklični adenozin monofosfat (cAMP), ki deluje kot soaktivator cAMP-receptorskega proteina (CRP), ki je aktivatorski protein.
V odsotnosti alolaktoze v celici se represor veZe na primarni operator in na enega od sekundarnih ter pre-precuje prepisovanje genov oziroma geni se prepisujejo in tako encimi tvorijo samo na osnovni ravni. Promotor je reprimiran. Promotor lahko spodbuja prepisovanje genov, samo ce ni reprimiran in ce je hkrati aktiviran. Galaktozid permeaza poskrbi, da laktoza vstopa v celico, ^-galaktozidaza pa, da se iz nje tvori alolaktoza, ki se poveze na represor in s tem povzroci, da se le-ta odcepi od primarnega in sekundarnega operatorja. Promotor v tem primeru ni reprimiran, vendar se prepisovanje genov ne izvaja na najvišji ravni, ce ni aktiviran. Njegovo aktiviranje je odvisno od kolicine glukoze v celici.
Kadar je vsebnost glukoze v celici majhna oziroma nicelna, je kolicina cAMP velika. To privede do vezave CRP s cAMP in kompleksa CRP-cAMP prek CRP na mesto blizu promotorja ("CRP-mesto"). Promotor se aktivira. Ce ni reprimiran, spodbudi prepisovanje genov. S tem se poveca raven p-galaktozidaze ter tako glukoze v celici. p-galaktozidaza pa se pri razgradnji laktoze porablja in s tem se njena raven manjša.
Kadar kolicina glukoze v celici naraste, kolicina cAMP pade. CRP se odcepi od cAMP in z mesta pri promotorju. Posledica je dezaktiviranje promotorja. Raven p-galaktozidaze pade in tvorjenje glukoze iz laktoze je ustavljeno, vsaj dokler raven glukoze ne pade.
3 Specifikacija sistema v stilu jezika CCS
3.1 Definicija jezika, podobnega CCS
CCS [6] je procesna algebra, ki omogoca opisovanje in analiziranje obnasšanja sistema, sestavljenega iz vecš komponent. Te predstavimo s procesi, ki med seboj komunicirajo. Njihovo obnašanje je podano z akcijami, ki jih lahko izvedejo. Locimo zunanje akcije, ki so lahko vhodne (a) ali izhodne (a), in notranjo akcijo t. Pravimo, da sta akciji a in a med seboj komplementarni. Pri pisanju specifikacije sistema smo v osnovi uporabili formalizem z naslednjo sintakso, ki je podobna sintaksi jezika CCS [12]:
P ::= 0 | a.Pi | A | Pi + P2 | Pi|P2 | Pi\a
Zapis a.P1 pomeni proces, v katerem se lahko najprej izvede akcija a, nato pa proces Pi. 0 je prazen proces, to je tak, ki ne naredi nicesar. Namesto a.0 bomo pisali kar a. Z zapisom A = P definiramo, da je A ime procesa P. V procesu P lahko nastopa A, s cimer dosezemo, da se P ne konca, ampak se izvede ponovno. Torej lahko imamo rekurzijo. Kot primer lahko zapišemo P = a.b.P, kar pomeni, da proces P najprej izvede
Ent = \ELAC.React	(1)
React = \ ILAC.React2 + \ rbeta.React	(2)
React2 = \ ELAC.React + \ rbeta.React2	(3) Beta _galactosidase_low = ?rbeta. \ RBETA.\iallo. \ IALLO.Beta _galactosidase_low
+ ?ibeta.\IBETA.Beta_galactosidase_high	(4) Beta _galactosidase_high = ?rbeta. \ RBETA.\iglu.\IGLU.Beta_galactosidase_high
+ ?dbeta.\DBETA.Beta _galactosidase_low	(5)
Allolactose_none = ?iallo.Allolactose_low	(6)
Allolactose_low = ?iallo.Allolactose_low + ?ballo.Allolactose_none	(7) Neg = \ BOl.iTAU. \ BO2.\rep.\REP.\ballo. \ BALLO.\UBO1.\ UBO2.\urep\UREP.Neg
+ TAU.\BO3.\rep. \ REP.\ballo.\BALLO. \ UBO1. \ UBO3. \ urep. \ UREP.Neg) (8)
Promoter_iu = ?.rep.Promoter_ir + ?act.\ ibeta.Promoter_au	(9)
Promoter_ir = ?urep.Promoter_iu + ?.act.Promoter_ar	(10)
Promoter_au = ?rep.\dbeta.Promoter_ar + ?iact.\dbeta.Promoter_iu	(11)
Promoter_ar = ?urep.\ibeta.Promoter_au + ?iact.Promoter_ir	(12)
Pos = \lev.(?low.\L_to_H.\BC.\BS.\act.\ACT.Act + ?high.Pos)	(13)
Act = \lev.(?low.Act + ?high.\H_to_L.\UBC. \ UBS.\iact. \ IACT.Pos)	(14) Glucose_high = ?.iglu.Glucose_high + ?lev. \ HIGH. \ high.Glucose_high
+ TAU.\DGLU.GlucoseJow	(15) Glucose_low = ?iglu.(TAU.Glucose_low + TAU.\GLU_L_to_H.Glucose_high)
+ ?lev. \ LOW. \ low.Glucose_low	(16)
raw net SpecFull =	\(Ent,Beta_galactosidase_low,Allolactosejnone,Neg,
Promoter_iu, Pos, Glucose_high)
\rbeta\iallo\ibeta\iglu\dbeta\ballo\rep\urep\act\iact\lev\low\high	(17)
Slika 1: Abstraktna specifikacija sistema (SpecFull)
vhodno akcijo a, za njo izhodno akcijo b, nato pa se ponovno obnaša kot P.
V procesu se lahko izbere, katera akcija se bo izvedla. To omogoča operator "+". Primer je proces P = a + b, kjer se lahko izvede vhodna ali izhodna akcija (nato pa se v obeh primerih proces konca).
Izvedba komponent sistema je lahko vzporedna. Vzporednost izrazimo z znakom "|" za paralelno kompozicijo, na primer (a.P)|(a.Q). Komunikacija med procesoma v paralelni kompoziciji je mogocša prek akcij, iz katerih sta sestavljena. Procesa lahko izvedeta komunikacijo, ce sta v njiju hkrati omogoceni med seboj komplementarni akciji, kakor v nasšem primeru. Procesa lahko hkrati izvedeta akcijo a in a, vendar se ta komunikacija oznaci z notranjo akcijo t, in prvi proces nadaljuje kot P, drugi pa kot Q. Komunikacija pa ni edina moznost. Levi proces lahko sam izvede akcijo a in nadaljuje kot P, pa tudi desni proces lahko sam izvede akcijo a in nadaljuje kot Q. Ce hocemo doseci, da se v nasšem primeru lahko izvede samo komunikacija, to storimo z operatorjem "\" za prepoved akcij.
Z zapisom Pi\a prepovemo, da bi se kdaj izvedla akcija a ali njej komplementarna akcija v procesu P1. S tem tudi preprecimo, da bi proces P1 komuniciral s
katerimkoli procesom prek akcije a ali a. Torej zapis ((a.P)|(a.Q))\a pomeni proces, ki najprej izvede notranjo akcijo t, nato pa nadaljuje kot proces (P|Q)\a. Recemo tudi, da je akcija a (in njen komplement) v procesu ((a.P)|(a.Q))\a skrita, saj je edina moznost, da nastopa v notranji komunikaciji.
3.2 Specifikacija sistema uravnavanja laktoznega operona
V [3] sta podani specifikacija sistema SystemFull in abstraktna specifikacija SpecFull. Specifikacija sistema uravnavanja, ki smo jo napisali v EST-u in jo uporabili za preverjanje vecšine lastnosti, je skoraj enaka specifikaciji SystemFull iz [3]. Zaradi njene dolzine je na sliki 1 namesto nje prikazana abstraktna specifikacija SpecFull, napisana za EST. Je paralelna kompozicija procesov Ent, Beta_galactosidase_low, Allolactose_none, Neg, Promoter_iu, Pos in Glucose_high. SystemFull se od nje razlikuje v tem, da namesto vsakega od procesov Ent, Neg in Pos vsebuje dva procesa ali vec. Procesi Beta_galactosidase_low, Allolactose_none, Promoter_iu in Glucose_high predstavljajo ^-galaktozidazo, alolaktozo, promotor oziroma glukozo iz neformalnega opisa. Proces Ent pov-
zema skupno obnašanje procesov, ki predstavljajo laktozo na gojišču, laktozo v celici in galaktozid permeazo v specifikaciji SpecFull. Neg ("negativno uravnavanje") opisuje skupni ucinek obnašanja procesov, ki v zadnji predstavljajo laktozni represor in vsakega od treh operatorjev (te v nadaljevanju oznacimo z O1, O2 in O3). Pos ("pozitivno uravnavanje") pa specificira skupni ucinek obnašanja procesov, ki v njej predstavljata CRP in cAMP. Imena procesov v paralelni kompoziciji so hkrati zacetna stanja teh procesov in tako vidimo, kakšno zacetno stanje je privzeto za katero snov v sistemu. Na sliki 1 vidimo, da opis procesa Glucose_high sestoji iz štirih vrstic in da ima poleg zacetnega še stanje Glucose_low. Privzeto je torej, da je v zacetku izvajanja raven glukoze v celici visoka. Vzeto je še, da je kolicina ,0-galaktozidaze majhna, da v celici ni alolaktoze, da je promotor neaktiviran in nereprimiran, da represor ni povezan na operatorje in da so torej prosti, iz SystemFull [3] pa je razvidno, daje privzeto, daje laktoza ves cas na gojišcu in da obstaja nespremenljiva kolicšina galaktozid permeaze, da na zacšetku ni laktoze v celici ter da je malo cAMP, da ni povezan s CRP in da CRP ni povezan na promotor.
Orodje EST za branje uporablja razpoznavalnik za specifikacije CCS z nekoliko spremenjeno sintakso. Vhodno akcijo oznacimo z "?", izhodno pa s "!". Primer izhodne akcije na sliki 1 je !iglu, vhodne pa ?iglu. Za notranjo akcijo t uporabimo TAU. Za tvorjenje paralelne kompozicije uporabimo pri njenem imenu rezervirano besedo net. Z besedo raw pa povemo EST-u, da za kompozicijo ni treba izracunati pomoznih struktur za nadaljnje sestavljanje.
V specifikaciji nastopajo akcije za komunikacijo znotraj sistema, ki jih pišemo z malimi crkami (na primer iallo), akcija t in zunanje akcije sistema (na primer
IALLO). Na sliki 1 vidimo, da so vse akcije za komunikacijo znotraj sistema prepovedane in se torej skrijejo za akcijami t. Zunanje akcije so, kot obicajno
v specifikacijah CCS, uporabljene kot sonde, ki povedo, kaj se je kdaj zgodilo v notranjosti sistema, saj sicer ne bi mogli specificirati pricakovanih lastnosti sistema. Tako kot v [3] so izhodne. Akcija IALLO se na primer v sistemu lahko zgodi takoj za iallo v procesu Beta_galactosidase_low in tako takoj za komunikacijo le-tega s procesom Allolactose_none prek akcije iallo ter pove, da je nastala alolaktoza. Akcija t je v procesih uporabljena za modeliranje obnašanja, ki ni odvisno od drugih procesov ali je nedeterministicšno. V procesu Glucose_high na primer vidimo, da ko je raven glukoze visoka, se lahko samodejno znizša. To predstavlja porabo glukoze v celici. Ko pa je raven glukoze nizka, se lahko zgodi akcija iglu, ki na splošno pomeni zvišanje ravni, povzroceno z ,0-galaktozidazo (akcija iglu), vendar je s pomocjo notranje akcije specificirano, da ostane raven nespremenjena ali pa se povisša. Tako je narejeno zato, ker je kolicšina glukoze modelirana kvalitativno samo z
dvema ravnema in naj bi bilo specificirano, da raven še ni tako narasla, da bi bila ze oznacena kot visoka ("high") in ne kot nizka ("low").
V specifikaciji sistema tako kot v [3] nastopajo naslednje zunanje akcije:
ELAC
ILAC
RBETA
IALLO
IBETA
DBETA
IGLU
vstop laktoze v celico povečanje količine laktoze v celici zmanjšanje kolicine laktoze v celici povecanje kolicine alolaktoze povecanje kolicine p-galaktozidaze zmanjšanje kolicine p-galaktozidaze tvorjenje glukoze vezava represorja na O1 vezava represorja na O2 vezava represorja na O3 represor vezan na operatorja represor odcepljen od operatorjev vezava alolaktoze na represor odcep represorja od O1 odcep represorja od O2 odcep represorja od O3 vezava cAMP na CRP vezava CRP-cAMP na CRP-mesto aktiviranje promotorja odcep cAMP od CRP odcep CRP s CRP-mesta dezaktiviranje promotorja povecanje kolicine cAMP zmanjšanje kolicine cAMP zmanjšanje kolicine glukoze GLU_L_to_H povecanje kolicine glukoze
Za potrebe preverjanja lastnosti smo dodali še akciji
BO1
BO2
BO3
REP
UREP
BALLO
UBO1
UBO2
UBO3
bc
BS
ACT
UBC
UBS
I ACT
L_to_H
H_to_L
DGLU
HIGH in LOW, ki kazeta raven glukoze v celici.
Orodje EST ne omogoca izrazov oblike a.(Ai + A2), kjer sta A1 in A2 imeni procesov. Takšna izraza sta v specifikaciji SystemFull v [3] uporabljena za specifici-ranje, da po neki akciji a proces, ki predstavlja laktozo v celici, sam odloci, ali se bo njena raven spremenila ali ne. Namesto tega smo uporabili zapis a.A1 + a.A2, kar samo prestavi trenutek odlocanja in ne vpliva na preverjane lastnosti.
4 Preverjanje modelov z ACTLW
4.1 Definicija ACTLW
ACTLW [7] je izjavna temporalna logika razvejanega cšasa. Definirana je nad oznacšenim sistemom prehajanja stanj (LTS - Labelled Transition System). LTS je cetverica M = (S,ActT,D,sinit), v kateri je S mnozica vseh stanj, ActT mnozica, ki vsebuje vsaj notranjo akcijo, lahko pa še zunanje, D C S x ActT x S prehajalna relacija in sinit g S zacetno stanje. LTS M je koncen, ce in samo ce sta mnozici S in ActT
a = a a = -X a = X V s =m true s =m s =m ^ V s =m EE y s =m AA Y n =m [{xV U {x>'j
n=m [{xV W {X>'j,
ce in samo ce a = a;
ce in samo Ce a = x;
Ce in samo Ce a = x ali a = x';
vedno;
Ce in samo Ce s =m y>;
Ce in samo Ce s =m ^ ali s =m <£>';
Ce in samo Ce v M obstaja polna pot n, za katero velja n(0) = s in n =m y; Ce za vse polne poti n v M velja n(0) = s n =m y ; Ce in samo Ce len(n) > 1 in obstaja tak i, 1 < i < len(n), da n(i) =m <£>' in n(i) G D/x//(n(i-1))
ter za vsak 1 < j < i-1 velja n(j) =m ^ in n(j) G D/x/(n(j-1)); Ce in samo Ce n =m [{x}^ U {x'}^']
ali pa za vsak i, 1 < i < len(n), velja n(i) =m ^ in n(i) G D/x/(n(i-1)).
Slika 2: Definicija pomena operatorjev pri temporalni logiki ACTLW; za podane izraze velja a e ActT in /x/ = {a | a = x}.
koncni. Trojka (s, a, s') G D se imenuje prehod z akcijo a iz stanja s v stanje s', pri cemer se prehod z akcijo t imenuje tudi notranji prehod. Pot n v LTS-ju je koncno ali neskončno zaporedje stanj in akcij s0, ai, si, a2, s2,..., ki se zacne v stanju s0 in v katerem za vsaki zaporedni stanji si-1 in si velja (si-1, a.j, sž) G D. Eno stanje na poti n oznacimo s n(i), pri cemer je n(0) prvo stanje na poti, stanje n(i+1) pa tisto, ki neposredno sledi stanju n(i). Dolzina poti je število stanj na poti n in jo oznacimo z len(n). Dolzina neskoncne poti je w.
CCe obstaja (s, a, s') G D, potem je stanje s' naslednik stanja s. Z oznako DA(s) oznacimo mnozico vseh naslednikov stanja s, ki so dosegljiva s prehodom, ki vsebuje akcijo iz mnozice A. Stanje brez naslednikov se imenuje zagatno stanje. Neskoncne poti in koncne poti, ki se koncajo v zagatnem stanju, imenujemo polne poti.
Skladnja formul ACTLW ^ (imenovanih tudi formule stanja) nad M-jem je definirana z naslednjo slovnico, pri cemer je x formula akcije, a G ActT, y formula poti, EE in AA sta kvantifikatorja poti, U in W pa temporalna operatorja until in unless:
X ::= a | —x | x v X
::= true | —^ | ^ V ^ | EE y | AA y Y ::= [{xV U {xM | [{xV W {xM
Pomen formul ACTLW je induktivno definiran s pravili na sliki 2. Z a = x oznacimo, da akcija a zadošca formuli akcije x, s s =m y>, da formula stanja ^ velja v stanju s, s n =m Y pa, da formula poti Y velja na polni poti n. Formulo a V —a, v kateri je a G ActT poljubno izbrana akcija, krajše zapišemo kot true. Namesto —true v formulah akcije in formulah stanja pišemo false. Operator A je definiran kot x A x' = —(—x V —x') oziroma ^ A y>' = — (—^ V —y>'). Ce a = x, prehod (s, a, s') imenujemo x-prehod, ce a = x in s' =m y>, pa prehod (s, a, s') imenujemo (x, -prehod. Formula ACTLW ^ velja v LTS-ju M (to oznacimo z M = y), ce in samo ce sinit =m ¥>.
Iz definicije skladnje formul ACTLW sledijo operatorji EEU, EEW, AAU in AAW. Dodatno definiramo izpeljane operatorje ACTLW EEF, AAF, EEG in AAG:
EEF{x}^> = EE[{true}true U {xM AAF{x}^ = AA[{ true}true U {x}^j EEG{x}^ = EE[{x}^ W {false}false] AAG{x}^ = AA[{xV W {false}false]
Na splošno je vsak operator ACTLW sestavljen tako, da kvantifikatorju poti EE ali AA pridruzimo tempo-ralni operator F, G, U ali W. Pomen teh neformalno razlozimo takole. Za formulo poti F{x}^> velja, da je zadošcena na polni poti, ce in samo ce na njej obstaja (x, -prehod (slika 3). Formula G{x}^ je zadošcena na polni poti, ce in samo ce so vsi prehodi na njej (x, -prehodi. To ilustrira slika 4, ki hkrati prikazuje primera veljavnosti formul ACTLW v LTS-jih. V prvem velja formula EEG{x}^, v drugem pa tudi AAG{x}^. Formula [{x}^ U {x'}^'j je zadošcena na polni poti, ce in samo ce se ta zacne s koncnim zaporedjem (x, -prehodov, ki mu sledi (x', y>')-prehod. Formula [{x}^ W {x>'j je zadošcena na polni poti, ce in samo ce je na tej poti zadošcena formula [{x}^ U {x'}^'j ali formula G{x}^.
Slika 3: Pomen formule poti F{x}^
Zapis formul ACTLW lahko dodatno okrajšamo s skladenjskimi okrajsšavami, pri katerih namesto {x}true zapišemo samo {x}, namesto {true}^ pa samo Tukaj je nekaj primerov:
X
X
¥
¥
¥
Slika 4: Pomen formul ACTLW EEG{x}^ in AAG{x}^ v LTS-ju
EEF{x} = EEF{x}true
EEF ¥ = EEF{true
EEg{x} = EEG{x}true
EEG ¥ = EEG{ true}¥
EE[{x} U {x'}] = EE[{x}true U {x'}true]
EE[¥ U ¥'] = EE [{true }¥ U {true }¥']
4.2 Formalna verifikacija uravnavanja laktoznega operona
Pričakovane lastnosti sistema, opisanega z našo specifikacijo SystemFull, smo specificirali s formulami AC-TWL in z metodo preverjanja modelov v EST-u ugotovili, ali jim sistem zadošca. V EST-u se opis sistema s procesno algebro najprej pretvori v LTS. Preverjanje modelov za izbrano formulo ACTLW deluje tako, da se poišce mnozica vseh stanj, v katerih formula velja, nato pa preveri, ali je zacetno stanje LTS-ja v tej mnozici. V [3] porocajo, da jim z orodjem CWB-NC in s 4 GB RAM-a ni uspelo tvoriti LTS-ja. Po vec kot dveh urah je orodju zmanjkalo pomnilniškega prostora. V EST-u nam ga je uspelo tvoriti v trenutku, pa tudi potrebe po vecji kolicšini pomnilnika ni bilo. Naslednja tabela prikazuje število stanj in prehodov dobljenega LTS-ja brez akcij HIGH in LOW (S1) ter z njima (S2) (cas tvorjenja je bil izmerjen na racunalniku s procesorjem Intel Core i5-4250U pri frekvenci 1,2 GHz):
sistem	stanja	prehodi	cas	porabljeni
			tvorjenja	pomnilnik
S1	440700	2156768	1,15 s	55 MiB
S2	460164	2235304	1,24 s	55 MiB
V osnovi locimo varnostne in živostne lastnosti sistemov. Varnostna lastnost pove, da se na nobeni poti v LTS-ju nikoli ne zgodi nic slabega, živostna pa, da se na vsaki poti nekoc zgodi nekaj dobrega.
Najpomembnejsše je preveriti varnostne lastnosti. Najprej smo preverili, da v sistemu ni zagatnih stanj, saj pricakujemo, da se nikoli ne ustavi. To smo preverili s formulo EEX{true} AND AAG EEX{true}. Formula EEX{true} je definirana kot EE[{/alse} / alse U {true}true] in v stanju velja, ce in samo ce ima to naslednika. Ce EST ugotovi, da sistem ne zadošca formuli, lahko izpiše protiprimer, tj. zaporedje akcij, ki krši trditev, opisano s formulo. Sledi besedni opis pomembnih lastnosti uravnavanja, podanih na sliki 5 skupaj z rezultati preverjanja:
(A) S formulami pokazemo odnos med kolicino glukoze in cAMP.
(A21) Na vseh poteh se vedno, kadar je kolicina cAMP velika, zmanjša, samo ce prej naraste kolicšina glukoze. V nasprotju s pricakovanji ta formula ni veljavna. Tvorjeni protiprimer je pokazal, da se lahko zgodi, da proces, ki predstavlja cAMP (na sliki 1 je skrit v procesu Pos [3]), izvede akcijo lev in nato low skupaj s procesom glukoze, ko je ta nizka, nato raven glukoze naraste, tj. izvede se GLU_L_to_H, šele zatem pa proces cAMP izvede akcijo L_to_H (tj. raven cAMP naraste, ker je proces prej dobil informacijo, da je glukoza nizka). Nato cAMP izvede akcijo lev, dobi informacijo, da je glukoza visoka, in izvede akcijo H_to_L. Vzrok, da formula A21 ne velja, je v tem, da poizvedovanje o ravni glukoze in reakcija na informacijo ne tvorita nedeljive akcije. Tako sonda GLU_L_to_H ne izraza nujno ravni glukoze, ki je bila uposštevana pri spremembi ravni cAMP. Zato smo v procesu, ki predstavlja glukozo, uvedli sondazno akcijo HIGH (slika 1), ki jo izraza, saj se zgodi po poizvedovanju procesa cAMP po trenutni ravni glukoze prek akcije lev in pred akcijo high, ki cAMP-ju da odgovor. Tako lahko izrazimo naslednjo lastnost, ki je veljavna.
(A23) Na vseh poteh vedno, kadar je kolicina cAMP velika (tj. potem ko naraste), se zmanjša, samo ce je kolicina glukoze velika. To je varnostna formula in ne pove, ali bo raven cAMP padla. To izrazimo z zivostjo. (A40) Na vseh poteh vedno, kadar je kolicina cAMP velika, ko raven glukoze naraste, se zmanjša kolicina cAMP. Ta formula ne velja, ker obstajajo tudi poti, na katerih bi se lahko izvedla akcija H_to_L, vendar so omogocene tudi druge akcije, kot na primer vezava represorja na operatorja in nato odcep, kar se lahko nenehno izvaja. Zagotovo pa obstaja kakšna pot, na kateri se bo cAMP zmanjsšal. To izrazimo s formulo, ki jo dobimo iz zivostne z nadomestitvijo drugega operatorja
A	property	A21	== NOT EEF {!L_to_H} EE [{NOT !GLU_L_to_H} U {!H_to_L}]	FALSE
	property	A23	== NOT EEF {!L_to_H} Ee[{not !HIGH} U {!H_to_L}]	TRUE
	property	A40	== NOT EEF {!L_to_H} EEF {!HIGH} EEG {NOT !H_to_L}	FALSE
	property	A42	== NOT EEF {!LJO_H} EEF {!HIGH} AAG {not !H_to_L}	TRUE
B	property	B23	== NOT EEF {!H_to_L} EE [{NOT !LOW} U {!L_to_H}]	TRUE
	property	B2z	== AA[{NOT !L_to_H} W {!DGLU}]	TRUE
C	property	C1 =	== AAG EEF {!BC}	TRUE
D	property	D1 =	== NOT EEF {!H_to_L} EE[{NOT !L_to_H} U {!BC}]	TRUE
	property	D2 =	== NOT EEF {!L_to_H} Ee[{nOT !H_to_L} U {!UBC}]	TRUE
E	property	E14	== NOT EEF {!L_to_H} AAG {NOT !BC}	TRUE
	property	E15	== NOT EEF {!UBS} EE [{NOT !BC} U {!BS}]	TRUE
F	property	F11	== AAG EEF {!BS}	TRUE
	property	F12	== NOT EEF {!BC} AAG {NOT !BS}	TRUE
G	property	G2 =	== NOT EEF {!IACT} EE[{NOT !BS} U {!ACT}]	TRUE
K	property	K 1z	== AA[{NOT !IALLO} W {!RBETA}]	TRUE
	property	K13	== NOT EEF{ !BALLO} AAG {NOT !IALLO}	TRUE
L	property	L12 -	== AA[{NOT !IALLO} W {!ELAC}]	TRUE
M	property	M12	== NOT EEF {!IALLO} AAG {NOT !BALLO}	TRUE
N	property	N1 =	== NOT EEF {!REP} EE [{NOT !BALLO} U {!UREP}]	TRUE
O	property	O11	== AAG EEF {!BO1}	TRUE
	property	O12	== AAG EEF {!UBO1}	TRUE
U	property	U11	== NOT EEF {!BO2} EE [{NOT !UBO2} U {!BO3}]	TRUE
	property	U 21	== NOT EEF {!BOl} Ee[{nOT !BO2 AND NOT !BO3} U {!UBO1}]	TRUE
V	property	V 1z	== AA[{NOT !IBETA} W {!BS}]	TRUE
	property	V 2z	== AA[{NOT !BS} W {!BC}]	TRUE
	property	V 7 =	== NOT EEF {!IBETA} EE[{not !IACT AND NOT !REP} U {!DBETA}]	FALSE
	property	V 8 =	== NOT EEF {!DBETA} EE [{NOT !ACT AND NOT !UREP} U {!IBETA}]	FALSE
W	property	W 3 =	== NOT EEF {!DBETA} EE [{NOT !IBETA} U {!IGLU}]	TRUE
Y	property	Y12	== NOT EEF {!GLU_L_to_H} AAG {NOT !DBETA}	TRUE
Z	property	Z1 =	== NOT EEF {!DGLU} EE [{NOT !IGLU} U {!GLU_L_to_H}]	FALSE
Slika 5: Formule ACTLW za lastnosti uravnavanja
EE z operatorjem AA. Taksnim lastnostim pravimo lastnosti moZnosti [13]. (A42) Na vseh poteh vedno, kadar je količina cAMP velika, ko raven glukoze naraste, je mogoče, da se količina cAMP zmanjša.
(B)	(B23) pravi nasprotno kot A23. Na vseh poteh vedno, potem ko količina cAMP pade, naraste, samo če je količina glukoze majhna.
Ker je na začetku izvajanja sistema raven čAMP ze nizka, pa ta formula ne zajame začetnega dogajanja. To izraza naslednja formula.
(B2z) Na nobeni poti na začetku ne naraste količina čAMP, razen če prej ne pade raven glukoze.
(C)	Na vseh poteh je vedno mogoče, da se čAMP veze na CRP.
(D)	(D1) Na vseh poteh se čAMP vedno veze na CRP samo, če je raven čAMP visoka.
(D2) Na vseh poteh se čAMP vedno odčepi od CRP samo, če je raven čAMP nizka.
(E)	(E14) Na vseh poteh je vedno, kadar se količina čAMP poveča, mogoče, da se čAMP veze na CRP.
(E15) Na nobeni poti se nikoli, kadar se CRP odčepi s CRP-mesta, ne veze nanj, dokler se čAMP ne veze na CRP.
(F)	Na vseh poteh je vedno mogoče, da se CRP-čAMP veze na CRP-mesto.
(G)	Na vseh poteh se promotor vedno aktivira samo, če se prej CRP-čAMP veze na CRP-mesto.
(K) S formulami preverimo lastnosti alolaktoze. (K1z) Na nobeni poti se na začetku ne zviša raven alolaktoze, dokler ne nastopi reakčija
laktoze in fi-galaktozidaze, ki zmanjša količino laktoze.
(K13) Na vseh poteh je vedno, kadar se raven alolaktoze zmanjša, mogoče, da se nekoč poveča.
(L) Na nobeni poti se na začetku ne poveča količina alolaktoze, če v čeličo ne vstopi laktoza.
(M) Na vseh poteh je vedno, če obstaja alolaktoza v čeliči, mogoče, da se veze na laktozni represor. (N) Na vseh poteh, kadarkoli je promotor reprimiran, ne postane nereprimiran, razen če se na represor ne veze alolaktoza. (O) S formulami preverimo lastnosti vezave laktoz-nega represorja na operatorje. Enako kot za O1 lahko zapišemo še za O2 in O3.
(011)	Na vseh poteh je vedno mogoče, da se laktozni represor vezše na O1.
(012)	Na vseh poteh je vedno mogoče, da se laktozni represor odčepi od O1.
(U) S formulami preverimo lastnosti operatorjev. (U11) Na vseh poteh se vedno, kadar se represor veze na O2, od njega odčepi, preden se veze na O3.
(U21) Na nobeni poti se nikoli, kadar se laktozni represor veze na O1, ne odčepi, dokler se ne veze na O2 ali na O3. (V) S formulami preverimo lastnosti fi-galaktozidaze.
(V1z) Na nobeni poti količina fi-galaktozidaze ne naraste, če se CRP-čAMP ne veze na CRP-mesto.
(V2z) Na nobeni poti se CRP-čAMP ne veze na CRP-mesto, dokler se čAMP ne veze na CRP.
(V7) Na vseh poteh vedno, kadar je količina fi-galaktozidaze velika, pade, samo če promotor postane dezaktiviran ali reprimiran. (V8) Na vseh poteh vedno, kadar je količina fi-galaktozidaze majhna, naraste, samo če promotor postane aktiviran ali nereprimiran. (W) Na vseh poteh se vedno, če je raven fi-galaktozidaze nizka, glukoza lahko tvori, samo če raven fi-galaktozidaze postane visoka. (Y) Na vseh poteh je vedno, kadar količšina glukoze naraste, mogoče, da se zmanjša količina fi-galaktozidaze. (Z) Na vseh poteh vedno, kadar raven glukoze pade, ne naraste, dokler se iz laktoze v čeliči ne tvori glukoza.
Samo na prvi pogled je presenetljiva neveljavnost formul V7, V8 in Z1 na sliki 5. Vzrok je podobno kot pri A21 to, da v modelu ni zagotovljeno, da se sondazšna akčija izvede takoj po komunikačiji, za katero igra vlogo sonde. Da bi to vsaj delno zagotovili, smo v spečifikačiji SystemFull uporabili podoben prinčip kot pri akčijah
HIGH in LOW. Na sliki 1 vidimo, da je pri njiju akcija high oziroma low nekakšna potrditev zahteve lev, ki poskrbi, da se komunicirajoča procesa ne nadaljujeta, dokler se poizvedovanje, vključno z izvedbo sonde, ne konča. Tako smo za vsako zunanjo nesondazno akcijo, takoj za katero je v procesu napisana sondazna akcija, uvedli potrditveno zunanjo nesondazno akcijo. To je, za vse prepovedane akcije specifikacije SystemFull razen za ubo23e, acte in iacte ter lev, low in high smo uvedli še akcijo z enakim imenom z dodano predpono ack in tudi potrditvene akcije pri kompoziciji prepovedali. V procesih pa smo jih uporabili takole. Vzemimo, da v enem procesu nastopa zaporedje akcij a.s, pri cemer je a zunanja vhodna nesondazna akcija, s pa sondazna, v drugem pa akcija a, komplementarna akciji a. Potem smo v prvem procesu namesto a.s napisali zaporedje akcij a.s.acka, pri cemer je acka potrditvena akcija akcije a, v drugem pa a.acka namesto a. Analogno smo storili, ce je bil a v prvem procesu izhodna, v drugem pa vhodna akcija (dejansko ni pomembno, v katerem od obeh procesov je potrditvena akcija vhodna, v katerem pa izhodna). Tako se je na primer zaporedje ?dbeta. ! D BET A v procesu Beta_galactosidase_high (slika 1) spremenilo v ?dbeta. ! DBETA. ! ackdbeta, na obeh mestih v procesu Promoter_au pa smo za akcijo !dbeta dodali ?ackdbeta. Tudi LTS za novo specifikacijo SystemFull se je tvoril hitro (3,55 s), imel pa je 1379904 stanj in 6405300 prehodov. EST je za tvor-jenje LTS-ja porabil 106 MiB pomnilnika. Preverjanje lastnosti je za novo specifikacijo trajalo 8,12 s, v sistemu S1 in S2 pa 3,92 s oziroma 4,51 s. EST za preverjanje lastnosti ne zahteva rezervacije dodatnega pomnilnika.
V	novi specifikaciji so formule V7, V8 in Z1 veljavne, veljavnost preostalih formul s slike 5 pa se ne spremeni.
5 SKLEP
V	clanku smo izvedli formalno verifikacijo uravnavanja laktoznega operona. Neformalno smo opisali obnasšanje in lastnosti biološkega procesa v bakteriji E. coli na gojišcu z laktozo. Uporabili smo formalno specifikacijo sistema, opisano v clanku [3]. Njegovim avtorjem je pomenila tezšavo kompleksnost specifikacije, zato smo preverili, kako lahko z njo opravi orodje EST. Ugotovili smo, da EST uspesšno in v zelo kratkem cšasu tvori oznacen sistem prehajanja stanj celo za specifikacijo, ki vsebuje še vec akcij kot prvotna. Formalno smo specificirali lastnosti uravnavanja laktoznega operona s formulami ACTLW. Z metodo preverjanja modelov smo ugotavljali, ali jim sistem zadosti. Z zacetnimi primeri lastnosti smo skušali prikazati, da je pomembno, da formule pa tudi njihov neformalni opis izrazajo znacilnosti vseh mogocših poti, da za dolocšeno znacšilnost posebej izrazimo varnost in zivost oziroma da se vedno znova nekaj lahko zgodi in da je treba morda z dodatnimi formulami poskrbeti, da bodo znacšilnosti izrazšene tudi za zacšetek poti. Vse to je v [3] le delno uposštevano.
Rezultati verifikacije se skladajo s pričakovanimi lastnostmi laktoznega operona, vendar smo za nekatere lastnosti to dosegli šele z uvedbo dodatnih akcij. Na podlagi rezultatov lahko z veliko verjetnostjo trdimo, da so lastnosti pravilno specificirane s formulami ACTLW in da specifikacija sistema zvesto opisuje realni sistem, kar se tice lastnosti, ki so nas zanimale, razen zivosti. Za razlicne snovi nam je uspelo potrditi samo veljavnost lastnosti moznosti. Da bi lahko potrdili tudi veljavnost pricšakovanih lastnosti zšivosti, bi bilo treba preverjanje modelov v EST-u razširiti z moznostjo upoštevanja poštenostnih omejitev. Z njimi bi lahko dosegli, da bi se pregledovale samo tiste poti, na katerih se ne bi ves cas izvajale samo nekatere akcije, druge, ki bi se v realnosti zagotovo obcšasno izvedle, pa nikoli.
Logika ACTLW in orodje EST sta se sicer izkazala za dobro kombinacijo pri pisanju formalne specifikacije lastnosti in izvajanju verifikacije. Zelo nam je pomagala moznost tvorjenja protiprimerov. Tezave so nastale zaradi jezika, podobnega CCS, ki zahteva uporabo sond. V prihodnje bi bilo jezik v EST-u dobro dopolniti tako, da bi lahko izbrali, naj se komplementarni akciji pri komunikaciji ne skrijeta za notranjo akcijo, ampak naj nova akcija odraza ime sodelujocih akcij. Tako bi za specifikacijo lastnosti lahko uporabili kar imena novih akcij in sonde ne bi bile potrebne. Verifikacija pa ni nujno namenjena samo preverjanju ze znanih lastnosti. Zelimo si, da bi za sistem odkrili lastnosti, ki so bile do zdaj neznane.
Zahvala
Raziskovalno delo Tatjane Kapus je sofinancirala Javna agencija za raziskovalno dejavnost Republike Slovenije (ARRS) v okviru programa P2-0069.
proteome: a sweet tale," Molecular & Cellular Proteomics, vol. 5, no. 4, pp. 589-607, 2006.
[9] P. Drabik, P. Maggiolo-Schettini, P. Milazzo, "Modular verification of interactive systems with an application to biology," Scientific Annals of Computer Science, vol. 21, no. 1, pp. 3972, 2011.
[10]	G. Bernot and J.-P. Comet, "On the use of temporal formal logic to model gene regulatory networks," in Proc. Int. Meeting on Computational Intelligence Methods for Bioinformatics and Biostatistics, LNBI 6160, Berlin: Springer-Verlag, 2010, pp. 112-138.
[11]	T. A. Basuki, A. Cerone, P. Milazzo, "Translating stochastic CLS into Maude," Electronic Notes in Theoretical Computer Science, vol. 227, pp. 37-58, Feb. 2009.
[12]	Wikipedia, "Calculus of communicating systems," Available: https://en.wildpedia.org/wiki/Calculus_of_communicating _systems. Accessed on: July 7, 2017.
[13]	L. Lamport, "Proving possibility properties," Theoretical Computer Science, vol. 206, no. 1-2, pp. 341-352, Oct. 1998.
Rok Vogrin je diplomiral leta 2015 na Fakulteti za elektrotehniko, računalništvo in informatiko Univerze v Mariboru, kjer je trenutno v absolventskem stažu magistrskega študijskega programa Telekomunikacije.
Robert Meolic je docent na Fakulteti za elektrotehniko, racšunalnisštvo in informatiko Univerze v Mariboru. Njegovo raziskovalno podrocje so simbolicne metode za formalno verifikacijo sistemov, še zlasti metoda preverjanja modelov. Je avtor orodja EST.
Tatjana Kapus je redna profesorica na Fakulteti za elektrotehniko, racšunalnisštvo in informatiko Univerze v Mariboru. Njeno glavno raziskovalno podrocje je formalna specifikacija in verifikacija reaktivnih sistemov, kot so na primer komunikacijski protokoli, sekvencna digitalna vezja in biološki sistemi.
Literatura
[1]	T. A. Basuki, "Model-checking biological systems using calculi of looping sequences," Ph.D. Thesis proposal.
[2]	G. Bernot, J.-C. Comet, A. Richard, M. Chaves, J.-L. Gouze, and F. Dayan , "Modeling and analysis of gene regulatory networks," in Modeling in Computational Biology and Biomedicine: A Multidisciplinary Endeavour, F. Cazals and P. Kornprobst, Eds. Springer, 2013, pp. 47-80.
[3]	M. C. Pinto, L. Foss, J. C. M. Mombach, L. Ribeiro, "Modelling, property verification and behavioural equivalence of lactose operon regulation," Computers in Biology and Medicine, vol. 37, no. 2, pp. 134-148, Feb. 2007.
[4]	R. Meolic, "Preverjanje pravilnosti obnašanja sistemov s socasnostjo," Master's Thesis, Univerza v Mariboru, Fakulteta za elektrotehniko, racšunalnisštvo in informatiko, 1999.
[5]	R. Meolic, "Notes on specifying systems in EST," in Zbornik ERK 2006, Portoroz, Slovenia, vol. B, pp. 23-26, Sept. 2006.
[6]	R. Milner, Communication and Concurrency, New York, NY, USA: Prentice-Hall, 1989.
[7]	R. Meolic, "Akcijska logika dreves izvajanj z operatorjem unless," Ph.D. Dissertation, Univerza v Mariboru, Fakulteta za elektrotehniko, racšunalnisštvo in informatiko, 2005.
[8]	J. C. Silva, R. Denny, C. Dorschel, M. V. Gorenstein, G. Z. Li, K. Richardson, D. Wall, and S. J. Geromanos, "Simultaneous qualitative and quantitative analysis of the Escherichia coli