Comp432 - Functional Programming References Light Version

Honours | Calendar | References (Normal) (Formal) (Quick) (Links only) (Light Toggle)

Total of 31 records found.
Current page is: file:///C:/My Documents/Education/University/public_html/comp471.html?HTML=true&
File is: comp471_lite.html

Sort by Category, type, title, short_title, author, pub_date, read_date, rank. View rank.

[LN] Title: COMP 471: Semantics of Concurrency - Lecture Notes
Author(s): Matthew Hennessy
Publication Date: (2002)
Remote: http://www.mcs.vuw.ac.nz/courses/COMP471/2002/
Comments: Lecture notes.

[BISIM] Title: Bisimulation
Comments: To prove a machine X simulates Y, come up with a relation between states in X and Y and then show it works.
To prove otherwise, show that no possible relation will have a simulation that works.
X should simulate Y and Y should simulate X. The relations should be the inverse of each other.

[LTS] Title: Labelled Transition Systems (LTS)
Found/Read: 2002/02/26
Comments: From the lecture notes [LN].
An lts is a triple (Q, Act, T).
A formalism to encompass all the different views of a system.

[LEQ] Title: Language equivalence
Comments: Two states are language equivalent if they can generate exactly the same set of strings.
Language equivalenve is fine for finite automata, but not so suitable for more general systems. Example of behavioural equivalence of two drink machines.

"language equivalence does not distinguish between states in a system which lead to different branching possibilities."
"at least some forms of branching have important repercussions for users of systems."

[SIM] Title: Simulation
Comments: From [LN]:
Definition 1 In a given LTS [LTS] the state Q simulates the state P if there is a simulation (relation) which relates P and Q; that is a simulation S such that P S Q.
For Q to simulate P we require:

that every action of P be matched by one from Q
more importantly the residual of Ps action, the resulting state, be simulated in turn by the residual of Qs action.

To prove that S is a simulation we need to show that:

for every pair (A,B) in S
for every action from the first state A -a-> A'

there is some corresponding action from the second state B -a-> B' such that the pair (A',B') is again in S.

To show that a certain state does not simulate another state. Show that Q cannot simulate all the moves that P can. I.e. P can do the same action to two different states where as Q can only do the action two one state. The important part comes from P having more options than Q.
A dead state can be simulated by almost any state, as by definition it can't do any actions.
See also [SBISIM]

[SBISIM] Title: Strong Bisimulation Equivalence
Comments: P ~ Q
A notion of behavioural equivalence between system states should be symmetric. Strong bisimulation is just a symmetric version of simulation [SIM].

every action from P -a-> P', must be matched by a corresponding action from Q, Q -a-> Q'. Here matching means that the residuals are related, P' R Q'.
symmetrically every action from Q, Q -a-> Q', must be matched by a corresponding move from P, P -a-> P'.

R is a simulation. R^-1 is also a simulation, R^-1 = {(Q,P) | (P,Q) ∈ R}
Definition 2 In an lts [LTS] we say the states P and Q are strongly bisimular, written P ~ Q, if there is some bisimulation R such that P R Q.

If P simulates Q and Q simulates P it is not necessarily true that P and Q are bisimilar, the relation in one direction may no be the reverse of the other.

[WBE] Title: Weak Bisimulation Equivalence
Comments: a.k.a. Observational Equivalence. P _~^~ Q. Ignoring internal moves (τ) - treats them as unobservable.
P =s=> P'
P =ε=> P' ≡ P -τ^*-> P'
P =a₁…a_n=> Q ≡ P -τ^*-> -a₁-> -τ^*-> … -τ^*-> -aⁿ-> -τ^*-> Q

P =û=> P' ≡ P -τ-> P' if μ = τ
P =û=> P' ≡ P =μ=> P' if μ ≠ τ
<<μ>>Φ - Satisfied by a process P if P =û=> P' for some residual P' such that P' statisfies Φ.

[LPT] Title: Language of process terms - sequential processes
Comments: P ::= 0 | µ.P | P + P | A(ñ)
µ ::= n? | n! | n
A(ñ) <= D_A

[SEM] Title: Semaphore
Comments: A Historical Note
Semaphores were first proposed by Edsger W. Dijkstra in 1968. Dijkstra, a Dutchman, used P for Wait() because P is the first letter of the Dutch word "passeren," which means "to pass," and V for Signal() because V is the first letter of the Dutch word "vrijgeven," which means "to release." Some books may also use down and up for Wait() and Signal(), respectively.

[CSP] Title: The Critical Section Problem
Comments: Mutual exclusion - only one process at a time in a critical section
Progress - some process must always be making process
Bounded waiting - no process should be delayed indefinitely.

[ML] Title: Modal Logic
Comments: Φ ::= true | ¬Φ | Φ ∧ Φ | <μ>Φ
false = ¬true
P |= <μ>Φ' if P -μ-> P' where (there exists a P' such that) P' |= &Phi' -it is possible to do μ and enter a state where Φ is true.
[a]Φ = ¬<a>(¬Φ) - everytime an 'a' is done &Phi is true.
The formula [μ]Φ is satisfied by by a process if every state it can reach satisfies the property Φ. [a]false is satisfied by a process if it can not do the action a.