Hubert Garavel
email: hubert.garavel@inria.fr

Revisiting Sequential Composition in Process Calculi

Keywords: ACP, concurrency theory, CCS, CSP, E-LOTOS, formal specification, formal semantics, LOTOS, LNT, modelling language, muCRL, OCCAM, process algebra, process calculus, programming language, PSF, sequential composition, software engineering, specification language

The article reviews the various ways sequential composition is defined in traditional process calculi, and shows that such definitions are not optimal, thus limiting the dissemination of concurrency theory ideas among computer scientists. An alternative approach is proposed, based on a symmetric binary operator and write-many variables. This approach, which generalizes traditional process calculi, has been used to define the new LNT language implemented in the CADP toolbox. Feedback gained from university lectures and real-life case studies shows a high acceptance by computer-science students and industry engineers.

Introduction

Process calculi (or process algebras) are a corner stone of concurrency theory and exist under many variants, among which CCS [START_REF] Milner | A Calculus of Communicating Systems[END_REF][START_REF] Milner | Communication and Concurrency[END_REF], CSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF][START_REF] Hoare | Communicating Sequential Processes[END_REF][START_REF] Roscoe | Understanding Concurrent Systems[END_REF], MEIJE [START_REF] Austry | Algèbre de Processus et Synchronisation[END_REF], ACP 2 [START_REF] Bergstra | Algebra of Communicating Processes with Abstraction[END_REF][START_REF] Baeten | Process Algebra[END_REF][START_REF] Fokkink | Introduction to Process Algebra[END_REF], LOTOS [START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF][START_REF] Bolognesi | Introduction to the ISO Specification Language LOTOS[END_REF], PSF [START_REF] Mauw | An Introduction to PSFd[END_REF][START_REF] Mauw | A Process Specification Formalism[END_REF][START_REF] Veltink | PSF -A Retrospective[END_REF], µCRL [START_REF] Groote | The Syntax and Semantics of µCRL, CS-R 9076[END_REF][START_REF] Groote | The Syntax and Semantics of µCRL[END_REF], and mCRL2 [START_REF] Groote | Modeling and Analysis of Communicating Systems[END_REF], to name only a few. From a theoretical point of view, process calculi are mathematical models for the study of concurrency. To this aim, they are expected to be of manageable complexity, i.e., have a minimal number of constructs or, at least, a small set of core constructs to which other constructs can be translated.

In practice, however, this definition is too narrow and process calculi clearly have another role. They are often used as modelling languages to formally describe the behavior of complex concurrent systems, including telecommunication protocols, distributed software, and hardware circuits. The intent of applying process calculi to real-life problems can be traced back at least to the mid-80s, when LOTOS was defined as an international standard to formally describe OSI protocols and services. Moreover, many compilers and software verification tools have been developed to implement process calculi, e.g., CWB [START_REF] Cleaveland | The Concurrency Workbench[END_REF] and CWB-NB [START_REF] Cleaveland | The Concurrency Workbench of the New Century (Version 1.2) -User's Manual[END_REF] for CCS, FDR [START_REF]Failures-Divergence Refinement -FDR2 User Manual[END_REF][START_REF] Gibson-Robinson | FDR3 -A Modern Refinement Checker for CSP[END_REF] and PAT [START_REF] Sun | Model Checking CSP Revisited: Introducing a Process Analysis Toolkit[END_REF][START_REF] Shi | An Analytical and Experimental Comparison of CSP Extensions and Tools[END_REF] for CSP, CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] for LOTOS, the mCRL tools [START_REF] Dams | Specification and Implementation of Components of a µCRL Toolbox[END_REF][START_REF] Cranen | An Overview of the mCRL2 Toolset and Its Recent Advances[END_REF] for µCRL and mCRL2, etc. All in one, this is a clear indication that more is expected from process calculi than merely providing a theoretical framework for abstractly reasoning about concurrency.

Whether a given process calculus can conveniently play these two roles is very much an open question. For instance, Milner believed that CCS was meant for theory only and he proposed, to describe more concrete systems, another language named M [2, Chapter 8] based on shared variables and algorithmic programming constructs, together with a translation algorithm from M to CCS. Although there have been follow-ups to this idea, e.g., [START_REF] Sokolsky | Efficient Graph-based Algorithms for Model Checking in the Modal Mu-calculus[END_REF] [28] [5, Chapter 18], one may wonder if having two languages instead of one is a true benefit. Moreover, most of the aforementioned process calculi claim to be modelling languages for concurrent systems as well as formalisms supporting mathematical reasoning, therefore indicating a general trend towards a single-language approach.

To describe and analyze real systems, process calculi have genuine advantages: they provide built-in parallel composition operators, they are equipped with formal semantics, and they have compositionality properties (e.g., congruence results) for scaling to large component-based systems. Despite a growing number of success stories, the practical impact of process calculi is not as high as it should be: formal approaches are not widely used in industry and few recent languages for modelling or programming take inspiration from concurrency theory.

There are several reasons for this situation [START_REF] Garavel | Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular[END_REF]: fragmentation (multiple, similar yet incompatible process calculi), lack of expressiveness, and lack of user-friendliness, all resulting in a steep learning curve that discourages potential users. The aforementioned dichotomy between mathematical models and modelling languages also contributed to creating a gap: the simplicity and elegance of CCS, reinforced by the algebraic approach of ACP, shifted the focus towards mathematical models, weakening the links with mainstream programming languages.

We believe it is important to disseminate concurrency theory results to a wider audience, and that process calculi can be an essential vector for this. It is high time to reconsider the dichotomy between process calculi and programming languages, and to come up with enhanced process calculi acceptable by professionals. As part of this agenda, we review the way sequential composition is handled in process calculi. This topic is often seen as a matter of secondary importance with respect to concurrency and mobility, but the present article reopens the case by considering sequential composition as a major subject that almost entirely shapes a process calculus and determines its compatibility with mainstream programming languages. The core of the issue is not so much expressiveness -most process calculi provide the same expressiveness whatever the approach chosen for sequential composition -but conciseness (objective) and convenience (subjective).

The present article is organized as follows. Sec. 2 sets a few definitions that will be used throughout the article. Sec. 3 reviews and gives a critical evaluation of the sequential composition operators available in traditional process calculi. Sec. [START_REF] Hoare | Communicating Sequential Processes[END_REF] proposes an enhanced definition of sequential composition, which has been integrated in LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.2)[END_REF], the most recent specification language supported by the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. Sec. 5 discusses the expressiveness of LNT and proposes encodings that map large fragments of former process calculi (CCS, ACP, LOTOS, and CSP) to LNT. Sec. 6 illustrates the advantages of LNT on several design patterns that cannot be concisely expressed using traditional process calculi. Finally, Sec. 7 gives concluding remarks and perspectives for future work.

Preliminary definitions

The present article assumes that the reader has some basic familiarity with the general concepts of process calculi, but no extensive knowledge is required. As the various process calculi use different vocabulary and notations to define their syntax and semantics, we introduce here common terminology and notations that will be used for all languages throughout the article.

In the following, terminal symbols (i.e., identifiers or constants) are noted in lower case, while non-terminal symbols (defined by BNF rules) are noted in upper case. If y (resp. Y ) is a symbol of a given category, then y , y , y 0 , y 1 , y 2 , etc. (resp. Y , Y , Y 0 , Y 1 , Y 2 , etc.) are also symbols of that same category.

We note t a data type, x a variable, and v a constant. Variables and constants are typed and we note "v ∈ t" the fact that v is a constant of type t. We note V an expression (also: data expression, value expression, or value term), i.e., a syntactic term which is built using variables, constants, and function symbols and that computes a typed value.

We note a an action (also: atomic action or atom), i.e., a communication event proposed by the system under study or its environment. Any action a can be decomposed as a tuple a = g o 1 ... o n , where g is a gate (also: channel or communication port) and o 1 ... o n a possibly empty list of offers (also: experiment offers or action parameters). Each offer is either an emission (noted "!V ") of some expression V , or a reception (noted "?x:t", or simply "?x") of some constant value to be stored in variable x of type t. We note gate(a) the gate of action a. There exists an internal (also: invisible or hidden) gate noted either "τ " or "i", which must be used without offer (and is thus also considered to be an action).

We note B a behavior (also: behavior expression or process term), i.e., a syntactic term built using actions and the various operators of the process calculi being considered. Most of our attention focuses on sequential composition operators, so that other kinds of operators (e.g., parallel composition, disruption, etc.) will only be mentioned when needed. We note "[v 1 /x 1 ...v n /x n ]B" the behavior obtained from B by replacing all free occurrences of variables x 1 , ..., x n by constants v 1 , ..., v n , respectively. We note p a process identifier (also: agent name), i.e., a symbolic name that can be associated to a behavior (this is needed to define recursive behaviors).

Sequential composition in traditional process calculi

The "action prefix" operator and its drawbacks

The most widespread means of expressing sequentiality in process calculi is the action prefix operator (also called prefixing), which is present in many process calculi. This operator will be noted here ".", as in CCS; it is also noted ":" in MEIJE, "→" in CSP, and ";" in LOTOS. Its syntax is defined by the BNF rule "B ::= a.B" and its semantics by the SOS rule:

-

a.B a -→ B
meaning that "a.B" first performs action a and then behaves as B.

