@prefix log: . @prefix owl: . @prefix xsd: . @prefix rdfs: . @prefix rdf: . @prefix : . ### Pi-Calculus # # see http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-85/ECS-LFCS-89-85.ps # http://www.lfcs.inf.ed.ac.uk/reports/89/ECS-LFCS-89-86/ECS-LFCS-89-86.ps # # We presuppose an infinite set N of names, and let u, v, w, x, y, z range over names. # We also presuppose a set K of agent identifiers, each with an arity an integer >= 0. # We let A, B, C, ... range over agent identifiers. We now let P, Q, R, ... range # over the agents or process expressions, which are of six kinds as follows: :Process a rdfs:Class. :Port a rdfs:Class. :empty a :Process. # 1. A summation # -------------- # sum_i Pi where the index set I is finite. # This agent behaves like one or other of the Pi. We write 0 for the empty # summation, and call it inaction; this is the agent which can do nothing. # Henceforward, in defining the calculus, we confine ourselves just to 0 and # binary summation, written P1 + P2 . # e.g. (eg:process1 eg:process2) :summation eg:process. :summation a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 2. A prefix form -yx.P , y(x).P or tau.P # ---------------------------------------- # '-yx.' is called a negative prefix. y may be thought of as an output port of # an agent which contains it; -yx.P outputs the name x at port y and then # behaves like P . # e.g. (eg:port1 (?name1 ?name2) eg:process1) :output eg:process. :output a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 'y(x).' is called a positive prefix. A name y may be thought of as an input # port of an agent; y(x).P inputs an arbitrary name z at port y and then # behaves like P{z/x} (see the definition of substitution below). The name x # is bound by the positive prefix 'y(x).' (Note that a negative prefix does # not bind a name) # e.g. (eg:port1 (?name1 ?name2) eg:process1) :input eg:process. :input a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 'tau.' is called a silent prefix. tau.P performs the silent action tau and then # behaves like P. # e.g. (eg:action1 eg:process1) :silent eg:process. :silent a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 3. A composition P1 | P2 # ------------------------ # This agent consists of P1 and P2 acting in parallel. The components may # act independently; also, an output action of P1 (resp. P2) at any output # port x may synchronize with an input action of P2 (resp. P1) at x, to create # a silent (tau) action of the composite agent P1 | P2 . # e.g. (eg:process1 eg:process2) :composition eg:process. :composition a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 4. A restriction (x)P # --------------------- # This agent behaves like P except that actions at ports -x and x are prohibited # (but communication between components of P along the link x are not # prohibited, since they have become tau actions as explained above). # e.g. (?name1 eg:process1) :restriction eg:process. :restriction a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 5. A match [x = y]P # ------------------- # This agent behaves like P if the names x and y are identical, and otherwise # like 0. # e.g. ((?name1 ?name2) d:process1) :match eg:process. :match a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. # 6. A defined agent A(y1, ..., yn) # --------------------------------- # For any agent identifier A (with arity n) used thus, there must be a unique # defining equation A(x1, ..., xn) == P, where the names x1, ..., xn are distinct # and are the only names which may occur free in P . Then A(y1, ..., yn) behaves # like P{y1/x1, ..., yn/xn} (see below for the definition of substitution). # Defining equations provide recursion, since P may contain any agent # identifier, even A itself. # e.g. (eg:process1 eg:name1 eg:name2 eg:name3) :identifies eg:process. :identifies a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range :Process. ### axiomatic semantics :reduction a rdf:Property; rdfs:domain :Process; rdfs:range :Process. :congruent a rdf:Property; rdfs:domain :Process; rdfs:range :Process. {} => {(?P1 ?P2)!:summation :congruent (?P1 ?P2)!:summation}. {} => {(?P1 ?P2)!:summation :congruent (?P2 ?P1)!:summation}. {} => {(?P1 (?P2 ?P3)!:summation)!:summation :congruent ((?P1 ?P2)!:summation ?P3)!:summation}. {?P1 :congruent ?P2} => {(?P1 ?P3)!:summation :congruent (?P2 ?P3)!:summation}. {} => {(?P1 ?P2)!:composition :congruent (?P1 ?P2)!:composition}. {} => {(?P1 ?P2)!:composition :congruent (?P2 ?P1)!:composition}. {} => {(?P1 (?P2 ?P3)!:composition)!:composition :congruent ((?P1 ?P2)!:composition ?P3)!:composition}. {?P1 :congruent ?P2} => {(?P1 ?P3)!:composition :congruent (?P2 ?P3)!:composition}. {?P1 :congruent ?P2. ?P2 :congruent ?P3} => {?P1 :congruent ?P3}. {} => {(?N :empty)!:restriction :congruent :empty}. {} => {(?N (?M ?P)!:restriction)!:restriction :congruent (?M (?N ?P)!:restriction)!:restriction}. {} => {((?N ?P1)!:restriction ?P2)!:composition :congruent (?N (?P1 ?P2)!:composition)!:restriction}. {?P1 :congruent (?P3 (?X ?Y ?P5)!:input)!:summation. ?P2 :congruent (?P4 (?X ?Y ?P6)!:output)!:summation} => {(?P1 ?P2)!:composition :reduction (?P5 ?P6)!:composition}. {?P1 :reduction ?P3} => {(?P1 ?P2)!:composition :reduction (?P3 ?P2)!:composition}. {?P1 :reduction ?P3} => {(?X ?P1)!:restriction :reduction (?X ?P3)!:restriction}. {?P1 :congruent ?P2. ?P2 :reduction ?P3. ?P3 :congruent ?P4} => {?P1 :reduction ?P4}.