• Ingen resultater fundet

Global Computing

N/A
N/A
Info
Hent
Protected

Academic year: 2022

Del "Global Computing"

Copied!
384
0
0

Indlæser.... (se fuldtekst nu)

Hele teksten

(1)

Introduction Interplay: Process Algebra and Markov Process

Stochastic Modelling Part I: Foundations

Stephen Gilmore LFCS, University of Edinburgh

GLOBAN Summerschool Lygby, Denmark

25th August 2006

(2)

Introduction Interplay: Process Algebra and Markov Process

Global Computing

What distinguishesglobal computing fromlocalcomputing?

(3)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance

I Network latency

I Partial failures

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(4)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance

I Network latency

I Partial failures

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(5)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance

I Network latency

I Partial failures

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(6)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance

I Network latency

I Partial failures

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(7)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance — need to represent time

I Network latency

I Partial failures

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(8)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance — need to represent time

I Network latency

I Partial failures — randomness and probability

I Server may be down

I Routers may be down

I Scale

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(9)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance — need to represent time

I Network latency

I Partial failures — randomness and probability

I Server may be down

I Routers may be down

I Scale — need to quantify population sizes

I Workload characterisation

I Resource sharing

I Network contention

I CPU load

(10)

Introduction Interplay: Process Algebra and Markov Process

Global Computing: Some differences

I Physical distance — need to represent time

I Network latency

I Partial failures — randomness and probability

I Server may be down

I Routers may be down

I Scale — need to quantify population sizes

I Workload characterisation

I Resource sharing — need to express percentages

I Network contention

I CPU load

(11)

Introduction Interplay: Process Algebra and Markov Process

Modelling Global Computing: The challenges

Time What representation of time will we use?

Randomness What kind of random number distributions will we use?

Probability How can we have probabilities in the model without uncertainty in the results?

Scale How can we escape the state-space explosion problem?

Percentages What can it mean to have a fraction of a process?

(12)

Introduction Interplay: Process Algebra and Markov Process

Quantitative Modelling: Motivation

Quality of Service issues

I Can the server maintain reasonable response times?

(13)

Introduction Interplay: Process Algebra and Markov Process

Quantitative Modelling: Motivation

Scalability issues

I How many times do we have to replicate this service to support all of the subscribers?

(14)

Introduction Interplay: Process Algebra and Markov Process

Quantitative Modelling: Motivation

Scalability issues

I Will the server withstand a distributed denial of service attack?

(15)

Introduction Interplay: Process Algebra and Markov Process

Quantitative Modelling: Motivation

Service-level agreements

I What percentage of downloads do complete within the time we advertised?

(16)

Introduction Interplay: Process Algebra and Markov Process

Outline

Introduction

Interplay: Process Algebra and Markov Process

(17)

Introduction Interplay: Process Algebra and Markov Process

Outline

Introduction

Interplay: Process Algebra and Markov Process

(18)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

SYSTEM Q = MARKOV

...

...

... ...

...

...

...

...

PROCESS DIAGRAM

TRANSITIONSTATE

(19)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

DIAGRAM TRANSITIONSTATE

sm

si sk

sl sj

DIAGRAM TRANSITIONSTATE

q(j,l) q(k,l) q(m,j)

q(m,i) q(i,j) q(j,k)

A negative exponentially distributed duration is associated with each transition.

(20)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

MARKOV Q =

...

...

... ...

...

...

...

...

PROCESS DIAGRAM

TRANSITIONSTATE

sm

si sk

sl sj

DIAGRAM TRANSITIONSTATE

sm si

DIAGRAM TRANSITIONSTATE

q(i,j) q(j,k) q(j,l)

q(k,l) q(m,j)

q(m,i)

these parameters form the entries of the infinitesimal generator matrix Q

(21)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

... ...

MARKOV Q =

...

...

... ...

...

...

...

...

PROCESS DIAGRAM

TRANSITIONSTATE

sm

si sk

sl sj

DIAGRAM TRANSITIONSTATE

pi pk

pl pm

pj q(i,j) q(j,k)

q(j,l) q(m,j)

q(m,i)

In steady state the probability flux out of a state is balanced by the flux in.

= EQUILIBRIUM PROBABILITY DISTRIBUTION

p , p , p , 1 2 3 , pN

(22)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

... ...

MARKOV Q =

...

...

... ...

...

...

...

...

PROCESS DIAGRAM

TRANSITIONSTATE

sm

si sk

sl sj

DIAGRAM TRANSITIONSTATE

pi pk

pl pm

pj

"Global balance equations" captured by Q = 0 solved by linear algebra

q(i,j) q(j,k) q(j,l) q(m,j)

q(m,i) = EQUILIBRIUM PROBABILITY

DISTRIBUTION

p , p , p , 1 2 3 , pN

(23)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