Action prefix is simple, suitable for proofs, and well accepted by (most of) the concurrency theory community. In practice, however, action prefix suffers from several drawbacks: 1. It is non-standard with respect to mainstream programming languages. Action prefix is asymmetric in the sense that its left-hand and right-hand sides require different syntactic objects (an action must come first, followed by a behavior) whereas sequential composition is symmetric in most programming languages (a statement is followed by another statement). Asymmetry proves to be confusing to those that learn process calculi, and students always tend to write symmetric sequential composition by default. 2. It does not support loops directly. With action prefix, the standard way of expressing iterative behaviors is to use recursion, by introducing extra process identifiers and inserting a recursive process call at each loop-back point. There have been attempts at defining iteration operators in the presence of action prefix (e.g., [5, p. 134]), but their usefulness is limited (the values computed at some iteration cannot be passed to the next iterations) and such proposals are usually not implemented in software tools. 3. It is incompatible with regular expressions. Quite often, the components of concurrent systems can be described as automata. Regular expressions are a standard means to express automata and most industry engineers are familiar with regular expressions, which are routinely used in text editors and script languages, for instance. Unfortunately, regular expressions cannot be easily expressed using action prefix, because it is asymmetric and a "loop" (Kleene star) operator is missing. 4. It prohibits control-flow sharing. Often in programming, a choice must be made between two computations B 1 and B 2 , only one of which can be executed, and afterwards a third computation B 3 has to be executed, whatever which branch B 1 or B 2 was taken before. In sequential programming, the choice between B 1 or B 2 usually depends on some deterministic condition v, so that the whole pattern can be written "if v then B 1 else B 2 end if ; B 3 ". So doing, the computation B 3 is shared, i.e. written only once. Action prefix makes sharing of B 3 impossible because prefixing favors tree-like patterns [START_REF] Milner | A Complete Inference System for a Class of Regular Behaviours[END_REF] and prohibits dag3 -like patterns. For instance, in CCS, it is syntactically illegal to write "(a 1 + a 2 ).B 3 ", where the "+" operator denotes nondeterministic choice; one must write instead "(a 1 .B 3 ) + (a 2 .B 3 )" at the expense of duplicating B 3 . Such undesirable unfolding can be avoided by defining an auxiliary process identifier p = B 3 in order to write "(a 1 .p) + (a 2 .p)" without duplicating B 3 ; however, this solution is questionable, because each call to p is similar to a "goto p" and decreases the readability of the specification by transferring the control elsewhere. 5. It prohibits data-flow sharing. The syntax of action prefix also forbids terms of the form "(g 1 ?x + g 2 ?x).B 3 ", where the variable x is received on either gate g 1 or gate g 2 and its value passed to B 3 . Such data-flow sharing is standard in sequential programming, where the variables assigned in the branches of an "if " or "case" statement can be reused afterwards. Unfortunately, action prefix forces either the duplication of B 3 (as in "(g 1 ?x.B3) + (g 2 ?x.B 3 )") or the introduction of an auxiliary process identifier p (as in "(g 1 ?x.p(x)) + (g 2 ?x.p(x))") with the aforementioned drawbacks. 6. It is not well-adapted to action refinement, i.e., program transformations based on the replacement of individual actions by more complex behaviors. For such transformations, symmetric sequential composition is usually preferred, e.g. [32] [33, 34] [35, 36, 37].

The "enable" operator and its drawbacks

The limitations of action prefix have been recognized for long -at least as early as the mid-80s. The usual remedy is to introducing a new sequential composition operator that complements action prefix and tries palliating its shortcomings. Such operator is called enable in LOTOS and is noted ">>" (it also exists in CSP, where it is called sequential composition and is noted ";"). The behavior "B 1 >> B 2 " expresses that B 1 executes first and is followed by B 2 , which only starts after B 1 is done. The enable operator is used together with another operator called successful termination (noted "exit" in LOTOS and "SKIP " in CSP), which differs from the inaction or deadlock operator (noted "nil" in CCS, "STOP " in CSP, and "stop" in LOTOS).

We consider here the LOTOS ">>" and "exit" operators, which are the most flexible ones, as they support the passing of values. We note " √ " a special termination gate4 that is different from any other gate, including "τ ". The BNF rule defining the syntax of the "exit" operator is:

B ::= exit(R 1 , ..., R n )
where R 1 , ..., R n is a (possibly empty) list of results, each R i being a syntactic term that is either an expression V i or a clause "any t i ". We note "v i ∈ R i " the fact that expression V i evaluates to constant v i (if R i has the form V i ) or the fact that v i ∈ t i (if R i has the form "any t i "). The semantics of the "exit" operator is defined by the following SOS rule:

v 1 ∈ R 1 ∧ ... ∧ v n ∈ R n exit(R 1 , ..., R n ) √ v1...vn -→ stop
The BNF rule defining the syntax of the enable operator is:

B ::= B 1 >> [accept x 1 :t 1 ... x n :t n in] B 2
where x 1 :t 1 , ..., x n :t n declares a (possibly empty) list of variables x i of type t i , which are visible in B 2 only -if the list is empty, the "accept...in" clause is omitted. When B 1 terminates by invoking an "exit(R 1 , ..., R n )" operator, each variable x i captures the value returned by the corresponding result R i . Typing constraints ensure that the type of each R i is the same as t i . The semantics of the ">>" operator is defined by two SOS rules:

B 1 a -→ B 1 ∧ gate(a) = √ B 1 >> accept x 1 :t 1 ... x n :t n in B 2 a -→ B 1 >> accept x 1 :t 1 ... x n :t n in B 2 B 1 √ v1...vn -→ B 1 B 1 >> accept x 1 :t 1 ... x n :t n in B 2 τ -→ [v 1 /x 1 ...v n /x n ]B 2
The enable operator has been used in many formal models described using LOTOS or CSP. However, it presents several drawbacks: 1. Each occurrence of an "exit" operator creates a √ -transition that is turned into a τ -transition when caught by an enable operator -as pointed out in [2, pp. 191], the enable operator relies on concurrency, synchronization, and communication to perform sequential composition. In practice, the introduction of such extra transitions is a nuisance because it makes labelled transition systems larger, causing or worsening state explosion issues. Another worrying consequence is that the enable operator lacks a neutral element modulo strong bisimulation (the extra τ -transitions can only be ignored if a weaker bisimulation is used), which is different from mainstream programming languages, most of which provide some "empty" statement that does nothing and is a neutral element with respect to sequential composition.

2. Keeping action prefix and introducing the enable operator leads to two different operators for almost the same purpose: one sequential composition operator that is asymmetric and another one that is symmetric -at least, if one forgets about the "accept...in" clause. This goes against Occam's razor law 5 , and against the idea that a process calculus should contain a minimal set of operators expressing independent ("orthogonal") concepts.

For instance, the same sequence of actions can be written in many different ways, e.g. "(a 1 ; a 2 ; exit) >> (a A lighter syntax for the first example above was proposed in [START_REF] Brinksma | On the Design of Extended LOTOS -A Specification Language for Open Distributed Systems[END_REF]Sec. 6.5], but never implemented and assessed on large-size examples.

The "product" operator and its drawbacks

The action prefix and enable operators are not the only possible approach. From the beginning, ACP explored a different way by adopting a symmetric sequential composition operator, called product and noted "•". Its syntax is thus defined by the BNF rule "B ::= B 1 • B 2 ". Following the tradition of ACP, the semantics of this operator is usually given by algebraic axioms, but it can alternatively be defined using SOS rules [START_REF] Mauw | An Introduction to PSFd[END_REF][START_REF] Fokkink | Introduction to Process Algebra[END_REF]:

B 1 a -→ B 1 B 1 • B 2 a -→ B 1 • B 2 B 1 a -→ √ B 1 • B 2 a -→ B 2
where " √ " is a special behavior (distinguishable from all other behaviors) with an associated SOS rule "a a -→ √ " applicable to each action a, including "τ ". Clearly, this product operator avoids many of the aforementioned pitfalls of action prefix and enable operators: there is a unique symmetric sequential composition, as in mainstream programming languages; it does not create extra τ -transitions; it can be equipped with a neutral element (usually noted "ε") [START_REF] Koymans | Extending Process Algebra with the Empty Process, Logic Group Preprint Series[END_REF][START_REF] Vrancken | The Algebra of Communicating Processes With Empty Process[END_REF]; it can be extended with iteration operators to express loops [START_REF] Bergstra | Process Algebra with Recursive Operations[END_REF]; it subsumes regular expressions and context-free languages [START_REF] Bergstra | The Algebra of Recursively Defined Processes and the Algebra of Regular Processes[END_REF]; finally, it allows control-flow sharing, which is explicitly permitted by axiom A4 of ACP:

(B 1 + B 2 ) • B 3 = (B 1 • B 3 ) + (B 2 • B 3 ) -notice that there is no "dual" axiom B 1 •(B 2 +B 3 ) = (B 1 •B 2 )+(B 1 •B 3
) in order to preserve the branching structure.

It remains to examine whether this product operator also supports dataflow sharing. This question cannot be directly answered within ACP, which is a pure process algebra (i.e., does not handle data). Moreover, there is an impossibility claim [START_REF] Baeten | On Sequential Composition, Action Prefixes and Process Prefixes[END_REF] stating that variable-binding actions are incompatible with associativity of sequential composition; indeed, assuming the existence of a variable-binding action (e.g., an action "g?x" that declares variable x and assigns to it an input value), then the term "g?x • B 1 • B 2 " would be ambiguous, as it can be parsed either as "(g?x • B 1 ) • B 2 " or "g?x • (B 1 • B 2 )", which gives two incompatible scopes for x (either B 1 or B 1 • B 2 ); thus, variable binding in ACP should only be achieved by means of unary "prefix" operators.

This principle is followed by the two value-passing languages based on ACP: PSF [START_REF] Mauw | An Introduction to PSFd[END_REF][START_REF] Mauw | A Process Specification Formalism[END_REF][START_REF] Veltink | PSF -A Retrospective[END_REF] and µCRL [START_REF] Groote | The Syntax and Semantics of µCRL, CS-R 9076[END_REF][START_REF] Groote | The Syntax and Semantics of µCRL[END_REF], which both rely on abstract data types and are similar enough to be considered as the consensual (if not official) valuepassing extension of ACP. PSF introduces variables and expressions in ACP behaviors at four different places:

