Calculus of communicating systems

<h2 id="syntax">Syntax</h2>
<p>Given a set of action names, the set of CCS processes is defined by the following <a href="/facts/BNF_grammar/xbMXDntc">BNF grammar</a>:
</p>

P
        ::=
        0
        
        
        
        
          |
        
        
        
        
        a
        .
        
          P
          
            1
          
        
        
        
        
        
          |
        
        
        
        
        A
        
        
        
        
          |
        
        
        
        
        
          P
          
            1
          
        
        +
        
          P
          
            2
          
        
        
        
        
        
          |
        
        
        
        
        
          P
          
            1
          
        
        
          |
        
        
          P
          
            2
          
        
        
        
        
        
          |
        
        
        
        
        
          P
          
            1
          
        
        [
        b
        
          /
        
        a
        ]
        
        
        
        
          |
        
        
        
        
        
          P
          
            1
          
        
        
          ∖
        
        a
        
        
        
      
    
    {\displaystyle P::=0\,\,\,|\,\,\,a.P_{1}\,\,\,|\,\,\,A\,\,\,|\,\,\,P_{1}+P_{2}\,\,\,|\,\,\,P_{1}|P_{2}\,\,\,|\,\,\,P_{1}[b/a]\,\,\,|\,\,\,P_{1}{\backslash }a\,\,\,}

<p>The parts of the syntax are, in the order given above
</p>
inactive process
the inactive process 
  
    
      
        0
      
    
    {\displaystyle 0}
  
 is a valid CCS process
action
the process 
  
    
      
        a
        .
        
          P
          
            1
          
        
      
    
    {\displaystyle a.P_{1}}
  
 can perform an action 
  
    
      
        a
      
    
    {\displaystyle a}
  
 and continue as the process 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}

process identifier
write 
  
    
      
        A
        
          
            =
            
              
              
                d
                e
                f
              
            
          
        
        
          P
          
            1
          
        
      
    
    {\displaystyle A{\overset {\underset {\mathrm {def} }{}}{=}}P_{1}}
  
 to use the identifier 
  
    
      
        A
      
    
    {\displaystyle A}
  
 to refer to the process 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}
  
 (which may contain the identifier 
  
    
      
        A
      
    
    {\displaystyle A}
  
 itself, i.e., recursive definitions are allowed)
summation
the process 
  
    
      
        
          P
          
            1
          
        
        +
        
          P
          
            2
          
        
      
    
    {\displaystyle P_{1}+P_{2}}
  
 can proceed either as the process 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}
  
 or the process 
  
    
      
        
          P
          
            2
          
        
      
    
    {\displaystyle P_{2}}

parallel composition

P
          
            1
          
        
        
          |
        
        
          P
          
            2
          
        
      
    
    {\displaystyle P_{1}|P_{2}}
  
 tells that processes 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}
  
 and 
  
    
      
        
          P
          
            2
          
        
      
    
    {\displaystyle P_{2}}
  
 exist simultaneously
renaming

P
          
            1
          
        
        [
        b
        
          /
        
        a
        ]
      
    
    {\displaystyle P_{1}[b/a]}
  
 is the process 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}
  
 with all actions named 
  
    
      
        a
      
    
    {\displaystyle a}
  
 renamed as 
  
    
      
        b
      
    
    {\displaystyle b}

restriction

P
          
            1
          
        
        
          ∖
        
        a
      
    
    {\displaystyle P_{1}{\backslash }a}
  
 is the process 
  
    
      
        
          P
          
            1
          
        
      
    
    {\displaystyle P_{1}}
  
 without action 
  
    
      
        a
      
    
    {\displaystyle a}