SYSTEM Q = MARKOV

...

...

... ...

...

...

...

...

PROCESS

... ...

DIAGRAM TRANSITIONSTATE

= EQUILIBRIUM PROBABILITY DISTRIBUTION

p , p , p , 1 2 3 , pN

(24)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

SYSTEM Q = MARKOV

...

...

... ...

...

...

...

...

PROCESS

... ...

DIAGRAM TRANSITIONSTATE

e.g. throughput, response time, utilisation

= EQUILIBRIUM PROBABILITY DISTRIBUTION

p , p , p , 1 2 3 , pN

PERFORMANCE MEASURES

(25)

Introduction Interplay: Process Algebra and Markov Process

Performance Modelling using CTMC

SYSTEM Q = MARKOV

...

...

... ...

...

...

...

...

PROCESS

... ...

DIAGRAM TRANSITIONSTATE

e.g. throughput, response time, utilisation e.g. queueing networks and

stochastic Petri nets = EQUILIBRIUM PROBABILITY

DISTRIBUTION

p , p , p , 1 2 3 , pN

PERFORMANCE MEASURES HIGH−LEVEL

MODELLING FORMALISM

(26)

Introduction Interplay: Process Algebra and Markov Process

Outline

Introduction

Interplay: Process Algebra and Markov Process

(27)

Introduction Interplay: Process Algebra and Markov Process

Stochastic process algebras

Process algebras where models are decorated with quantitative information used to generate a stochastic process arestochastic process algebras (SPA).

(28)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA SPA

@

@

@

@@

integrated time integrated time integrated time

orthogonal time orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only exponential only exponential only

PEPA, Stochasticπ-calculus PEPA, Stochasticπ-calculus exponential + instantaneous exponential + instantaneous EMPA, Markovian TIPP EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA exponential only

exponential only IMC IMC

general distributions general distributions

IGSMP, Modest IGSMP, Modest

(29)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only exponential only exponential only

PEPA, Stochasticπ-calculus PEPA, Stochasticπ-calculus exponential + instantaneous exponential + instantaneous EMPA, Markovian TIPP EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA exponential only

exponential only IMC IMC

general distributions general distributions

IGSMP, Modest IGSMP, Modest

(30)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only exponential only

PEPA, Stochasticπ-calculus PEPA, Stochasticπ-calculus

exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP EMPA, Markovian TIPP

general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA exponential only

exponential only IMC IMC

general distributions general distributions

IGSMP, Modest IGSMP, Modest

(31)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only exponential only

PEPA, Stochasticπ-calculus PEPA, Stochasticπ-calculus

exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP EMPA, Markovian TIPP

general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA

exponential only

exponential only IMC IMC

general distributions

general distributions

IGSMP, Modest IGSMP, Modest

(32)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus exponential + instantaneous

exponential + instantaneous

EMPA, Markovian TIPP EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA exponential only

exponential only

IMC IMC

general distributions

general distributions

IGSMP, Modest IGSMP, Modest

(33)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP

EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA TIPP, SPADES, GSMPA exponential only

exponential only

IMC IMC

general distributions

general distributions

IGSMP, Modest IGSMP, Modest

(34)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP

EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA

TIPP, SPADES, GSMPA exponential only

exponential only

IMC IMC

general distributions

general distributions

IGSMP, Modest IGSMP, Modest

(35)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP

EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA

TIPP, SPADES, GSMPA exponential only

exponential only IMC

IMC

general distributions

general distributions

IGSMP, Modest IGSMP, Modest

(36)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA

SPA

SPA

@

@

@

@@

integrated time

integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only

exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus exponential + instantaneous

exponential + instantaneous EMPA, Markovian TIPP

EMPA, Markovian TIPP general distributions

general distributions

TIPP, SPADES, GSMPA

TIPP, SPADES, GSMPA exponential only

exponential only IMC

IMC

general distributions

general distributions

IGSMP, Modest

IGSMP, Modest

(37)

Introduction Interplay: Process Algebra and Markov Process

SPA Languages

SPA SPA

SPA

@

@

@

@@

integrated time integrated time

integrated time

orthogonal time

orthogonal time

@

@

@

@

Q

Q Q

Q

exponential only exponential only

exponential only

PEPA, Stochasticπ-calculus

PEPA, Stochasticπ-calculus

exponential + instantaneous

exponential + instantaneous

EMPA, Markovian TIPP

EMPA, Markovian TIPP

general distributions

general distributions

TIPP, SPADES, GSMPA

TIPP, SPADES, GSMPA

exponential only

exponential only

IMC

IMC

general distributions

general distributions

IGSMP, Modest

(38)

Introduction Interplay: Process Algebra and Markov Process

The Importance of Being Exponential

@

@

@ R

@

@

@@R

Stopk(β,s).Stop (α,r).StopkStop