B ::= ... | g (V 1 , ..., V n ) (parameterized action) | [V ] → B 0 (boolean guard) | sum (x in t, B 0 ) (summation over data) | p (V 1 , ..., V n ) (parameterized process call)
The syntax of µCRL is almost identical, the main difference being that PSF uses (unary) boolean guards whereas µCRL uses (binary) "then-if-else" conditionals "B 1 V B 2 " that can also be expressed as "

[V ] → B 1 + [¬V ] → B 2 ".
The PSF/µCRL approach to data handling is simpler than its counterparts in CSP and LOTOS. Precisely, it is a strict subset of LO-TOS, "g (V 1 , ..., V n )" denoting "g!V 1 ...!V n ", "sum (x in t, B 0 )" denoting "choice x:t[]B 0 ", PSF/µCRL guards and process calls having the same syntax as in LOTOS. Even if this restricted set of PSF/µCRL operators provides the same expressiveness as LOTOS (in the sense that it can generate the same set of labelled transition systems), it has several limitations with respect to convenience and conciseness:

1. Contrary to CCS, CSP, and LOTOS, there is no dedicated syntactic notation to distinguish between emissions and receptions, thus creating omnipresent ambiguities that significantly degrade the readability of behavioral specifications. For instance, a reader confronted to "sum (x in t, g(x))" must rely on some intuitive understanding of the specification to decide whether the writer intended to model the input of x on gate g (noted "g?x:t ; ..." in LOTOS) or the output of some nondeterministic value of type t on gate g (noted "choice x:t[]g!x ; ..." in LOTOS). Paradoxically, LOTOS has been often reproached for having untyped gates [START_REF] Garavel | On the Introduction of Gate Typing in E-LOTOS[END_REF], an issue that does not exist in PSF/µCRL, where the types of action parameters must be explicitly declared; but LOTOS provides different syntax for inputs and outputs, whereas PSF and µCRL cannot express in which direction communications take place. 2. In PSF and µCRL, data values can pass from left to right over the product operator, but only to some limited extent. For instance, it is not possible to directly specify "g 1 ?x:t • g 2 !x", as the lack of difference between emissions and receptions is equivalent to having emissions only. Instead, one must specify "sum (x in t, g 1 (x) • g 2 (x))", with the difference that x is not assigned during an input on g 1 but before, in the summation operator -said differently, a choice that should be external (i.e., determined by the environment) has to be syntactically written as internal (i.e., locally decided by the current process). 3. PSF and µCRL permit simple forms of data-flow sharing. For instance, the aforementioned behavior "(g 1 ?x:t + g 2 ?x:t) • B 3 ", where variable x is visible in B 3 , can be written "sum (x in t, (g 1 (x) + g 2 (x)) • B 3 )" -again, a single internal choice is used to model two different external choices. However, data-flow sharing ceases to be possible as soon as the behavior becomes slightly more complex, e.g., when at least one reception is not an initial action. For instance, "(g

1 ?x:t + τ • g 2 ?x:t) • B 3 " must not be written "sum (x in t, (g 1 (x) + τ • g 2 (x)) • B 3
)", as the summation cannot be moved before the τ -transition without altering the branching structure. One has no other option than writing this behavior "sum (x in t, g 1 (x)

• B 3 ) + τ • sum (x in t, g 2 (x) • B 3
)", thus duplicating B 3 , or introducing an auxiliary process that avoids duplicating B 3 but degrades the readability of the specification.

Rationale for enhancing sequential composition

From the previous section, it is clear that none of the widespread process calculi (namely, CCS, CSP, MEIJE, LOTOS, ACP, PSF, and µCRL) provides an optimal approach to sequential composition. The present section addresses this problem and proposes rationale for a better solution, which has been retained for the LNT language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.2)[END_REF] implemented in the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. The purpose of this section is not to describe LNT in full detail, but to explain how sequential composition should be handled in a modern language.

Forerunner languages

Certain design ideas behind LNT have been put forward in a few precursor languages, which never reached the same level of audience as the widespread process calculi listed above. We pay here a tribute to these almost-forgotten yet inspiring languages by mentioning their contributions and limitations:

• ACP ε is a variant of ACP defined in [START_REF] Koymans | Extending Process Algebra with the Empty Process, Logic Group Preprint Series[END_REF][START_REF] Vrancken | The Algebra of Communicating Processes With Empty Process[END_REF] and mentioned in [START_REF] Baeten | Merge and Termination in Process Algebra[END_REF] [START_REF] Baeten | Process Algebra[END_REF] and [START_REF] Bergstra | Process Algebra with Recursive Operations[END_REF]Chp. 5 [START_REF] Baeten | Formalizing Programming Variables in Process Algebra[END_REF]), it provides a convincing treatment of value passing in the presence of symmetric sequential composition, attempts at making process calculi closer to existing specification and programming languages, and investigates the relationships between Hoare logic, on the one hand, and algebraic and operational semantics, on the other hand.

• ACBS& (Algebra of Broadcasting Systems with Fork ) [START_REF] Weichert | Algebra of Broadcasting Systems: Value Passing, Sequential Composition, and Fork[END_REF] is a process calculus based on ACP ε in which parallel composition and handshake communication are replaced by forking and (asymmetric) broadcasting, respectively. This design choice impacts the sequential composition operator "B 1 • B 2 ", as B 2 can start executing while the processes forked by B 1 are still running as background tasks. Value-passing issues for symmetric sequential composition are discussed, but the problem of uninitialized variables is not mentioned. The conclusion sounds quite pessimistic, stating that symmetric sequential composition has no obvious advantage over action prefix in the presence of value passing.

• Extended LOTOS is a language defined by Ed Brinksma in his PhD thesis [START_REF] Brinksma | On the Design of Extended LOTOS -A Specification Language for Open Distributed Systems[END_REF]. Brinksma, who headed the ISO committee that designed the LOTOS standard, proposed in his thesis a different language bringing ideas and extensions not included in the official version of LOTOS. With respect to the present article, the two most relevant features of Extended LOTOS are its bracketed syntax for n-ary behavioral operators and its tentative merging of LOTOS action prefix and enable operators into a single, compound operator -these features are summarized and discussed in [39, Sec. 9, 12, and 13].

• E-LOTOS (or Enhanced LOTOS) [START_REF]ISO/IEC, Enhancements to LOTOS (E-LOTOS), International Standard 15437[END_REF] is an ISO international standard designed between 1992 and 2001. Undertaking a revision of LOTOS to increase its expressiveness and usability, the E-LOTOS committee eventually produced a new formal language significantly different from LOTOS in many respects, including symmetric sequential composition [56]. Because of its complexity, E-LOTOS has never been implemented, but gave birth to a simplified version named LOTOS NT [START_REF] Garavel | Towards a Second Generation of Formal Description Techniques -Rationale for the Design of E-LOTOS[END_REF][START_REF] Garavel | Compiler Construction using LOTOS NT[END_REF], which itself progressively evolved into LNT.

• OCCAM is a concurrent programming language derived from the original version of CSP [59] [60]. An interesting trait of OCCAM is that its successive versions (1.0 [START_REF] May | OCCAM[END_REF], 2.0 [START_REF] Inmos Limited | OCCAM 2 Reference Manual[END_REF][START_REF] Jones | Programming in occam2[END_REF], 2.1 [START_REF] Inmos Limited | OCCAM 2.1 Reference Manual[END_REF], and 3.0 [START_REF] Barrett | OCCAM 3 Reference Manual, iNMOS Limited[END_REF]) were primarily driven by industrial needs, developed away from the theoretical influence of the CCS and ACP schools, and focused on language usability and implementation issues rather than formal semantics. Yet, academia bridged the gap by proposing various semantics for OCCAM, either denotational [START_REF] Roscoe | Denotational Semantics for Occam[END_REF] [67], algebraical [START_REF] Roscoe | The Laws of Occam Programming[END_REF] [69], or operational [70] [71]. OCCAM made valuable suggestions for symmetric sequential composition and nary behavioral operators; unfortunately, the language has been abandoned after the Transputer project was cancelled, so that the place left by OC-CAM has been taken by the (more traditional) Theoretical CSP process calculus.

In addition to these general-purpose languages, one can also mention a few domain-specific process calculi that also depart from traditional process calculi regarding value passing and sequential composition, e.g., CHP (Communicating Hardware Processes) [START_REF] Martin | Compiling Communicating Processes into Delay-Insensitive VLSI Circuits[END_REF], for which an operational semantics is given in [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF], MoDeST (Modeling and Description Language for Stochastic Timed Systems) [START_REF] D'argenio | MoDeST -A Modelling and Description Language for Stochastic Timed Systems[END_REF][START_REF] Bohnenkamp | MoD-eST: A Compositional Modeling Formalism for Real-Time and Stochastic Systems[END_REF][START_REF] Hahn | A Compositional Modelling and Analysis Framework for Stochastic Hybrid Systems[END_REF], Chi [START_REF] Bos | Redesign of a Systems Engineering Language: Formalisation of χ[END_REF][START_REF] Schiffelers | Formal Semantics of Hybrid Chi[END_REF][START_REF] Van Beek | Syntax and Consistent Equation Semantics of Hybrid Chi[END_REF], and AWN (Algebra for Wireless Networks) [START_REF] Fehnker | A Process Algebra for Wireless Mesh Networks[END_REF].

Design decision #1: Have symmetric sequential composition

In spite of its simplicity and its adoption in most process calculi, action prefix has too many drawbacks that cannot be solved. It is actually a limiting factor that hampers a wider dissemination and acceptance of process calculi. One should thus get rid of action prefix and use instead one single symmetric sequential composition operator, for which the product operator of ACP and the enable operator of LOTOS and CSP provide healthy inspiration. Therefore, LNT includes a binary operator noted ";"6 and two constant operators. So doing, LNT follows the tracks of E-LOTOS and ACP ε . The corresponding BNF rules are the following ones:

