Slides Foi 1502

7/24/2019 Slides Foi 1502

1/15

BioMaxP : A Formal Approach forCellular Ion Pumps

Bogdan Aman Gabriel Ciobanu

Romanian Academy, Institute of Computer ScienceBld. Carol I, no.8, 700505, Iasi, Romania

FOI 201524-29 August 2015

B.Aman; G.Ciobanu BioMaxP : A Formal Approach for Cellular Ion Pumps 1 / 15
http://find/

7/24/2019 Slides Foi 1502

2/15

Outline

1 Introduction

2 Syntax and Semantics of BioMaxP

3 Safety Automata

4 Relating BioMaxP to Safety Automata

5 Conclusion

http://find/

7/24/2019 Slides Foi 1502

3/15

Introduction

Afundamental mechanismin most of the living cells is the Na+

/K+

-ATPasethat is essential for the maintenance ofNa+ andK+ concen-trations across the membrane by transporting Na+ out of the cell andK+ back into the cell.

In this paper we model the movement of ions and the conforma-tional transformations of ion transporters (NaK ion pumps, Na andK ion channels) using a verysimple but powerfulnew formalism calledBioMaxP .

BioMaxPallows to work with multisets of ions, explicit interpretation of

the transportation (from inside to outside, and from outside to inside)based on the number of existing ions, and a maximal parallel executionof the involved pumps.

http://find/

7/24/2019 Slides Foi 1502

4/15

Syntax and Semantics of BioMaxP

BioMaxP Syntax

ProcessesP, Q ::= amin!(v :T) then P (sending)

amax?(f(u:T)) then P (receiving)id(v) (recursion)

P |Q (parallel)

A constraint min associated with a sending action amin!(z :T) then Pmakes the channel a available for sending zunits/ions of type T only

if the total available quantity of ions of type T is greater than min.A constraint max associated to a receiving actionamax?(x :T) then Palong a channelais activated only if the number of ions of the type Tavailable is less than max.

http://find/

7/24/2019 Slides Foi 1502

5/15


BioMaxP Syntax

ProcessesP, Q ::= amin!(v :T) then P (sending)

amax?(f(u:T)) then P (receiving)id(v) (recursion)

P |Q (parallel)

Remark

In order to focus on the local interaction aspects of BioMaxP , we ab-

stract from arithmetical operations(using the function f ), considering bydefault that the simple ones (comparing, addition, subtraction) are includedin the language.

http://find/

7/24/2019 Slides Foi 1502

6/15


BioMaxP Operational Semantics

(Com) v :T and min |T| max

amin!v then P |amax?(f(u:T)) then P {v/u}P | {v/u}P

and |T|= |T| v iff =id or|T|=|T| +v iff =add

(Call) {v/u}Pid

idPid

id(v) idPid

where id(v :T)def= Pid

(Par1) P1 1P1 P

P1|P 1P1|P

(Par2) P1 1P1 P2 2P2

P1|P212P1|P

2


S d S i f Bi M P
http://find/

7/24/2019 Slides Foi 1502

7/15


Example

Consider a system formed from n1 NaK pumps, n2 Na channels andn3 K channels.

Each pump i is modelled bythree processes: one that models the interaction of the pump with the environment, one modelling the interaction with the cell and one that models the transport of ions through the membrane.

The molecular components are processes modelled as the ends of achannel(one end for input, and another for output), while the molecularinteraction coincides withcommunication on channels.

NaKPumpEnv(id) =site2[id]160?(add(yna:NaEnv))then site2[id]2!2Kthen p[id]6?(add(yp :P))then NaKPumpEnv(id)


S f A
http://find/

7/24/2019 Slides Foi 1502

8/15

Safety Automata

Definition

Anautomaton A is a tuple N, n0, E,where

N is afinite set of nodes;

n0 is theinitial node; E N B(C) NC N is

theset of edges.

n g,a,rn is a shorthand notation for

n, g, a, r, n E. rdenotes fresh as-signments to variables after the tran-sition is performed.

A Safety Automata

start

y

7/24/2019 Slides Foi 1502

9/15

Safety Automata

Network of Safety Automata

Is theparallel composition A1 | . . . | An of a set of safety automataA1, . . . , An combined into a single system.

Synchronous communication inside the network is by handshake syn-chronisationof input and output actions.

In this case, the action alphabet consists of a? symbols (for input actions), a! symbols (for output actions),

symbols (for internal actions).


S f t A t t
http://find/

7/24/2019 Slides Foi 1502

10/15

Safety Automata

Anetwork stateis a pair n, u, where n denotes a vector of current nodesof the network (one for each automaton), and u is an assignment storingthe current values of all network integer variables.

Definition

The operational semantics of a automaton is a transition system wherestates are pairs n, u and transitions are defined by the rules:

n, u n[ni/ni], u

ifnig,,r

ni, g|= uand u = r[u];

n, u n[n

i

/ni][n

j

/nj], u if there exist i=jsuch that

1 nigi,a?,ri

ni, njgj,a!,rj

nj, gi gj |=u,2 u =ri[rj[u]].


R l ti Bi M P t S f t A t t
http://find/

7/24/2019 Slides Foi 1502

11/15

Relating BioMaxP to Safety Automata

ConstructionGiven a processPwithout the parallel operator at the top level, we associateto it an automaton A=N, n0, E, where n0 =l0, N={l0}, E =. Thecomponents NandE areupdated depending on the structureof processP:

forP=a

min

!v then P1 we have N=N {li+1} where i=max{j |ljN}; E=E {n, min |T|, a!, , li+1}.

forP=amax?(f(u:T)) then P1 we have N=N {li+1} where i=max{j |ljN};

E=

E {li, |T| max, a!, |T| =|T| |u|, li+1}, iff =id;E {li, |T| max, a!, |T| =|T| + |u|, li+1}, iff =add.

.


http://find/

7/24/2019 Slides Foi 1502

12/15


Building an automaton for each process leads to the next result about theequivalencebetween a BioMaxP processPand its corresponding automatonAP in state nP, uP (i.e., (AP, nP, uP). Their transition systems differnot only in transitions, but also in states; thus, we adapt the notion of

bisimilarity:

Definition

A symmetric relation between BioMaxP processes and their corresponding

automata is a bisimulation if whenever (N, (AN

, nN

, uN

)) ifP P,

then nP, uP nP , uP and (P

, (AP , nP , uP)) for some P.


http://find/

7/24/2019 Slides Foi 1502

13/15


Theorem

Given a BioMaxP process P, there exists an automata APwith abisimilarbehaviour. Formally, P AP.

Corollary

For a BioMaxP process, thereachability problem is decidable.


Conclusion
http://find/

7/24/2019 Slides Foi 1502

14/15

Conclusion

In this paper we try to unify and extend our previous attempts to modelthe movement of ions using the sodium-potassium pump by introducinga simple, elegant and powerful new formalism called BioMaxP .

BioMaxP is able to: capture thequantitative aspects(e.g., number of ions); abstract conditions associated with evolution(e.g., the number of ions

is between certain thresholds).

This approach facilitates a better understanding of the processes hap-pening in a cell viewed as a complex system of ion pumpsworking inparallel.

Asfuture workwe plan to use Uppaal to verify some properties of thesystems modelled in BioMaxP .

http://find/

7/24/2019 Slides Foi 1502

15/15

Thank you!

http://find/

Documents

Slides Foi 1502