StopkStop (α,r).Stopk(β,s).Stop

(β,s)

(α,r) (β,s)

(α,r)

(39)

Introduction Interplay: Process Algebra and Markov Process

The Importance of Being Exponential

@

@

@ R

@

@

@@R

Stopk(β,s).Stop (α,r).StopkStop

StopkStop (α,r).Stopk(β,s).Stop

(β,s)

(α,r) (β,s)

(α,r)

The memoryless property of the negative exponential distribution means thatresidual timesdo not need to be recorded.

(40)

Introduction Interplay: Process Algebra and Markov Process

The exponential distribution and the expansion law

We retain theexpansion law of classical process algebra:

(α,r).Stopk(β,s).Stop=

(α,r).(β,s).(StopkStop) + (β,s).(α,r).(StopkStop) onlyif the negative exponential distributionis used.

(41)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(42)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(43)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(44)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(45)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(46)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(47)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA

LABELLED TRANSITION

SYSTEM - CTMC Q

SOS rules

state transition diagram

(48)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM

CTMC Q

-

-

SOS rules

state transition diagram

(49)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA LABELLED

CTMC Q

SOS rules state transition

(50)

Introduction Interplay: Process Algebra and Markov Process

Performance Evaluation Process Algebra

I Models are constructed from componentswhich engage in activities.

(α, r ).P

*

6 HYHH

action type or name

activity rate (parameter of an exponential distribution)

component/

derivative

I The language is used to generate a CTMC for performance modelling.

PEPA MODEL

LABELLED TRANSITION

SYSTEM CTMC Q

- -

SOS rules state transition

diagram

(51)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L

PREFIX: (α,r).S designated first action CHOICE: S+S competing components CONSTANT: A=defS assigning names COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions HIDING: P/L abstractionα∈L⇒α→τ

(52)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L PREFIX: (α,r).S designated first action

CHOICE: S+S competing components CONSTANT: A=defS assigning names COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions HIDING: P/L abstractionα∈L⇒α→τ

(53)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L PREFIX: (α,r).S designated first action CHOICE: S+S competing components

CONSTANT: A=defS assigning names COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions HIDING: P/L abstractionα∈L⇒α→τ

(54)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L PREFIX: (α,r).S designated first action CHOICE: S+S competing components CONSTANT: A=defS assigning names

COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions HIDING: P/L abstractionα∈L⇒α→τ

(55)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L PREFIX: (α,r).S designated first action CHOICE: S+S competing components CONSTANT: A=defS assigning names COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions

HIDING: P/L abstractionα∈L⇒α→τ

(56)

Introduction Interplay: Process Algebra and Markov Process

PEPA

S ::= (α,r).S |S +S |A P ::= S |P BCL P |P/L PREFIX: (α,r).S designated first action CHOICE: S+S competing components CONSTANT: A=defS assigning names COOPERATION: P BC

L P α /∈L individual actions α∈L shared actions HIDING: P/L abstractionα∈L⇒α→τ

(57)

Introduction Interplay: Process Algebra and Markov Process

Interplay between process algebra and Markov process

I The theoretical development underpinning PEPA has focused on the interplay between the process algebra and the

underlying mathematical structure, the Markov process.

I From the process algebra side the Markov chain had a profound influence on the design of the language and in particular on the interactions between components.

I From the Markov chain perspective the process algebra structure has been exploited to find aspects of independence even between interacting components.

(58)

Introduction Interplay: Process Algebra and Markov Process

Interplay between process algebra and Markov process

I The theoretical development underpinning PEPA has focused on the interplay between the process algebra and the

underlying mathematical structure, the Markov process.

I From the process algebra side the Markov chain had a profound influence on the design of the language and in particular on the interactionsbetween components.

I From the Markov chain perspective the process algebra structure has been exploited to find aspects of independence even between interacting components.

(59)

Introduction Interplay: Process Algebra and Markov Process

Interplay between process algebra and Markov process

I The theoretical development underpinning PEPA has focused on the interplay between the process algebra and the

underlying mathematical structure, the Markov process.

I From the process algebra side the Markov chain had a profound influence on the design of the language and in particular on the interactions between components.

I From the Markov chain perspective the process algebra structure has been exploited to find aspects of independence even between interacting components.

(60)

Introduction Interplay: Process Algebra and Markov Process

Example: Browsers, server and download

Server =def (get,>).(download, µ).(rel,>).Server

Browser =def (display,pλ).(get,g).(d ownload,>).(rel,r).Browser + (display,(1−p)λ).(cache,m).Browser

WEB =def BrowserkBrowser

BCL Server

whereL={get,download,rel}

(61)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis

Qualitativeverification can now be complemented byquantitative verification.

(62)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis: Reachability analysis

Reachability analysis

How longwill it take for the system to arrive

in a particular state?