B ::= stop (inaction) | null (successful termination) | a (action) | B 1 ; B 2 | ...
• Operator "stop" is the same as "nil" in CCS, "STOP " in CSP, "δ" in ACP, and "stop" in LOTOS. It has no associated SOS rule.

• Operator "null" (the name of which was borrowed from Ada) is the same as "SKIP " in CSP, "exit" in LOTOS, "null" in E-LOTOS, and "ε" in ACP ε . Its operational semantics is given by the following rule:

-

null √ -→ stop
Notice that " √ " is a special action in LNT, rather than a special behavior as in ACP. So doing, LNT follows the choice of CSP, LOTOS, and ACP ε not to have distinguished states and to put all information on transition labels only. Having two different classes of states with respect to termination brings undesirable complexity in software implementations. For instance, equivalence checking and model checking algorithms have to consider information attached not only to transitions but also to states, i.e., operate on Kripke transition systems rather than labelled transition systems. This would also break the expected backward compatibility between LNT and LOTOS.

• In LNT, each action a (different from " √ ") is also a behavior, and its semantics is given (as in ACP and ACP ε ) by the following SOS rule:

-

a a -→ null
• The sequential composition operator of LNT is defined by two SOS rules similar to those for the enable and product operators. The first rule is the same as in CSP, LOTOS, and ACP ε . The second rule is borrowed from ACP ε and differs from CSP and LOTOS by not creating a τ -transition when the control flow passes over sequential composition:

B 1 a -→ B 1 ∧ a = √ B 1 ; B 2 a -→ B 1 ; B 2 B 1 √ -→ B 1 ∧ B 2 a -→ B 2 B 1 ; B 2 a -→ B 2 4.
3. Design decision #2: Have "true" (i.e., write-many) variables Another feature that isolates process calculi from mainstream programming languages is the status of variables. Following the leading influence of CCS, most process calculi use exclusively immutable variables (also: dynamic constants), which are assigned only once, at the point they are declared, and whose values cannot change afterwards -unless by creating new, distinct instances of the variables (e.g., parameter instantiation). This functional style sharply contrasts with mainstream programming languages, in which imperative style with multiple assignments to variables is the norm.

The main advantage of the functional style is a slight simplification of syntax (as declarations and initializations of variables occur at the same place) and operational semantics (as assignments to variables can be expressed using substitutions). But, from a practical point of view, the functional style is not flexible enough to let values naturally pass from left-to-right over sequential composition and permit data-flow sharing.

Below are given six desirable value-passing examples; the four latter ones cannot be properly specified without departing from the functional style in two key points: (i) declarations of variables and assignments to variables must be syntactically dissociated, and (ii) it must be possible to assign the same variable at different places, e.g., in the various branches of deterministic and nondeterministic choices:

g 1 ?
x where x > 0 ; g 2 !(x + 1)

g 1 ?x 1 ; g 2 ?x 2 ; g 3 !(x 1 + x 2 ) (g 1 ?x[]g 2 ?x) ; g 3 !(x + 1) ((g 1 ?x 1 ; g 2 ?x 2 )[](g 2 ?x 2 ; g 1 ?x 1 )) ; g 3 !(x 1 + x 2 ) if x 2 > 0 then g 1 ?x 1 else x 1 := 0 end if ; g 2 !(x 1 + x 2 ) case x 2 in 0 → g 1 ?x 1 | 1 → x 1 := 0 end case ; g 2 !(x 1 + x 2 )
In the four latter examples, assignments to the same variables are alternative, as they occur on mutually exclusive branches. One may go further by permitting successive assignments, so that the values of variables can evolve in time; this is clearly needed to directly express loops (i.e., without using recursive process definitions), as the values computed at some iteration must be passed to the next iterations.

So far, very few process calculi dared to deviate from the functional style set by CCS. Interestingly, the original version of CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF] was imperative, as well as its descendents CHP and OCCAM, but CSP later adopted the functional style with Theoretical CSP [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF] and shows no intention to switch back [5, p. 132-133]. Extended LOTOS proposed a mixed approach, in which locally imperative sequential code fragments are immersed in a globally functional process calculus [38, chapter 6]. The E-LOTOS standard went further by introducing a unique symmetric sequential composition operator and implementing points (i) and (ii) above: dissociation between variable declarations and assignments, and possibility of alternative assignments; however, E-LOTOS only featured "write-once" variables, explicitly deferring "write-many" variables to a future revision of the standard.

In the realm of mobile processes, the update calculus [START_REF] Parrow | The Update Calculus (Extended Abstract)[END_REF] proposes a similar dissociation between, on the one hand, the declaration of a name x local to behavior P (which is done using a scope operator noted "(x)P ") and, on the other hand, the substitution of all occurrences of x by y (noted "[y/x]") or by some value received on port a (noted "ax"); such dissociation is a key difference with the π-calculus where declarations and input actions are bound together; notice however that the update calculus is based on action prefix and uses name substitutions rather than genuine assignments.

Actually, write-many variables are only used in a handful of process calculi.

Beside CHP and OCCAM, one can mention ACBS&, ACP G (where modifications of state variables, such as assignments, must be attached to visible or "τ " transitions), AWN and Chi (where each assignment systematically creates a potentially undesirable τ -transition), and MoDeST (where assignments may only occur as operands of a probabilistic choice taking place after a visible or "τ " action). LNT does not have such restrictions and handles "write-many" variables in the same way as most imperative programming languages do. Focusing on the places where variables are declared and modified, the BNF rules for LNT behaviors are extended as follows (brackets "[...]" meaning optional):

B ::= ... | var x:t in B 0 end var variable declaration | x := V (deterministic) assignment | x := any t [where V ] nondeterministic assignment | g (O 1 , ..., O n ) [where V ] value-passing action | p [g 1 , ..., g m ] (N 1 , ..., N n ) process call | ... O ::= [!]V emission offer | ?x [where V ] reception offer N ::= V "in" parameter | ?x "out" parameter | !?x "in-out" parameter
These rules deserve a few comments:

• The "var" operator declares a variable that only exists in the scope of behavior B 0 . This operator (similar to, e.g., the "var" operator of Esterel) is the dual of the "hide" operator of LOTOS, which declares a gate only visible in the scope of a given behavior; such duality between variables and gates goes further because the only other places where variables (resp. gates) can be declared are the formal variable (resp. gate) parameters of process definitions. Notice that the ability to declare local variables does not exist in all process calculi; for instance, ACP G only allows global variables.

• The "where V " optional clauses (called selection predicates in LOTOS) are Boolean constraints specifying the acceptable values for nondeterministic assignments and value receptions.

• To follow Ross's uniform referents principle [START_REF] Ross | Uniform Referents: An Essential Property for a Software Engineering Language[END_REF] and to pave the way for action refinement [START_REF] Gorrieri | Action Refinement[END_REF], the syntax adopted for value-passing actions in LNT is a mix between CCS (the "?" symbol is kept and the "!" symbol becomes optional) and PSF/µCRL (value-passing actions are written with the same conventions as function and procedure calls in programming languages).

• In the imperative style of LNT, processes can have "in" parameters (call by value), "out" parameters (call by result), and "in out" parameters (call by value-result). The evaluation strategy is strict.

Notice that the dissociation between variable declarations (using the "var" operator) and variable modifications (i.e., assignments or receptions) is the only way to defeat the impossibility claim of [START_REF] Baeten | On Sequential Composition, Action Prefixes and Process Prefixes[END_REF] recalled in Sec. 3.3 above: sequential composition can indeed be associative as expected if its operands do not declare variables but only modify them.

The syntax proposed for LNT behaviors is permissive enough to express all aforementioned examples. However, it is not free from difficulties, which we consider in the next sections.

Design decision #3: Prohibit uninitialized variables

Unfortunately, certain behaviors accepted by the syntax of LNT have no obvious semantics.

For instance, the behavior B defined as "(g 1 ?x 1 []g 2 ?x 2 ) ; g 3 !(x 1 + x 2 )" is problematic because, depending on which execution branch is taken, either x 1 or x 2 is not assigned, and thus the sum (x 1 + x 2 ) may be undefined. However, this behavior B becomes trouble-free if inserted in some larger behavior, such as "x 1 := 0 ; x 2 := 0 ; B". Various approaches can be considered for this problem:

1. The semantics could (explicitly or implicitly) state that reading uninitialized variables has "undefined" (i.e., implementation-dependent) effects. This is a usual solution for imperative languages (e.g., C) and sometimes for process calculi as well (e.g., CHP and, to some extent, the early versions of Chi in which undefined variables are said to remain symbolic when evaluating expressions [83, pp. 54 and 250] [77, p. 375]). However, this solution is unacceptable in the context of formal methods; moreover, determining whether a behavior is "undefined" or not is undecidable in general -this is equivalent to the halting problem. 2. The semantics could implicitly initialize each variable to some default value when the variable is declared. This is the approach taken in Eiffel, which automatically sets integers to zero, Booleans to false, etc. Such a semantics is formal, but presents the risk of silently hiding user mistakes, namely all forgotten assignments with values different from the default ones. 3. The semantics could state that reading an uninitialized variable triggers some particular behavior. For instance, the various definitions of OCCAM are not very precise on this matter, but it seems that any behavior requiring the evaluation of an expression containing some uninitialized variable should behave like "STOP" [63, pp. 17 and 215], although the OCCAM compiler can also be instructed to halt the whole system in such event [62, Annex E]. Alternatively, a catchable exception [START_REF] Garavel | On the Introduction of Exceptions in LO-TOS[END_REF] could be raised. In such approaches, the detection of user mistakes is postponed at run time, which is not advisable for safety-and security-critical designs. 4. The semantics could state that reading an uninitialized variable provokes a nondeterministic assignment ("x := any t") to this variable. Such a semantics would be formal, but it would be non-standard (although it has been implemented in a CHP-to-LOTOS translator [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF]) and would also hide user mistakes (yet, complexity explosions occurring during statespace generation could indirectly inform the user about potential mistakes). 5. Our idea consists in adding static semantics constraints that reject syntactically correct, yet semantically problematic behaviors. This is standard practice in programming languages, where static semantics rules out programs containing, e.g., undefined identifiers, mistyped expressions, etc. This way, one can introduce restrictions to ensure that all variables are properly initialized; this idea was first experimented in IBM's NIL and Hermes languages [START_REF] Strom | Typestate: A Programming Language Concept for Enhancing Software Reliability[END_REF] and later adopted in Java.