<h2 id="related-calculi-models-and-languages">Related calculi, models, and languages</h2>
<ul><li><a href="/facts/Communicating_sequential_processes/bzKGnJ50">Communicating sequential processes</a> (CSP), developed by <a href="/facts/Tony_Hoare/vBeb3cmn">Tony Hoare</a>, is a formal language that arose at a similar time to CCS.</li>
<li>The <a href="/facts/Algebra_of_Communicating_Processes/WPuehJrV">Algebra of Communicating Processes</a> (ACP) was developed by <a href="/facts/Jan_Bergstra/zk2SbKJz">Jan Bergstra</a> and <a href="/facts/Jan_Willem_Klop/JvRpGM6a">Jan Willem Klop</a> in 1982, and uses an axiomatic approach (in the style of <a href="/facts/Universal_algebra/uMJAL6ER">Universal algebra</a>) to reason about a similar class of processes as CCS.</li>
<li>The <a href="/facts/Pi-calculus/rAHByKdf">pi-calculus</a>, developed by <a href="/facts/Robin_Milner/oMfdsRwK">Robin Milner</a>, Joachim Parrow, and David Walker in the late 80's extends CCS with mobility of communication links, by allowing processes to communicate the names of communication channels themselves.</li>
<li><a href="/facts/PEPA/ypBwNmqd">PEPA</a>, developed by <a href="/facts/Jane_Hillston/1vJ7VTFK">Jane Hillston</a> introduces activity timing in terms of exponentially distributed rates and probabilistic choice, allowing performance metrics to be evaluated.</li>
<li>Reversible Communicating Concurrent Systems (RCCS) introduced by Vincent Danos, Jean Krivine, and others, introduces (partial) reversibility in the execution of CCS processes.</li></ul>
<p>Some other languages based on CCS:
</p>
<ul><li><a href="/facts/Calculus_of_broadcasting_systems/CEEoBXKa">Calculus of broadcasting systems</a></li>
<li><a href="/facts/Language_Of_Temporal_Ordering_Specification/UH9FXwDu">Language Of Temporal Ordering Specification</a> (LOTOS)</li>
<li>Process Calculus for Spatially-Explicit Ecological Models (PALPS) is an extension of CCS with probabilistic choice, locations and attributes for locations<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a></li>
<li><a href="/facts/Jolie_(programming_language)/JfGFHhnn">Java Orchestration Language Interpreter Engine</a> (Jolie)<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a></li></ul>
<p>Models that have been used in the study of CCS-like systems:
</p>
<ul><li><a href="/facts/History_monoid/2Jtzdm3X">History monoid</a></li>
<li><a href="/facts/Actor_model/MJ49opnU">Actor model</a></li></ul>

<ul><li>Robin Milner: <i>A Calculus of Communicating Systems</i>, Springer Verlag, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-387-10235-3. 1980.</li>
<li>Robin Milner, <i>Communication and Concurrency</i>, Prentice Hall, International Series in Computer Science, <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 0-13-115007-3. 1989</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>Herzog, Ulrich, ed. (May 2007). "Tackling Large State Spaces in Performance Modelling". Formal Methods for Performance Evaluation. Lecture Notes in Computer Science. Vol. 4486. Springer. pp. 318–370. doi:10.1007/978-3-540-72522-0. ISBN 978-3-540-72482-7. Archived from the original on 2008-04-12. Retrieved 2009-04-21. <a href="978-3-540-72482-7" target="_blank">978-3-540-72482-7</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>A Philippou, M Toro, M Antonaki. Simulation and Verification in a Process Calculus for Spatially-Explicit Ecological Models.
Scientific Annals of Computer Science 23 (1). 2014 <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>Montesi, Fabrizio; Guidi, Claudio; Lucchi, Roberto; Zavattaro, Gianluigi (2007-06-27). "JOLIE: a Java Orchestration Language Interpreter Engine". Electronic Notes in Theoretical Computer Science. Combined Proceedings of the Second International Workshop on Coordination and Organization (CoOrg 2006) and the Second International Workshop on Methods and Tools for Coordinating Concurrent, Distributed and Mobile Systems (MTCoord 2006). 181: 19–33. doi:10.1016/j.entcs.2007.01.051. ISSN 1571-0661. <a href="https://doi.org/10.1016%2Fj.entcs.2007.01.051" target="_blank">https://doi.org/10.1016%2Fj.entcs.2007.01.051</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
</ol>

Calculus of communicating systems open-in-new

Calculus of communicating systems