e e

e e e e

h e

e e

- - -

?

-

(63)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis: Specification matching

Specification matching

With what probability does system behaviour match its specification?

e

e e e

e -

6 -

?

∼=? e e e ee e e

e e

- - -

?

-

(64)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis: Specification matching

Specification matching

Does the “frequency profile” of the system match that of the specification?

e e e 0.5e

e0.5 -

6 -

?

e e

e e e 0.6e 0.4 e

e e

- - -

?

-

(65)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis: Model checking

Model checking

Does a given propertyφ hold within the system with a given probability?

φ

PP PP

PP PP

e e

e e e e

e

e e

- - -

?

-

(66)

Introduction Interplay: Process Algebra and Markov Process

Integrated analysis: Model checking

Model checking

For a given starting state how long is it until a given propertyφholds?

φ

PP PP

PP PP

e e

e e e e

e

e e

- - -

?

-

(67)

Introduction Interplay: Process Algebra and Markov Process

Parallel Composition

I Parellel composition is the basis of the compositionality in a process algebra

— it defines which components interact and how.

I In classical process algebra is it often associated with communication.

I When the activities of the process algebra have a duration the definition of parallel composition becomes more complex.

(68)

Introduction Interplay: Process Algebra and Markov Process

Parallel Composition

I Parellel composition is the basis of the compositionality in a process algebra — it defines which components interact and how.

I In classical process algebra is it often associated with communication.

I When the activities of the process algebra have a duration the definition of parallel composition becomes more complex.

(69)

Introduction Interplay: Process Algebra and Markov Process

Parallel Composition

I Parellel composition is the basis of the compositionality in a process algebra — it defines which components interact and how.

I In classical process algebra is it often associated with communication.

I When the activities of the process algebra have a duration the definition of parallel composition becomes more complex.

(70)

Introduction Interplay: Process Algebra and Markov Process

Parallel Composition

I Parellel composition is the basis of the compositionality in a process algebra — it defines which components interact and how.

I In classical process algebra is it often associated with communication.

I When the activities of the process algebra have a durationthe definition of parallel composition becomes more complex.

(71)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(72)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input andoutput pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(73)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugatepairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(74)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(75)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinctionbetween input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(76)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis ofshared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(77)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adopt CSP-style synchronisation.

(78)

Introduction Interplay: Process Algebra and Markov Process

Who Synchronises...?

Even within classical process algebras there is variation in the interpretation of parallel composition:

CCS-style

I Actions are partitioned into input and output pairs.

I Communication or

synchronisation takes places between conjugate pairs.

I The resulting action has silent type τ.

CSP-style

I No distinction between input and output actions.

I Communication or

synchronisation takes place on the basis of shared names.

I The resulting action has the same name.

Most stochastic process algebras adoptCSP-style synchronisation.

(79)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

I The issue of what it means for two timed activities to synchronise is a vexed one....

(80)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r1

s1

P2 r2

s2

s?

r?

(81)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r1

s1

P2 r2

s2

r1 s1

r2 s2

s = max(s , s )1 2

Barrier Synchronisation

(82)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

(83)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r1

s1

P2 r2

s2

r1 s1

r2 s2

s = max(s , s )1 2

s is no longer exponentially distributed

(84)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r1

s1

P2 r2

s2

s?

r?

algebraic considerations limit choices

(85)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r1

s1

P2 r2

s2

r1 s1

r2 s2 r = r x r1 2

TIPP: new rate is product of individual rates

(86)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

(87)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

P1 r =?1

P2 r2

s2

r2 s2 r = r 2 r =?1

EMPA: one participant is passive

(88)

Introduction Interplay: Process Algebra and Markov Process

Timed Synchronisation

UNF 738 S UNLEADED

PETROL

Referencer

RELATEREDE DOKUMENTER

However it is important to mention that strategy O is seen as a continuous process of development and adaption in a wanted direction, while the functional vision model still holds

The most common approach is to fit a CPH model, (Cox, 1972), and search for significant, in terms of p-values, independent predictors of the survival time using a stepwise

As a model-based approach is used in this work, this paper starts by presenting the model of a submersible pump application in section III. The fault detection algorithm is

For example, a new, generated elevation model (test file) may be compared to an existing model (reference file), and in case there is a difference in elevations greater than the

In  this  dissertation,  the  energy  system  analysis  and  planning  model  EnergyPLAN  is  used  [18].  The  aim  of  a  planning  model  is  to design 

I will try to give a smooth transition between the different models used in this thesis, starting from the single (multivariate) Gaussian model to the more complex Linear Factor and

The challenge is extensive: (1) to construct a design for learning model that matches learning in a networked society and, at the same time, bypasses the consequences of the

A stochastic model is developed and the model is used to simulate a time series of discharge data which is long enough to achieve a stable estimate for risk assessment of