LNT follows the fifth approach. The LNT compiler implements data-flow analysis techniques to statically detect and reject "dubious" specifications in which some variables might be used before set.

Of course, it is not possible to decide, for all specifications, whether all variables are set before used, but one can check instead sufficient conditions that only accept those specifications in which a proper initialization of variables can be proven, and reject all other specifications in which such initialization is uncertain. There is obviously a risk of rejecting specifications that make sense; for instance, the current LNT compiler front-end does not accept the following behavior:

if x 1 ≤ x 2 then x 3 := 0 end if ; if x 2 > x 1 then g (x 3 ) end if
because the analysis is not involved enough to discover that the second condition is implied by the first one. In practice, such false positives are not too frequent, and it is not so difficult to modify an LNT specification to get it accepted by the compiler. Moreover, the experience with Java indicates that data-flow constraints uncover many mistakes and are appreciated by programmers. Finally, the data-flow algorithms are always perfectible and will certainly benefit, for instance, from recent advances in static analysis and SAT/SMT solvers; the set of accepted LNT specifications is thus expected to grow as time passes.

Looking retrospectively at traditional process calculi, it is clear they also set constraints to rule out unwanted behaviors. For instance, action prefix in CCS and "input-only" actions in PSF/µCRL are two different means to forbid problematic behaviors such as "(g 1 ?x 1 []g 2 ?x 2 ) ; g 3 !(x 1 + x 2 )". But these are syntactic restrictions, i.e., very primitive defense means that bluntly reject many meaningful and useful behaviors. To the contrary, the LNT approach has a more permissive syntax combined with static semantics restrictions, leading to a language that is more flexible and closer to end-user intuition and expectations.

Design decision #4: Prohibit shared variables

The dissociation between declarations of variables and assignments to variables, together with the introduction of "write-many" variables creates new issues with parallel composition as well. For instance, it allows behaviors of the form "var x:t in (g 1 (?x) || g 2 (?x)) ; g 3 (x) end var", where "||" denotes some parallel composition operator, so that x is actually a shared variable, whose semantics depends on the possible interleavings.

This issue has been diversely addressed in the various forerunner languages that permit variable assignment. In CHP, for instance, such situation cannot occur due to a restrictive syntax: there is no explicit parallel composition operator, so that concurrent processes operate in disjoint memory spaces without shared variables. In OCCAM, a parallel composition is considered to be invalid if any of its branches may change the value of a variable used in another branch; this situation is handled at run time: in such case the parallel composition may stop (while other parts of the system continue their execution) or halt the entire system. In ACBS&, each parallel branch forks to execute in its own memory space that contains copies of shared variables; race-condition issues are thus deferred until join points when forked processes return, with several possible semantics to merge once-separate memory spaces [START_REF] Weichert | Algebra of Broadcasting Systems: Value Passing, Sequential Composition, and Fork[END_REF]Sec. 6.4].

LNT follows a similar approach to OCCAM, but ensures the existence of a formal semantics. Rather than stopping or halting at run time, LNT adds static semantic constraints that forbid at compile time all (syntactically correct) behaviors involving shared variables. Namely, all parallel branches can see the variables declared in an enclosing scope; by default, all parallel branches can read such shared variables, but if a branch writes to a shared variable, the other branches can neither write nor read this variable. When parallel composition terminates, the disjoint variables computed by each branch are merged into a single memory space, e.g., "var x 1 , x 2 :t in (g 1 (?x 1 ) || g 2 (?x 2 )) ; g 3 (x 1 + x 2 ) end var" -actually, this corresponds to the "combine" semantics of ACBS& [START_REF] Weichert | Algebra of Broadcasting Systems: Value Passing, Sequential Composition, and Fork[END_REF]Sec. 6.4.3].

With such a design decision, LNT remains in the strict message-passing framework of traditional process calculi, as the most direct motivation behind LNT was the need for a better language to replace LOTOS in academia and industry. On the longer term, static semantics restrictions on shared variables could be relaxed, giving a nice opportunity to combine message-passing and shared-memory paradigms in the same formal language. Work in this direction already exists, such as ACP G , which allows shared variables without restriction (race conditions leading to nondeterminism, as each variable keeps the last value it was assigned during the interleaved execution of parallel branches). The aforementioned shared-variable languages that translate to traditional process calculi [2, Chapter 8] [27] [28] [5, Chapter 18] also provide a basis for reflection. However, given the multiplicity and complexity of shared-memory models, machines, and languages, a deep reflection is needed if one wants to produce a language general enough to accurately model a variety of parallel hardware and software.

Design decision #5: Prohibit complex forms of process recursion

It is well-known from the ACP body of knowledge that symmetric sequential composition opens the way to context-free recursion, e.g., process definitions of the form "p = (a 1 • p • a 2 ) + a 3 ", a situation syntactically prohibited by action prefix operator. Also, "write-many" variables may lead to problematic behaviors when combined with recursion and other operators.

Such issues have not yet been fully explored in LNT, for two reasons. First, such forms of process recursion are not so useful in practice, as the desired behaviors can be described in a different way, using regular processes with additional variables to encode recursion stacks. Second, LNT is currently implemented by translation to LOTOS, and the LOTOS compiler of CADP [START_REF] Garavel | Compilation and Verification of LOTOS Specifications[END_REF] does not accept recursion through parallel composition operators, nor on the left-hand side of the enable and disable operators.

Therefore, restrictions have been added to the static semantics of LNT in order to disallow such forms of recursion. Relaxing these restrictions should trigger future investigation, based on existing work to automatically eliminate non-tail process recursion [START_REF] Groote | Linearization in Parallel pCRL[END_REF]. Notice that no similar restrictions exist for recursive functions, because LNT functions are translated to C functions, thus deferring the handling of recursion to the C compiler.

Design decision #6: Have structured programming constructs

Most of the discussion above is about sequential composition. Regarding the remaining behavioral operators, the following remarks can be made:

1. With traditional process calculi, it was sometimes tricky to introduce certain operators, such as the empty process or loops. These difficulties vanish once symmetric sequential composition and "write-many" variables are adopted. Introducing the usual structured programming constructs then becomes straightforward. LNT has thus most Ada-like constructs, including "if-then-else" with "elsif ", "case", forever "loop" with "break", "while" loop, "for" loop, etc. Notice that the "case" operator of LNT supports ML-like pattern matching, whereas traditional process calculi have no "case" operator at all in their control part, partly compensated with algebraic equations in their data part only. Nearly 70% of LNT behavioral operators look familiar to average computer scientists; this favors the acceptance of the language. 2. Opting for such imperative programming constructs (disciplined by static semantics constraints on variable initialization) brings a proper solution to another problem faced by most specification languages based on process calculi: the coexistence of two different languages, one to describe the control part (namely, communication channels and processes), and another one to describe the data part (namely, types and functions). For the latter part, algebraic data types have been often used (e.g., in LOTOS, ACP/SDF, ACP/COLD, PSF, µCRL, mCRL2, etc.), but functional language are also possible, as in LCS (which combines CCS and ML) [START_REF] Berthomieu | Programming with Behaviors in an ML Framework -The Syntax and Semantics of LCS[END_REF] or CSP M (which combines CSP and Haskell) [START_REF] Roscoe | The Theory and Practice of Concurrency[END_REF]Appendix B]. Whatever the approach chosen, juxtaposing two languages increases complexity and often violates the uniform referents principle: in most process calculi, for instance, "if-then-else" conditionals are expressed very differently whether they occur in the control part or in the data part, causing much confusion among beginners.

To our knowledge, the ISO committee that designed E-LOTOS was the first to state this problem and propose a unifying approach in which the language to describe functions is a subset of the language to describe processes. LNT follows the same inspiration, by considering a function as a restricted form of process that is deterministic, cannot perform (visible nor internal) actions, and in which only sequential programming constructs can be used -to be complete, there is a minor exception to this rule at the moment: functions can return a result using a "return" construct that processes do not have, but this could easily be addressed by allowing processes as well to (optionally) return results when they terminate, keeping in mind that processes already have "out" and "in out" parameters. 3. The remaining behavioral operators that can be used in processes (but not in functions) are: nondeterministic choice (noted "select" as in Ada), nondeterministic assignment ("x := any t"), parallel composition (which, in LNT, is based on the so-called graphical parallel operators [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF]), action hiding, and disruption (i.e., the disable operator noted "[>" in LOTOS). 4. Process calculi were originally designed to reason about small yet salient examples but have been later used to model increasingly large systems. At this point, the algebraic syntax becomes a nuisance for readability, leading to (LISP-like) excessive nestings of parentheses. LOTOS tried to address this issue by defining eight levels of precedence between behavioral operators, but these levels are not intuitive and provoke mistakes that are difficult to catch.

