Before moving on, there’s one question that I thought was important enough to promote up to the front page, instead of just answering it in the comments. A commenter asked about process replication, !P, wanting to know if it terminates.<\/p>\n
The answer comes in two parts.<\/p>\n
The next place to go in our exploration of π-calculus is considering just what it really means for two processes to be equivalent. The fundamental equivalence relation in <\/p>\n Consider two processes, P and Q. The only<\/em> thing that an external observer can see are the communication channels<\/em> that are not localized to the processes. So the first requirement for P and Q to be equivalent is that they have equivalent externally visible communication channels.<\/p>\n We need to look a bit more in detail at that first requirement. What does it mean for communication channels to be equivalent? Given two channels x and y, they are equivalent if they can be used to send exactly the same messages. So far, in our examination of π-calculus, we’ve used a fully general notion of channels – any channel can be used to send or receive any message. But as we move on, we’ll be starting to use typing. So two channels will be equivalent if they have the same type<\/em>; and the definition of the type of a channel will be a list of the kinds of messages that can be sent and received using the channel. (To keep things simple, we’ll assume that channels are symmetric<\/em>, meaning that any process that can use a channel can use it to send or receive (or both) any message supported by the channel.)<\/p>\n So now we get to the difficult part.<\/p>\n From the outside of the process, observing the process, we can view it as a kind of state transition system. What that really means is that we can send it a message, and then watch what happens after it receives it: to be specific, what messages it sends in response. <\/p>\n So given a process P with n<\/em> communication channels With that set of type definition, we can say that the transition relation<\/em> for Suppose we have two processes P, with transition relation TP<\/sub> and message set Now, here’s where it gets tricky.<\/p>\n Suppose I have a state Qx<\/sub>. Given a message m, there is some set<\/em> of If the initial state of P is P0<\/sub> and the initial state of Q is Q0<\/sub>, Whew. That’s a mouthful. (Or a keyboardful, or whatever…) All of that is a Now that that’s out of the way, the next step is easy. P and Q are equivalent under bisimulation if P simulates Q and Q simulates P.<\/p>\n So let’s look at one or two of the things that we’ve seen before, and see if they’re equivalent under bisimulation.<\/p>\n Before moving on, there’s one question that I thought was important enough to promote up to the front page, instead of just answering it in the comments. A commenter asked about process replication, !P, wanting to know if it terminates. The answer comes in two parts. !P does process creation on demand. It’s not an […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[50],"tags":[],"class_list":["post-395","post","type-post","status-publish","format-standard","hentry","category-pi-calculus"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-6n","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/395","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=395"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/395\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=395"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=395"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=395"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nπ-calculus is called bisimulation<\/em>. The idea of bisimulation is roughly a kind of observational equivalence: two processes are equivalent under bisimulation if they exhibit the same visible behavior under all tests by an external observer.<\/p>\n
\nCP<\/sub>=cp1<\/sub>…cpn<\/sub>, we’ll model it as a state machine. So, when the process
\nis first created, we’ll say it’s in state SP0<\/sub>. Each time it receives a message,
\nit will take a transition to a new state depending on which channel received the message,
\nand what the content of the message was. When it makes the transition, it can also
\ngenerate<\/em> a sequence of messages. So for each transition, we need to specify an
\ninitial state a message as input, and a target state and a sequence of messages as output.
\nSo for a process P, we’ll define the following types:<\/p>\n\n
\nP is a relation T : (SP<\/sub>×MP<\/sub>) → (SP<\/sub>×Sequence(MP<\/sub>)) – that is, a relation<\/em> from a state of P and an input message to a new state of P and a sequence of messages generated by the transition. The fact that it’s a relation<\/em> is very important: there can be more than one possible transition from P on a given message.<\/p>\n
\nMP<\/sub>, and Q with transition relation TQ<\/sub> and message set MQ<\/sub>
\nWe’ll say that P in state Pi<\/sub> simulates<\/em> Q in state Qj<\/sub> if
\nMQ<\/sub>⊆MP<\/sub>, and<\/em> for every message m ∈ MQ<\/sub>,
\nTQ<\/sub>(Qj<\/sub>,m) and TP<\/sub>(Pi<\/sub>) generate the same<\/em>
\nsequence of messages on corresponding channels. (I’ll gloss over the formality of defining corresponding channels; I’m sure you can use your intuition to figure out what it means.)<\/p>\n
\nstates Qx<\/sub>(m) that it could transition to. We can take the union<\/em> of the states in Qx<\/sub>(m) – Qx<\/sub>∪<\/sup>(m). Now, TQ<\/sub>(Qx<\/sub>∪<\/sup>(m), n) – that is, the transition relation from the set of possible targets to TQ<\/sub>(m) given message n – is the union of TQ<\/sub>(q,n) for all q∈Qx<\/sub>∪<\/sup>(m). A set of states<\/em> of P simulates a set of states of Q if the simulation relation as defined for single states works for the union-states when their transition sets are unioned.<\/p>\n
\nthen P simulates Q<\/em> if P0<\/sub> simulates Q0<\/sub>, and for all possible transitions from the set of states<\/em> Qi<\/sub> to the set of states<\/em> Qj<\/sub> triggered by message m, there is some pair of sets of<\/em> states Pk<\/sub> and Pl<\/sub> such that Pk<\/sub> can transition to Pl<\/sub> on message m, and<\/em> Pk<\/sub> simulates Qi<\/sub> and Pl<\/sub> simulates Qj<\/sub>. <\/p>\n
\nformal way of saying that for all sequences<\/em> of messages that can be received by Q, P and Q will make transitions that generate the same outputs. Note that this is not yet symmetric: P can<\/em> have messages not supported by Q, and it can do anything it wants when it receives one of its messages. But if someone has processes P and Q, then they cannot possibly distinguish them by sending messages that both processes can understand.<\/p>\n\n