Transcript slides - F.M.I.

Synchronous Parallel Composition in
Process Calculus for Ecological Models
Anna Philippou
Department of Computer Science
University of Cyprus
Joint work with
Mauricio Toro
Department of Comp. Sc.
EAFIT University
Spyros Sfenthourakis
Christina Kassara
Department of Biology
University of Patras
Department of Biology
University of Cyprus
Motivation and Background
• Population Ecology
– Population dynamics
– Conservation schemes, species reintroduction
• Individual-based modeling vs. population-based modeling
• Formal methods for ecological systems
– Process calculi, P-systems, cellular automata
2/25
Motivation and Background
• Previous work
– PALPS (Process Algebra with Locations for Population Systems)
• a discrete-time, probabilistic process calculus with locations
– Translation from PALPS to model checker PRISM
– Application of the framework for studying population dynamics through
model checking
• Limitations
– State space explosion
– Interleaving semantics in process calculi vs. phase-based execution
considered by ecologists
3/25
Illustration by example
• Consider a species that cycles through dispersal and reproduction
phases:
𝑆 = 𝑚𝑜𝑣𝑒. 𝑟𝑒𝑝. √. 𝑆
• State space of a single individual
move
rep
√
…
4/25
Illustration by example
𝑆 = 𝑚𝑜𝑣𝑒. 𝑟𝑒𝑝. √. 𝑆
• System with 2 individuals: S | S
• State space of 2 individuals (first time unit):
√
=
…
=
move
rep
5/25
Illustration by example
𝑆 = 𝑚𝑜𝑣𝑒. 𝑟𝑒𝑝. √. 𝑆
• System with 3 individuals: S | S | S
• State space of 3 individuals (first time unit):
=
√
…
=
move
rep
6/25
Illustration by example
• Intention: individuals execute their dispersal and reproduction
phases simultaneously.
• Proposed solution
– Syntax
Group individuals into populations
– Semantics
Synchronous parallel composition
• E.g.
– System with k individuals: Sk
– state space for k individuals
movek
repk
7/25
S-PALPS
• An extension of PALPS: a discrete-time, probabilistic process
algebra with locations
• World consisting of a set of locations each featuring its own
environmental characteristics and inhabited by populations.
World implemented as a graph:
8/25
S-PALPS
• Basic entities
– Channels: a, b, …
• can be used in input position, a, b, or in output position a, b
– Locations: l1, l2, …
• And a set of logical expressions, e, referring to properties of locations
– Species: s1, s2, …
• Individuals
–
–
–
–
Modelled as processes
Possess a species and a location
Locations may change dynamically
Engage in activities (e.g. reproduction, dispersal, predation, death)
9/25
Syntax (1)
• The Individual level
𝑃 ∷= 0
| 𝜂. 𝑃
|
𝑖∈𝐼 𝑝𝑖 : 𝑃𝑖
| 𝛾? (𝑃1 , 𝑃2 )
| 𝑃1 | 𝑃2
| 𝐶
• Actions
𝜂 ∷= 𝑎
| 𝑎
| 𝑔𝑜 𝑙
| √
Inactive Individual
Action prefix
Probabilistic choice
Conditional choice
Parallel composition
Constant
Input action
Output action
Dispersal action
Tick action
10/25
Syntax (2)
• The system level
𝑆 ∷= 0
| 𝑃: 𝑠, 𝑙, 𝑞
| 𝑆1 | 𝑆2
| 𝑆\L
Inactive system
Located Population
Parallel Composition
Restriction
11/25
S-PALPS Example
• The individual level: Individuals live on an nn lattice of sites and
they disperse and reproduce in two discrete phases.
• The system level: A system comprised of 2 individuals at location
ℓ and one individual at location ℓ’:
12/25
S-PALPS Semantics
• Two transition relations:
– Probabilistic transition relation
𝑆
𝑤
𝑝 𝑆′
– Nondeterministic transition relation
𝑆
𝛼
𝑛 𝑆′
• Key concepts
– All components must synchronize on a tick-action
– Probabilistic transition take precedence over nondeterministic transitions
– All components able to execute a nondeterministic action must proceed
synchronously
13/25
Selected Rules – Population Level
• (ACT)
• (MOVE)
14/25
Selected Rules – System Level
• (TICK)
• (SYNCH)
15/25
Model checking S-PALPS models
• S-PALPS  models where probabilistic and nondeterministic
behavior co-exists
• PRISM  model checker for probabilistic systems (Markov
Decision Processes, Discrete Markov Chains, Continuous MCs)
• Prism language
– State-based
– Guarded commands
– Set of modules that communicate with each other on shared actions
(CSP-style communication)
16/25
Encoding PALPS into PRISM
• To translate SPALPS into the PRISM language
– Each state of a located population is a module
– A module has a variable that counts the number of individuals at the
specific state
– the execution flow is facilitated by a local variable
– all modules synchronize via one of the following actions:
• synch – executed when a nondeterministic transition takes place
• tick – executed when a timed action takes place
• prob – executed when a probabilistic transition takes place
17/25
Encoding S-PALPS into PRISM – A Snapshot
global sp:[0,max] init 5
global sQ:[0,max] init 0
System = 𝑃: 𝑠, 𝑙, 5
𝑃 = 𝑎. 𝑄
𝑄 =…
module P
st:[0..5] init 1;
nP:[0..max]
[] (st=1)&(sP>0)  (tact’=0)&
(st’=2)&(np’=sP);
[] (st=1)&(sP=0)  (st’=2);
[synch] (st=2)  (st’=3);
[](st=3)&(pact=0)(sP’=sp– np)
&(sQ’=sQ+nP)
[prob] (st=3)&(pact=1)  …
module Q
…
18/25
Correctness of the encoding
Theorem. For any S-PALPS process 𝑆 and its PRISM translation 𝑆
we have
1. If 𝑆
2. If 𝑆
3. If 𝑆
√
𝑛 𝑆′ then
𝑤
𝑝 𝑆′ then
𝛼
𝑛 𝑆′ then
𝑆
𝑆
𝑆
𝑠𝑦𝑛𝑐ℎ 𝑡𝑖𝑐𝑘
𝑆′ .
𝑠𝑦𝑛𝑐ℎ 𝑝𝑟𝑜𝑏,𝑤
𝑠𝑦𝑛𝑐ℎ 𝛼
𝑆′ .
𝑆′ .
19/25
Case Study – The Eleonora Falcon
• Migrant species that breeds in the
Mediterranean sea
• Local conservation importance
• Three types of individuals
– Juveniles
– Young adults (sexual maturity at the age of 4)
– Mature adults (more likely to choose a protected nest)
• Parameters
– Probability of an individual to return to the island to breed (mortality)
– Availability of less-exposed nests
– Probabilities of offspring survival in exposed/less-exposed nests
20/25
The life cycle
Newborns
Dispersal
Newborns
Newborns
Juveniles of Age 4
Mortality
Surviving Adults
Dispersal
First-year breeders
Experienced
breeders
Reproduction
in exposed nest
Reproduction in
less exposed nest
Adults
Adults
DIspersal
DIspersal
Surviving Adults
Mortality
Surviving Adults
Mortality
21/25
The model in S-PALPS
22/25
Analysis in PRISM
• Verification of probabilistic temporal PCTL properties, e.g.
– Probability of extinction of the population in the next 10 years is less than
a certain threshold pe
– The total average number of individuals of species s at time unit t
• Semantics of PRISM model checking
– Defined over Markov Decision Processes: Computes minimum and
maximum probabilities
– Approximation defined over Discrete-Time Markov Chains: Computes
reward-based properties, steady state and reachability
• Simulation
– Explore random paths of execution
– Search for deadlocks using Prism simulation
– Perform model-checking by simulation (statistical model checking)
23/25
Representative results
• Impact of changing the offspring survival rates on the size of the
population
• Results indicate a fair degree of stability in the evolution of the
species and a relative insensitivity to small changes in local
conditions
24/25
Conclusions and future work
• S-PALPS
– Synchronous parallel composition – more faithful models
– Reduction of the state space of systems
– Case study – promising results
• Current/future work:
– Translation from S-PALPS to PRISM has been automated
– Improve the translation: generality vs. efficiency
– Further calibrate our model and take into account more aspects of interest
to biologists
– Apply to other case studies
– Mean field semantics à la CCS within a spatially-explicit framework
25/25