A better solution was proposed by OCCAM, which replaced binary operators by n-ary operators ("SEQ B 1 ...B n " for sequential composition, "ALT B 1 ...B n " for choice, "PAR B 1 ...B n " for parallel composition, etc.), while relying on indentation levels 7 to disambiguate nested behaviors. Such a proposal actually conveyed the hidden yet subversive message that a language for concurrency could choose the most appropriate syntax and was not fatally bound to imitate arithmetics. The OCCAM solution was improved in Extended LOTOS, which suppressed the questionable reliance on indentation levels by introducing fully bracketed n-ary constructs, e.g., "seq B 1 ; ... ; B n endseq" for sequential composition, "sel B 1 []...[]B n endsel" for choice, "par B 1 ||...||B n endpar" for parallel composition, etc. This idea, retained for E-LOTOS, was also adopted for LNT with two differences inspired from Ada: removing the "seq" and "endseq" keywords (which are not needed if all other constructs are properly bracketed), and splitting each keyword "endxxx" into "end xxx" to reduce the overall number of keywords. MoDeST chose a similar approach, using instead a C-like syntax with braces. Notice that bracketed n-ary operators are the most sensible option to introduce "case", graphical parallel composition [START_REF] Garavel | A Graphical Parallel Composition Operator for Process Algebras[END_REF], and probabilistic choice operators, at least.

Formal definition of LNT

The definition of traditional process calculi consists of two parts: syntax and dynamic semantics, the latter being specified algebraically (axioms) or operationally (SOS rules). Due to the design choices for LNT, a third part must be added, static semantics, which is usually absent from traditional process calculi or kept to a minimum (e.g., a few rules stating that value expressions must be well-typed). In LNT, static semantics is larger and cannot be overlooked, as it is a condition for the soundness of dynamic semantics.

In practice, one observes that new users learn the syntax and static semantics of LNT, but tend to ignore the dynamic semantics, based upon the (reasonable) assumption that anything permitted by the syntax and not forbidden by the static semantics should work simply just as expected. Although such a situation is annoying from a semanticist's point of view, it is in line with mainstream programming languages, the formal semantics of which is only studied by standardization committees, compiler writers, and test-suite producers, rather than being a prerequisite to start using the language.

The syntax, static semantics, and dynamic semantics of LNT are given in [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.2)[END_REF]. Formalized by Frédéric Lang, the dynamic semantics is defined operationally [30, Annex B] and comprises two parts:

• For LNT functions, each memory state is represented as a store, i.e., a mapping from variables to their current values; the execution of LNT constructs defines transitions between these states (i.e., store updates).

• For LNT processes, the dynamic semantics is given in terms of labelled transition systems. Following a minoritarian yet longstanding tradition [START_REF] Plotkin | A Structural Approach to Operational Semantics[END_REF][START_REF] Plotkin | A Structural Approach to Operational Semantics[END_REF] [START_REF] Mousavi | Congruence for SOS with Data[END_REF][START_REF] Mousavi | Notions of Bisimulation and Congruence Formats for SOS with Data[END_REF], each state is defined as a pair8 B, σ , where B is a behavior and σ a store, rather than a behavior only 9 . SOS rules define transitions between states; static semantics restrictions avoid complications, ensuring that each variable read has a defined value and avoiding race conditions when the store is accessed.

The dynamic semantics of LNT being too large (17 pages) to be entirely reproduced here, we only give a few salient SOS rules and compare them with the rules of ACP G [51, Fig. 3 and9]. Let " V, σ -→ v" denote that a value expression V evaluates to v in store σ, and let " B, σ a -→ B , σ " denote that it exists a transition labelled a from state B, σ to state B , σ . The two first rules extend, by adding stores, those already given in Sec. 4.2:

-

null, σ √ -→ stop, σ - g, σ g -→ null, σ
The two next rules consider actions with emission and reception offers (these are not supported in ACP G ):

V, σ -→ v g (V ), σ g (v) -→ null, σ v ∈ type(x) ∧ σ = σ[x/v] ∧ V, σ -→ true g (?x) where V , σ g (v)
-→ null, σ

where type(x) denotes the type of variable x, and where σ[x/v] is the store obtained from σ by assigning value v to variable x. The two next rules define deterministic and nondeterministic assignments:

V, σ -→ v x := V , σ √ -→ stop, σ[x/v] v ∈ t ∧ σ = σ[x/v] ∧ V, σ -→ true x := any t where V , σ √ -→ stop, σ
Although such assignments can also be expressed in ACP G (by means of state transformers), they must be attached to visible or "τ " transitions, whereas LNT is more general by attaching them to √ -transitions; as a consequence, √ -transitions never modify the store in ACP G , whereas they can in LNT. Another difference is that ACP G requires state transformers to have at least one solution, whereas LNT does not -namely, the condition V used in a Boolean guard "where V " is allowed to be always false, in which case the assignment or reception containing this guard is simply equivalent to "stop". Finally, the two main rules for value-passing sequential composition are the following ones (a third rule is actually needed to model the "break" statements used to exit from loops):

B 1 , σ a -→ B 1 , σ ∧ a = √ B 1 ; B 2 , σ a -→ B 1 ; B 2 , σ B 1 , σ √ -→ B 1 , σ ∧ B 2 , σ a -→ B 2 , σ B 1 ; B 2 , σ a -→ B 2 , σ
These rules are similar to those of ACP G , except that the second premiss of the second rule differs:

ACP G uses B 2 , σ a -→ B 2 , σ whereas LNT uses B 2 , σ a -→ B 2 , σ because √
-transitions can modify the store in LNT but not in ACP G .

Comparison with traditional process calculi

In this section, we discuss the relationship between LNT and established process calculi, focusing on sequential composition and excluding from the comparison the well-known differences arising from parallel composition, binary vs. multiway synchronization, hiding and/or renaming of actions, etc.

As a preliminary remark, it is worth noticing that LNT without its choice, parallel, hiding, and disabling operators, provides a small yet powerful language offering a combination of imperative and functional traits. This allows LNT to be taught in successive steps, starting from well-known sequential aspects, then progressively introducing concurrency-related features.

Expressiveness of LNT

The design of LNT is not driven by the desire to increase theoretical expressiveness, but by pragmatic considerations about the wide applicability of the language. At present, LNT is implemented by translation to LOTOS, so as to reuse the compilers already available in the CADP toolbox. More precisely, LNT is translated into a combination of LOTOS (slightly extended by allowing the enable operator ">>" not to create extra τ -transitions) and C (which serves to efficiently implement certain LNT types that do not exist in LOTOS, e.g., floating-point numbers and character strings). Despite these extensions, we conclude that the expressiveness of LNT is roughly the same as that of LOTOS.

Encoding of regular expressions in LNT

To start with a simple example, the following function T translates a regular expression R to an LNT behavior such that the automaton obtained from the labelled transition system of T (R) by considering as accepting states all states having an outgoing √ -transition recognizes the language of R; the two last equations extend the definition of T to ω-regular expressions:

T (ε) = null T (g) = g T (B 1 • B 2 ) = T (B 1 ) ; T (B 2 ) T (B 1 + B 2 ) = select T (B 1 ) [] T (B 2 ) end select T (B * ) = loop select T (B) [] break end select end loop T (B ∞ ) = loop T (B) end loop T (B ω ) = select T (B * ) [] T (B ∞ ) end select
Studies of the correspondences between regular expressions and process calculi when considering stronger relations rather than language equivalence can be found in [START_REF] De Nicola | A Completeness Theorem for Nondeterministic Kleene Algebras[END_REF][START_REF] Corradini | Fully Abstract Models for Nondeterministic Regular Expressions[END_REF][START_REF] Corradini | Models of Nondeterministic Regular Expressions[END_REF] and [START_REF] Baeten | Regular Expressions in Process Algebra[END_REF][START_REF] Baeten | A Characterization of Regular Expressions Under Bisimulation[END_REF].

Encoding of CCS in LNT

Migrating from CCS to LNT can easily be done using the following function T that translates a CCS term to an LNT behavior:

T (nil) = stop T (g.B) = g ; T (B) T (g(V ).B) = g(V ) ; T (B) T (g(x).B) = g(?x) ; T (B) T (τ.B) = i ; T (B) T (B 1 + B 2 ) = select T (B 1 ) [] T (B 2 ) end select T (if V then B) = only if V then T (B) end if
The "only" keyword before the "if " implicitly adds a blocking "else stop" rather than the default clause "else null" added by default when "only" is absent. Also, each CCS process call is translated to a corresponding LNT process call, but it is also possible to express recursive CCS processes using the "loop" operators of LNT. As stated above, the parallel, relabelling, and restriction operators are left out of the discussion. The same remarks will also apply to the next sections.

Encoding of (value-passing) ACP in LNT

Similarly, many operators of ACP, PSF, and µCRL have a simple counterpart in LNT, given by the following function T that translates an ACP term to an LNT behavior:

T (δ) = stop T (ε) = null T (g) = g T (g(V 1, ..., V n)) = g(V 1, ..., V n) T (τ ) = i T (B 1 • B 2 ) = T (B 1 ) ; T (B 2 ) T (B 1 + B 2 ) = select T (B 1 ) [] T (B 2 ) end select T ([V ] → B) = only if V then T (B) end if T (B 1 V B 2 ) = if V then T (B 1 ) else T (B 2 ) end if
T (sum (x in t, B)) = var x:t in x := any t ; T (B) end var One should of course keep in mind that " √ " is a state in ACP and a transition in LNT, leading to minor differences in the labelled transition systems: for instance, the LTS of "ε" in ACP has one state and no transition, whereas the LTS of "null" in LNT has two states and one √ -transition; similarly, the LTS of an action in ACP has two states and one transition, whereas the LTS of that same action in LNT has three states and two transitions (the last one being a √ -transition).

Encoding of LOTOS and CSP in LNT

As mentioned above, LNT is currently implemented by translation to LO-TOS. But the reverse translation from LOTOS to LNT is possible -and much simpler. It is given by the following function T that translates a LOTOS term to an LNT behavior; this translation also holds (modulo notational changes) for a large fragment of CSP:

