% Elements of Interaction % Andreas Harth % Journal Club Jan 2021

Introduction

Formalising (Concurrent) Computation

• Sequential computing has been formalised in lambda calculus
• Need to formalise concurrent programming and interactive systems
• Proposal: Calculus of Communicating Systems
• Naming and reference (mentioned, but why?) - talks about semantics a lot
• Rejects the idea of a single conceptual model - we need many different conceptual models and formalisms

Application Areas

• The flow of information in an insurance company
• Network communications
• The real-time communications among in-flight control computers
• Concurrency control in a database
• The behaviour of parallel object-oriented programs
• The semantic analysis of variables in concurrent logic programming

Universality/Generality

• "We surely do not expect the terms of discussion and analysis to be the same for all of these"
• But he proposes exactly that: a general formalism for describing "all of these"

Robin Milner, A Calculus of Communicating Systems, Springer 1980

• State machines (acceptors and generators) could serve as formalisation for concurrency
• Example: two nondeterministic acceptors, which are equivalent (accept the same set of strings)
• But: for interaction scenarios, the notion of equivalence of state machines is flawed, need observational equivalence
• Maybe also: need to be able to talk about multiple state machines interacting with each other

Two Nondeterministic State Machines (Acceptors)

Via applying substitution, distributive law and Arden's rule, one can show the two state machines are equivalent.

But are they? Difference in Behaviour

How to Proceed

• Concurrency is ubiquitous
• Combine models from logic and mathematics with a proper distillation of practical experience
• Ideal: have the purity and simplicity of lambda calculus
• Pin down ideas about concurrency and interaction suggested by programming and the realities of communication

Meaning

Meaning

• Process = an algebraic expression
• Should "process" not be a mathematical thing?
• "denotation" -> probably he means reference

• ...

• Use a mathematical apparatus to prove statements

• Map to first-order structure or to a Kripke structure (second order) or transition system (difference?)

Example: Turning Coffee into Publications

Aceto, L., Ingólfsdóttir, A., Larsen, K., & Srba, J. (2007). Reactive Systems: Modelling, Specification and Verification. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511814105

Fast-forward: SOS - Structural Operational Semantics

Aceto, L., Ingólfsdóttir, A., Larsen, K., & Srba, J. (2007). Reactive Systems: Modelling, Specification and Verification. Cambridge: Cambridge University Press. doi:10.1017/CBO9780511814105

Conclusion

Summary

• Presented a basic model of concurrency, guided by a sequential paradigm (the lambda calculus)
• Dared to talk about semantics (@@@but remains unclear to me what he actually means)
• CCS is reduced to atomic primitives (but many levels of explanation are needed)
• Claimed some generality for pi-calculus (hah!)
• Relative to Hewitt's actor model, pi-calculus is formal calculus, while the actor model wants to identify the laws which govern interaction (@@@?)

Further Work: Experiments

• How to test and experiment with a model of computing?

• Next to a experimental test, do a mathematical test: find a theory that is tractable

• CCS/pi calculus is a candidate theory

• Greater goal: towards a broad informational science of man-made and natural phenomena

Why?

• Model theory: check satisfiability, find tautologies, define entailment

• Compositionality: juxtapose multiple processes

• Proof properties about every possible execution of a process (analysis of behaviour)

• Check for observation equivalence between two processes (bisimulation - done on transition systems)

• Find deadlocks/livelocks for n processes
• Check termination for n processes
• Verify temporal formula on n processes
• Check for lost update problems on n processes
• Figure out causality between events in a process or n processes

"Hello World" with Two Agents

• User agents A1, A2

• Server (Resource) R1 (e.g., http://ldp.local/r1)

• Action w (request write to R1 with representation)

• Action w2 (response 201 Created)
• Action w3 (response 401 Unauthorized)
• Action r (request read from R1)
• Action r2 (response 200 OK with representation)

• Action r3 (response 404 Not Found)

• @@@Ports?

• A1: w

• R1: w2
• A2: r
• A2: r2

• done

• A1 := w.(w2.0 + w3.0)

• A2 := r.(r2.0 + r3.0)

• R1 := w.(w2.R1 + w3.R1) + r.(r2.R1 + r3.R1)

• A1 | A2 | R1

How to Represent Conditions?

• Is it possible to phrase ECA rules as CCS processes?
• Event: incoming action
• Action: outgoing action
• Condition: ?