T (stop) = stop T (exit) = null T (g ; B) = g ; T (B) T (g!V ; B) = g(V ) ; T (B)
T (g?x:t ; B) = var x:t in g(?x); T (B) end var T (g?x:t [V ] ; B) = var x:t in g(?x) where V ; T (B) end var

T (i ; B) = i ; T (B) T (B 1 []B 2 ) = select T (B 1 ) [] T (B 2 ) end select T ([V ] → B) = only if V then T (B) end if T (let x:t = V in B) = var x:t in x := V ; T (B) end var T (choice x:t []B) = var x:t in x := any t ; T (B) end var T (B 1 >>B 2 ) = T (B 1 ) ; i ; T (B 2 ) T (B 1 [>B 2 ) = disrupt T (B 1 ) by T (B 2 ) end disrupt
Despite their apparent simplicity, certain equations above are not trivial. For instance, the third equation converts an asymmetric action prefix operator into a symmetric sequential composition operator. The two next equations are given only for the emission/reception of a single offer, but naturally extend to the case of multiple offers.

The translation of value-passing "exit" and ">> accept" operators is more involved and not described by the above equations. The key idea is that LNT totally suppresses the need for such complex operators, which have been (for good reasons) introduced in LOTOS long ago. In essence, the elimination of these operators is summarized by the two following equations: T (... exit(V ) >> accept x:t in B) = ... i ; var x:t in x := V ; T (B) end var T (... exit(any t) >> accept x:t in B) = ... i ; var x:t in x := any t ; T (B) end var

Assessment on design patterns

In Sec. 3, several examples have been given that cannot be conveniently expressed in traditional process calculi. The present section goes further by providing larger examples (borrowed from typical design patterns) that can clearly be better expressed in LNT than with former process calculi.

Design pattern #1: Control-flow sharing

The benefits of control-flow sharing (i.e., the ability to specify dag-like patterns and not only tree-like patterns) have already been demonstrated on small examples. Here is a more involved LNT example featuring a sequence of "ifthen" conditionals -similar examples could be built using sequences of "ifthen-else", "case", or "select" operators:

--here, let x 1 , x 2 , ..., x n be initialized integer variables if x 1 = 0 then g (?x 1 ) end if ; if x 2 = 0 then g (?x 2 ) end if ; ...

if x n = 0 then g (?x n ) end if ; g (x 1 + x 2 + ... + x n )
Traditional process calculi do not allow to concisely express this example: they require a quadratic complexity in the number of variables, whereas LNT permits a linear complexity. Using LOTOS would be the best option: a sequence of (n -1) enable operators could be used, the (i + 1)-th operator having an "accept" clause to get all variables x 1 , ..., x i ; therefore, n(n -1)/2 auxiliary variables would be needed. For other languages based on action prefix, the only option to avoid unfolding 2 n branches would be to introduce (n -1) auxiliary processes, the (i + 1)-th process having i parameters to get the values of x 1 , ..., x i ; again, n(n -1)/2 auxiliary variables would be needed (in addition to the processes themselves). For the ACP-based languages PSF and µCRL, despite symmetric sequential composition, the introduction of (n -1) auxiliary processes totalling n(n -1)/2 parameters is also unavoidable, given that input actions are not allowed, and that summations and process calls are the only places where variables can be bound to values. No need to emphasize that quadratic-size specifications are error prone, and tedious to write, read, and maintain.

Design pattern #2: Guarded commands

A second class of patterns that are easier to express using LNT than traditional process calculi are Dijkstra's guarded commands [START_REF] Dijkstra | Guarded Commands, Non-determinacy and Formal Derivation of Programs[END_REF], which many model checkers adopted as their input language. LNT can express guarded commands naturally and concisely, e.g.:

var x 1 , x 2 , ..., x n :int in x 1 := 0 ; x 2 := 0 ; ... ; x n := 0 ; loop select only if x 1 < 10 then x 1 := x 1 + 1 ; B 1 end if [] only if x 2 < 10 then x 2 := x 2 + 1 ; B 2 end if []...[] only if x n < 10 then x n := x n + 1 ; B n end if end select end loop end var
where B 1 , B 2 , ..., B n can be arbitrary behaviors. Using traditional process calculi that lack a "loop" operator, one must introduce a recursive process with n parameters x 1 , x 2 , ..., x n . Because this process is called n times (once per branch), n 2 actual parameters are passed. Therefore, the size of the code, linear in LNT, becomes quadratic. The need to extend ACP-like value-passing process calculi to properly express guarded commands was acknowledged in [START_REF] Groote | Process Algebra with Guards: Combining Hoare Logic with Process Algebra[END_REF]Sec. 6].

Design pattern #3: Map-Reduce

In distributed computing, the map-reduce pattern is a means to divide a task between parallel workers. For instance, given n inputs x 1 , x 2 , ..., x n and an expression "f (f 1 (x 1 ), f 2 (x 2 ), ..., f n (x n ))" to compute, where f, f 1 , f 2 , ..., f n are function symbols, one can ask n workers to compute the partial results "y i = f i (x i )" in parallel. This pattern can easily be expressed in LNT, where parallel branches can assign variables declared in their enclosing scope(s):

--here, let x 1 , x 2 , ..., x n be initialized variables var y 1 , y 2 , ..., y n :t in par

y 1 := f 1 (x 1 ) || y 2 := f 2 (x 2 ) ||...|| y n := f n (x n ) end par ; g (f (y 1 , y 2 , ..., y n )) end var
Among traditional process calculi, LOTOS is probably the one that can most concisely express this pattern. This can be done using the ">> accept" operator, but with a quadratic complexity as n "exit" operators (each with n arguments) are needed:

--here, let x 1 , x 2 , ..., x n be initialized variables ( exit(f 1 (x 1 ), any t, ..., any t) ||| exit(any t, f 2 (x 2 ), ..., any t) |||...||| exit(any t, any t, ..., f n (x n )) ) >> accept y 1 , y 2 , ..., y n :t in g !f (y 1 , y 2 , ..., y n ) ; ... It is worth noticing that the above LOTOS fragment is not compositional, as each branch must be aware of its own position in the parallel composition to properly pass arguments to "exit". Moreover, the addition of an (n + 1)-th branch would require to modify all the branches.

Other traditional process calculi than LOTOS lack a native synchronized termination in which each parallel branch could contribute by passing its locally computed results. The map-reduce pattern can still be expressed in these calculi by introducing auxiliary gates to mimic LOTOS "exit" and ">>" operators; the complexity is also quadratic (counting the number of offers passed to these gates) and the modelling remains not compositional.

Beyond condition/actions models

Close in essence to guarded commands, condition-action transition systems are often used in model checkers and academic lectures on automated verification. Such systems have states, variables, and transitions; a transition can be fired if its associated Boolean condition is true; firing a transition triggers its associated action, i.e., a set of assignments that modify variables.

Condition/action models have the merit of simplicity, but lead to transition systems larger than actually needed. For this reason, they have been sharply criticized in [START_REF] Garavel | NTIF: A General Symbolic Model for Communicating Sequential Processes with Data[END_REF], where an alternative model named NTIF is proposed. LNT follows the principles of NTIF: in particular, it features blocks of sequential code (deterministic and nondeterministic assignments, conditionals, iterations) that execute atomically, i.e., without creating any visible or τ -transition. This is implemented by the definition of sequential composition in LNT: for instance, each assignment creates one √ -transition but a sequence of assignments only creates one single √ -transition, as the LNT sequential composition operator merges two successive √ -transitions in one. The flexible style permitted by LNT can be illustrated on the small excerpt below, which was taken from a much larger specification. The structure of the code shows that what is needed in practice is far more involved than mere conditions/actions. For instance, the second "select" is used to enumerate a finite number of values from an infinite type domain -notice that there are no visible or τ actions at all in the branches of this choice. Also, the "while" loop corresponds to a statically unbounded number of assignments.

--let x and x be two lists of integers x := {} ; loop select g (?x ) ;

x := insert (x, x ) [] select x := {} [] x := {0, 1} [] x := {1, 0, 2} end select ; g (x ) ; while x = {} loop
x := remove (x, head(x )) ; x := tail(x ) end loop end select end loop 7. Conclusion

Summary of Contributions

Process calculi are the prime vehicle for disseminating concurrency theory knowledge to other branches of computer science and to industry as well. Questioning tradition and designing better languages is an essential part of this agenda. Sequential composition is often overlooked as an easy problem of secondary importance. But, as discussed in Sec. 3, the various approaches to sequential composition adopted by mainstream process calculi (namely, CCS, CSP, ACP, LOTOS, PSF, µCRL, and mCRL2) all suffer from serious shortcomings. A few other process calculi mentioned in Sec. 4.1 (namely, ACP ε , ACP G , ACBS&, Extended LOTOS, E-LOTOS, and OCCAM) tried to propose better approaches, but had little success and are almost forgotten.

Considering sequential composition as a central topic in the design of modern process calculi, the present article has presented a carefully-motivated solution, which features a unique sequential composition operator, together with "writemany" variables and static semantics data-flow constraints ensuring, among other suitable properties, that all variables are properly set before use.

The advantages of the proposed solution, which has been retained for the LNT language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.2)[END_REF], are fourfold: (i) it is simple and easy to learn, as it matches the knowledge and intuition of software engineers; (ii) it allows to describe data and control using the same language (functions being a subset of processes) rather than two different sub-languages; (iii) it unifies and supersedes the various sequential composition operators that exist in traditional calculi, which can be "upgraded" to LNT using simple translation functions given in Sec. 5; (iv) it enables useful design patterns to be expressed in LNT with a linear complexity, where traditional process calculi require a quadratic complexity as shown in Sec. 6.

Implementation and Feedback

From 2005 to 2014, the proposed solution has been fully implemented in the LNT→LOTOS translator that is part of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. Since 2011, LNT has been successfully taught at ENSIMAG (Grenoble INP), the first French engineering school in computer science, and appears significantly faster to learn than LOTOS: lectures can indeed focus on "important" operators (e.g., choice, parallel composition, and hiding) rather than spending time explaining the intricacies of action prefix and enable. Quoting Hoare's remark [START_REF] Hoare | The Transputer and Occam: A Personal Story[END_REF] about the design of the "ALT" operator in OCCAM, and hoping that the same remark also holds for sequential composition in LNT: "as in all branches of engineering, the user of a product should never have to notice the skill with which the engineer has improved the design; true skill is that which conceals itself ".

LNT is also used in a growing number of case studies 10 and receives positive feedback from industry partners noticing major productivity boosts; quoting STMicroelectronics [START_REF] Lantreibecq | Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit Using CADP[END_REF]: "although modeling the DTD [Dynamic Task Dispatcher] in LOTOS is theoretically possible, using LNT made the development of a formal model practically feasible". This reinforces our conviction that LNT is the right kind of approach for transferring concurrency theory results to industry.

Further Work

We believe that long standing issues with sequential composition in valuepassing process calculi are satisfactorily solved by the approach proposed in the present article, which also brings a new vision of how modern process calculi should be defined. From a language-design point of view, this approach could be expanded and refined into three directions:

• Data-flow constraints in the static semantics constraints of LNT could be enhanced, e.g., with abstract interpretation techniques, to accept more specifications (see Sec. 4.4) and also provide users with accurate warnings about questionable code fragments.

• One could try relaxing some constraints currently in the dynamic semantics of LNT, such as the prohibition of non-tail recursion (see Sec. 4.6) and of shared variables in parallel branches (see Sec. 4.5).

• Finally, LNT could be extended with quantitative aspects (time, probabilities, distributions, etc.); much has been done in Chi [START_REF] Bos | Redesign of a Systems Engineering Language: Formalisation of χ[END_REF][START_REF] Schiffelers | Formal Semantics of Hybrid Chi[END_REF][START_REF] Van Beek | Syntax and Consistent Equation Semantics of Hybrid Chi[END_REF] and MoDeST [START_REF] D'argenio | MoDeST -A Modelling and Description Language for Stochastic Timed Systems[END_REF][START_REF] Bohnenkamp | MoD-eST: A Compositional Modeling Formalism for Real-Time and Stochastic Systems[END_REF][START_REF] Hahn | A Compositional Modelling and Analysis Framework for Stochastic Hybrid Systems[END_REF], the latter having already symmetric sequential composition, bracketed n-ary operators, and write-many variables, but still with residual action prefix and syntactic constraints associated to probabilistic choice.

From a language-implementation perspective, verification techniques based on state-space exploration (namely, model checking and equivalence checking) are crucial topics, as no other technique today seems better capable of analyzing complex specifications of concurrent systems. It would therefore be worth designing a direct compiling scheme for LNT in order to replace the existing multi-step translation chain (LNT → LOTOS → interpreted Petri nets → labelled transition systems).

Keeping in mind that process calculi have originally been designed for proving concurrent systems formally [START_REF] Milner | A Calculus of Communicating Systems[END_REF], and putting aside the fact that state-space exploration techniques nowadays predominate over proof techniques for the verification of industrial systems, one may wonder whether the proposed approach to sequential composition is still compatible with the needs of formal proofs. Indeed, a large body of knowledge has been developed for value-passing calculi as ATVA'13, CBSE'14, EICS'14, EICS'15, FMICS'13, FMICS'14, FORTE'13, FORTE'14, ICEFM'14, IFM'13, ISSE'13, PDP'15, SAC'14, SCICO'13, SCICO'14, TACAS'13, TACAS'15, VMCAI '15, etc. with action prefix (e.g., [107, 108] [109, 110] [111] in the case of CCS) and one may wonder whether the same would be possible for LNT. We conjecture that the answer to this question is positive, for at least two reasons: (i) When languages with symmetric sequential composition and "write-many" variables can be translated to process calculi with action prefix (which is the case for LNT and CHP [START_REF] Garavel | On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP[END_REF], both of which translate to LOTOS), one can reuse conventional proof techniques by applying them to the translated specifications; (ii) Prior work exists that gives algebraic semantics to forerunner languages sharing similar traits with LNT: in this respect, one can get inspiration from the algebraic laws for OCCAM [START_REF] Roscoe | The Laws of Occam Programming[END_REF][START_REF] Hoare | The Transputer and Occam: A Personal Story[END_REF] and from the ACP G theory [START_REF] Groote | Process Algebra with Guards: Combining Hoare Logic with Process Algebra (Extended Abstract)[END_REF][START_REF] Groote | Process Algebra with Guards: Combining Hoare Logic with Process Algebra[END_REF][START_REF] Ponse | Process Algebra and Dynamic Logic[END_REF], the latter providing a sound and complete axiom system combining Hoare logic and process algebra. Anyway, formal specifications being a prerequisite for proofs, it is likely that proof techniques will adapt to match the style of specifications produced by system designers. Moreover, making process calculi closer to programming languages will enable reusing, for sequential processes at least, state-of-the-art verification approaches based on theorem proving and abstract interpretation.

  [START_REF] Brookes | A Theory of Communicating Sequential Processes[END_REF] ; a 4 ; B)" vs. "a 1 ; a 2 ; τ ; a 3 ; a 4 ; B".

	This problem was acknowledged in [38, Sec. 3.4 and 6.5], which proposed
	a syntactic (yet not semantic) unification of both operators into a single
	construct noted "seq ...endseq"; an assessment of this proposal can be
	found in [39, Sec. 12 and 13].
	3. Control-flow sharing is supported by the enable operator, but quite heavy
	in practice, e.g., "((a 1 ; exit)[](a 2 ; exit)) >> B 3 ", where "[]" is the non-
	deterministic choice operator (noted "+" in CCS).
	4. Data-flow sharing is not possible in CSP, as the values of variables do not
	pass left-to-right over sequential composition [5, p. 132-133]. In LOTOS,
	values can pass over sequential composition, e.g.:
	g?x:t ; exit(x) >> accept x :t in B(x )
	making data-flow sharing feasible, yet cumbersome, e.g.:
	(g 1 ?x 1 :t ; exit(x 1 ) [] g 2 ?x 2 :t ; exit(x 2 )) >> accept x 3 :t in B 3 (x 3 )

  constant noted "ε" that is the neutral element for sequential composition. SOS rules for ACP ε can be found in, e.g.,[START_REF] Groote | Structural Operational Semantics and Bisimulation as a Congruence (Extended Abstract)[END_REF] Tab. 1] and[START_REF] Bloom | Precongruence Formats for Decorated Trace Preorders[END_REF] Tab. 1] as examples of general rule formats; slightly different rules are given in[START_REF] Baeten | Process Algebra[END_REF] Tab. 11] and discussed in[START_REF] D'argenio | A General Conservative Extension Theorem in Process Algebras with Inequalities[END_REF] Sec. 6.1]. Value-passing issues for ACP ε are not addressed in the aforementioned references. It seems that ACP ε was never implemented, and its "ε" operator is absent from the value-passing extensions of ACP (namely PSF, µCRL, and mCRL2).• ACP G (Algebra of Communicating Processes with Guards)[START_REF] Groote | Process Algebra with Guards: Combining Hoare Logic with Process Algebra (Extended Abstract)[END_REF][START_REF] Groote | Process Algebra with Guards: Combining Hoare Logic with Process Algebra[END_REF][START_REF] Ponse | Process Algebra and Dynamic Logic[END_REF] is a process calculus based on ACP ε ; it assumes the existence of global variables, the values of which can be consulted using guards (e.g., Boolean conditions) and modified using nondeterministic state transformers (e.g., assignments). The semantics of ACP

Sec. 7.2]. ACP ε extends ACP with a new "empty process" G is carefully defined, both algebraically and operationally, but in a context of open terms (i.e., with free variables only), so that issues related to uninitialized variables (see Sec. 4.4 below) do not show up. Although the work on ACP G was somewhat eclipsed by the research on µCRL by the same authors and had no immediate continuation (excepted perhaps

Directed Acyclic Graph.

The " √ " gate was noted "δ" in the official definition of LOTOS[START_REF] Iso/Iec | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], but we adopt here the CSP notation to avoid any confusion with ACP, where "δ" means inaction.

"Entities must not be multiplied beyond necessity".

The semicolon in LNT is a statement separator rather than a statement terminator.

Namely, the so-called off-side rule.

Such a pair is often called a configuration in the literature.

Systematic conversion from the former to the latter approach is studied in[START_REF] Gebler | Algebraic Meta-Theory of Processes with Data[END_REF].

These case studies are too many to be exhaustively cited here; please refer to the CADP web site (http://cadp.inria.fr) or search for LNT-related publications in venues such

Acknowledgements

This work benefited from scientific exchanges spanning over the last twenty years. Acknowledgements are due to the members of the ISO E-LOTOS committee (with particular thanks to Mihaela Sighireanu), to all colleagues at INRIA Grenoble who contributed to the design and implementation of LNT (especially Wendelin Serwe, who designed the translation algorithms for the control part and Frédéric Lang, who designed the translation algorithms for the data part and formalized the semantics of LNT), and to the users of LNT for their feedback (with a special mention to Bull and STMicroelectronics for their financial support). Comments from the anonymous reviewers, exchanges with Jan Friso Groote and Sjouke Mauw on ACP G and PSF, and discussions during the IFIP meeting on Open Problems in Concurrency Theory (Bertinoro, June 2014) and the SENSATION European project meeting (Aachen, September 2014) have been helpful in improving the present article.