Advertisement

Congruence from the operator’s point of view

Syntactic requirements on modal characterizations
  • Maciej Gazda
  • Wan FokkinkEmail author
  • Vittorio Massaro
Open Access
Original Article
  • 61 Downloads

Abstract

A basic sanity property of a process semantics is that it constitutes a congruence with respect to standard process operators. This issue has been traditionally addressed by developing, for a specific process semantics, a syntactic format for operational semantics specifications. We suggest a novel, orthogonal approach, which focuses on a specific process operator and determines a class of congruence relations for this operator. To this end, we impose syntactic restrictions on Hennessy–Milner logic, so that a process semantics whose modal characterization satisfies those criteria is guaranteed to be a congruence with respect to the operator in question. We investigate alternative composition, action prefix, projection, encapsulation, renaming, and parallel composition with communication, in the context of both concrete and weak process semantics.

1 Introduction

Congruence of process operators with respect to a process semantics is a fundamental issue in process algebra. In particular, it is an essential property for the existence of a sound and complete axiomatization. There is a large body of research on proving the congruence property. A widely used approach in the realm of structural operational semantics is to define syntactic restrictions on transition rules of process operators. If a process operator is defined by transition rules that comply with such a rule format, then the process semantics in question is guaranteed to be a congruence with respect to this operator. Examples include the panth format for bisimulation semantics [18] and formats designed specifically for several decorated trace semantics [7]. Such rule formats are usually defined with one particular process semantics in mind.

Interestingly, in [7] the modal characterization of a process semantics is taken as starting point to derive the syntactic constraints of the congruence format for this semantics. A modal characterization of a (concrete) process semantics is a sublanguage of Hennessy–Milner logic [14] such that two processes are semantically equivalent if and only if they satisfy exactly the same formulas in this modal characterization. For most process semantics in van Glabbeek’s concrete [17] as well as weak [16] spectrum, a corresponding modal characterization has been defined. Weak semantics, which take into account a special internal action \(\tau \), may require an extension of Hennessy–Milner logic.

We consider the congruence issue from an operator’s point of view. For a number of standard process operators, we determine sufficient requirements on process semantics to guarantee that the semantics are a congruence with respect to these operators. To be more precise, given a process operator, we develop syntactic constraints on modal characterizations, including some semantic parts concerning logical equivalence to relax these constraints. If the modal characterization of a process semantics satisfies these constraints, then the semantics is guaranteed to be compositional with respect to this process operator. So instead of going from a process semantics to a class of transition system specifications for which that semantics is a congruence, we go from the transition rules of a process operator to a class of process semantics for which this operator is compositional. This approach offers an orthogonal view on compositionality. It yields a convenient way to prove the congruence property for a given process algebra and (multiple) process semantics. It moreover provides further insight into connections between process algebra and modal logic.

In an earlier version of this paper [12] the method was applied to derive congruence formats for a range of basic operators: action prefix, alternative composition, and two restriction operators, and parallel composition (without communication), for concrete semantics. Here the work is extended to deal with weak semantics, and covers some additional operators: parallel composition with communication, renaming, and abstraction. For each of the operators we formulate specific requirements on an extension of Hennessy–Milner logic for weak semantics, and show that modal characterizations of existing semantics satisfy these requirements. They apply to concrete semantics as well, by ignoring requirements that concern the internal action \(\tau \).

It is with great pleasure that we make this contribution to the Festschrift for Rob van Glabbeek to celebrate his 60th birthday. His groundbreaking research in concurrency theory is pivotal for our paper. He developed the linear time—branching time spectrum and discovered the strong connection between modal characterizations of process semantics and congruence properties of operators. In general, his writings (not only confined to computer science) broaden the reader’s perspective. Moreover, he is a wonderful colleague and friend, owing to his sharp mind, colorful character, always cheerful mood, and taste for adventure.

2 Preliminaries

A labelled transition system (LTS) consists of a set S of states p (also called processes), a set \({ Act}\) of actions a, a special action \(\tau \), and a set of transitions \(p {\mathop {\longrightarrow }\limits ^{\alpha }} p'\), where \(\alpha \) ranges over \({ Act}\cup \{\tau \}\). A process semantics is an equivalence relation on states in LTSs. Such a semantics is called concrete if it disregards the action \(\tau \), and weak otherwise.

Hennessy–Milner logic [14] is a modal logic for specifying properties of states in an LTS. There exist different equally expressive versions [6, 14, 17]. Here we choose the version, denoted by \({ HML}_\tau \), that consists of the conjunction, negation, and diamond operators, extended with the so-called weak diamond operator that concerns a sequence of transitions carrying the internal action \(\tau \):
$$\begin{aligned} \varphi ~~{:}{:}=~~ \bigwedge _{i\in I}\varphi _i ~\mid ~ \lnot \varphi ~\mid ~ \langle \alpha \rangle \varphi ~\mid ~ \langle \epsilon \rangle \varphi \end{aligned}$$
where I is any index set and \(\alpha \) ranges over \({ Act}\cup \{\tau \}\). If I consists of two elements \(i_1\) and \(i_2\), \(\varphi _{i_1}{\wedge }\,\varphi _{i_2}\) denotes \(\bigwedge _{i\in I}\varphi _i\) and \(\varphi _{i_1}{\vee }\,\varphi _{i_2}\) denotes \(\lnot (\bigwedge _{i\in I}\!\lnot \varphi _i)\). Let \(\textsf {T}\) and \(\textsf {F}\) abbreviate \(\bigwedge _{i\in \emptyset }\varphi _i\) and \(\lnot \textsf {T}\), respectively. We use \(\varphi \langle \alpha \rangle \varphi '\) to denote \(\varphi \wedge \langle \alpha \rangle \varphi '\). Formulas are considered modulo associativity, commutativity and idempotence of conjunction.

\(p\models \varphi \) denotes that process p satisfies formula \(\varphi \). Conjunction and negation have the usual meaning. We have \(p\models \langle \alpha \rangle \varphi \) if there is a transition \(p{\mathop {\longrightarrow }\limits ^{\alpha }}p'\) where \(p'\models \varphi \). Moreover, \(p\models \langle \epsilon \rangle \varphi \) if there is a sequence of (zero or more) transitions \(p{\mathop {\longrightarrow }\limits ^{\tau }}\cdots {\mathop {\longrightarrow }\limits ^{\tau }}p'\) where \(p'\models \varphi \). We write \(\varphi \equiv \varphi '\) if \(p\models \varphi \Leftrightarrow p\models \varphi '\) for all processes p (in all LTSs).

A context C[] is an \({ HML}_\tau \) formula with one occurrence of []. More generally, a multicontext\(C[]_{i \in I}\) is an \({ HML}_\tau \) formula containing one or more [] symbols, indexed by the elements from set I. The formula \(C[\varphi _i]_{i \in I}\) is obtained by replacing the \([]_i\) symbols with formulas \(\varphi _i\).

Each sublanguage \({{\mathcal {O}}}\) of \({ HML}_\tau \) gives rise to an equivalence over processes \(\sim _{{{\mathcal {O}}}}\) by identifying those processes that satisfy exactly the same formulas in \({{\mathcal {O}}}\):
$$\begin{aligned} p \sim _{{{\mathcal {O}}}}q ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ \forall \varphi \in {{\mathcal {O}}}: (p \models \varphi ~\Longleftrightarrow ~ q \models \varphi ). \end{aligned}$$
\({{\mathcal {O}}}\) is called a modal characterization of \(\sim _{{\mathcal {O}}}\). Let \({\overline{{{\mathcal {O}}}}}\) denote the largest subset of \({ HML}_\tau \) for which \(\sim _{{\overline{{{\mathcal {O}}}}}}\) coincides with \(\sim _{{{\mathcal {O}}}}\). Clearly, \({{\mathcal {O}}}\subseteq {\overline{{{\mathcal {O}}}}}\). We note that \({\overline{{{\mathcal {O}}}}}\) may contain formulas that have no logically equivalent counterpart in \({{\mathcal {O}}}\).
Below, modal characterizations of standard process semantics from the literature are given. Formulas \(\varphi '\) and \(\varphi _i\) at the right-hand side of a BNF grammar range over the modal characterization under consideration, while formulas \(\psi \) and \(\psi _i\) range over some other class of formulas. We start with concrete semantics from the spectrum in [17].
  • trace observations\({{\mathcal {O}}}_{T}\)\(\varphi {:}{:}= \langle a\rangle \varphi ' \,|\, \textsf {T}\)

  • completed trace observations\({{\mathcal {O}}}_{CT}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \textsf {T}\,|\, \bigwedge _{a \in { Act}} \lnot \langle a\rangle \textsf {T}\)

  • failure observations\({{\mathcal {O}}}_{F}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \langle a_i\rangle \textsf {T}\)

  • readiness observations\({{\mathcal {O}}}_{R}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \langle a_i\rangle \textsf {T}\wedge \bigwedge _{j \in J} \langle b_j\rangle \textsf {T}\)

  • failure trace observations\({{\mathcal {O}}}_{FT}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \langle a_i\rangle \textsf {T}\wedge \varphi ' \,|\, \textsf {T}\)

  • ready trace observations\({{\mathcal {O}}}_{RT}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \langle a_i\rangle \textsf {T}\wedge \bigwedge _{j \in J} \langle b_j\rangle \textsf {T}\wedge \varphi \,|\, \textsf {T}\)

  • impossible futures\({{\mathcal {O}}}_{I\!F}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \psi _i \ (\psi _i \in {{\mathcal {O}}}_{T})\)

  • possible futures\({{\mathcal {O}}}_{P\!F}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \lnot \psi _i \wedge \bigwedge _{j \in J} \psi _j \ (\psi _i, \psi _j \in {{\mathcal {O}}}_{T})\)

  • simulation observations\({{\mathcal {O}}}_{1S}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \varphi _{i}\)

  • n-nested simulation observations\({{\mathcal {O}}}_{nS}\)\((n \ge 2)\): \(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \psi ~~(\psi \in {{\mathcal {O}}}_{(n-1)S})\)

  • ready simulation observations\({{\mathcal {O}}}_{RS}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \lnot \langle a\rangle \textsf {T}\,|\, \bigwedge _{i \in I} \varphi _{i}\)

  • bisimulation observations\({{\mathcal {O}}}_{B}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

We continue with modal characterizations for some weak semantics from the spectrum in [16].
  • weak trace observations\({{\mathcal {O}}}_{ WT}\)\(\varphi {:}{:}= \langle \epsilon \rangle \langle a\rangle \varphi ' \,|\, \textsf {T}\)

  • weak completed trace observations\({{\mathcal {O}}}_{WCT}\): \(\varphi {:}{:}= \langle \epsilon \rangle \langle a\rangle \langle \epsilon \rangle \varphi '\,|\, \textsf {T}\,|\, \langle \epsilon \rangle \bigwedge _{a \in { Act}} \lnot \langle \epsilon \rangle \langle a\rangle \textsf {T}\)

  • weak failure observations\({{\mathcal {O}}}_{ WF}\)\(\varphi {:}{:}= \langle \epsilon \rangle \langle a\rangle \varphi ' \,|\, \langle \epsilon \rangle \bigwedge _{i \in I} \lnot \langle \epsilon \rangle \langle a_i\rangle \textsf {T}\)

  • weak bisimulation observations\({{\mathcal {O}}}_{ WB}\)\(\varphi {:}{:}= \langle \epsilon \rangle \varphi ' \,|\, \langle \epsilon \rangle \langle a\rangle \langle \epsilon \rangle \varphi '\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • rooted weak bisimulation observations\({{\mathcal {O}}}_{RWB}\): \(\varphi {:}{:}= \langle \epsilon \rangle \langle \alpha \rangle \langle \epsilon \rangle \psi ~(\psi \in {{\mathcal {O}}}_{ WB})\,|\, \psi ~(\psi \in {{\mathcal {O}}}_{ WB})\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • delay bisimulation observations\({{\mathcal {O}}}_{ DB}\)\(\varphi {:}{:}= \langle \epsilon \rangle \varphi ' \,|\, \langle \epsilon \rangle \langle a\rangle \varphi '\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • rooted delay bisimulation observations\({{\mathcal {O}}}_{RDB}\): \(\varphi {:}{:}= \langle \epsilon \rangle \langle \alpha \rangle \psi ~(\psi \in {{\mathcal {O}}}_{ DB})\,|\, \psi ~(\psi \in {{\mathcal {O}}}_{ DB})\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • \(\eta \)-bisimulation observations\({{\mathcal {O}}}_{\eta B}\)\(\varphi {:}{:}= \langle \epsilon \rangle \varphi ' \,|\, \langle \epsilon \rangle \varphi '\langle a\rangle \langle \epsilon \rangle \varphi ''\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • rooted\(\eta \)-bisimulation observations\({{\mathcal {O}}}_{R \eta B}\): \(\varphi {:}{:}= \langle \alpha \rangle \langle \epsilon \rangle \psi ~(\psi \in {{\mathcal {O}}}_{\eta B})\,|\, \psi ~(\psi \in {{\mathcal {O}}}_{\eta B})\,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • branching bisimulation observations\({{\mathcal {O}}}_{BB}\): \(\varphi {:}{:}= \langle \epsilon \rangle \varphi '\langle a\rangle \varphi '' \,|\, \langle \epsilon \rangle \varphi '\wedge (\varphi ''\vee \langle \tau \rangle \varphi '') \,|\,\bigwedge _{i \in I} \varphi _{i}\,|\,\lnot \varphi '\)

  • rooted branching bisimulation observations\({{\mathcal {O}}}_{RBB}\): \(\varphi {:}{:}= \langle \alpha \rangle \psi ~(\psi \in {{\mathcal {O}}}_{BB}) \,|\, \psi ~(\psi \in {{\mathcal {O}}}_{BB}) \,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

A process algebra [8] is built from process operators with a certain arity and a set of variables. Each variable is considered an (open) process term. Moreover, if a process operator \(\bigtriangleup \) has arity n and \(t_1,\dots ,t_n\) are process terms, then also \(\bigtriangleup (t_1,\ldots ,t_n)\) is a process term. A process term is called closed if it does not contain variables. A structural operational semantics [1] associates an LTS to a given process algebra, in which the states are the closed process terms and the transitions are generated by what are called transition rules. A transition rule is of the formwhere the \(t_i\), u, and v are (open) process terms and I is some index set. Intuitively it states that if, for some substitution \(\sigma \) mapping variables to closed process terms, the transitions \(\sigma (t_i){\mathop {\longrightarrow }\limits ^{\alpha _i}}\sigma (t_i')\) are present in the LTS for all \(i\in I\), then the transition \(\sigma (u){\mathop {\longrightarrow }\limits ^{\beta }}\sigma (v)\) is also present in the LTS.
Given a process semantics \(\sim \), we say that \(\sim \) is a congruence with respect to process operator \(\bigtriangleup \) if, for all processes \(p_1,\ldots ,p_n,q_1,\ldots ,q_n\),
$$\begin{aligned} p_1 \sim q_1\,\wedge \,\cdots \,\wedge \,p_n \sim q_n ~\implies ~ \bigtriangleup \!(p_1, \dots , p_{n}) \sim \bigtriangleup (q_1, \dots , q_{n}) \end{aligned}$$

3 Congruence requirements

In this section, we investigate several common process operators. For each of these operators we provide syntactic requirements on modal characterizations of process semantics that guarantee the congruence property for this operator with regard to such process semantics.

3.1 Alternative composition

We begin with alternative composition \(x+y\), which expresses a nondeterministic choice between two processes. It is defined by the following transition rules:In order to state congruence requirements for this operator, we need to work with a restricted variant of a context. A root-level context is a multicontext without occurrences of modalities \(\langle \alpha \rangle \), for all \(\alpha \in Act \cup \{\tau \}\). Intuitively, a root-level context describes a property that only concerns the root state of a process (before any transition occurs). In what follows, we distinguish root-level contexts by adding a “0” subscript to a context’s name, e.g. \(C_0[]\). Given an \({ HML}_\tau \) formula \(\varphi \), its root-level subformulas are all subformulas \(\psi \) of \(\varphi \) that are not in the scope of a diamond operator \(\langle \alpha \rangle \).

In the case of alternative composition, the residual behaviour of the process \(p+q\) after performing a transition is completely determined by the behaviour of one of the components p or q. This is expressed formally in the following lemmas:

Lemma 1

\(p + q \models \langle \alpha \rangle \varphi ~~\Longleftrightarrow ~~ (p \models \langle \alpha \rangle \varphi ~\vee ~ q \models \langle \alpha \rangle \varphi )\).

Lemma 2

\(p + q \models \langle \epsilon \rangle \langle \alpha \rangle \varphi ~~\Longleftrightarrow ~~ (p \models \langle \epsilon \rangle \langle \alpha \rangle \varphi ~\vee ~ q \models \langle \epsilon \rangle \langle \alpha \rangle \varphi )\).

We shall moreover use the following straightforward fact.

Lemma 3

\(p \models \langle \epsilon \rangle \varphi ~~\Longleftrightarrow ~~ (p \models \varphi ~\vee ~ p \models \langle \tau \rangle \langle \epsilon \rangle \varphi )\).

For concrete semantics, Lemma 1 allows one to show a straightforward requirement guaranteeing the congruence property: the language in question needs to be closed on subconjunctions occurring at the root level, that is:
$$\begin{aligned} C_0\left[ \bigwedge _{i \in I} \varphi _i\right] \in {{\mathcal {O}}}~\implies ~ \forall i \in I: \varphi _i \in {{\mathcal {O}}}. \end{aligned}$$
Semantics that fail to satisfy the above property may not be a congruence with respect to alternative composition. For example, \({{\mathcal {O}}}= \{\langle a\rangle \textsf {T}\wedge \langle b\rangle \textsf {T}\}\) violates this property because the conjuncts \(\langle a\rangle \textsf {T}\) and \(\langle b\rangle \textsf {T}\) are not in \({{\mathcal {O}}}\). We have (using CCS notation): \(a.\mathbf{0} \sim _{{\mathcal {O}}}\mathbf{0}\), but \(a.\mathbf{0}+b.\mathbf{0} \not \sim _{{\mathcal {O}}}\mathbf{0}+b.\mathbf{0}\), because \(a.\mathbf{0}+b.\mathbf{0}\models \langle a\rangle \textsf {T}\wedge \langle b\rangle \textsf {T}\) while \(\mathbf{0}+b.\mathbf{0}\) does not satisfy this formula. Here \(a.\_\) and \(b.\_\) denote action prefix (see Sect. 3.2) and \(\mathbf{0}\) is a constant that displays no behaviour.

The above requirement is insufficient for weak semantics. To see this, consider \({{\mathcal {O}}}= \{ \langle \epsilon \rangle \lnot \langle b\rangle \textsf {T}\}\), which clearly satisfies this property. We have \( \tau .a.\mathbf{0} \sim _{{\mathcal {O}}}a.\mathbf{0}\), but \(\tau .a.\mathbf{0} +b.\mathbf{0} \not \sim _{{\mathcal {O}}}a.\mathbf{0} + b.\mathbf{0}\), because \(\tau .a.\mathbf{0}+b.\mathbf{0}\models \langle \epsilon \rangle \lnot \langle b\rangle \textsf {T}\) while \(a.\mathbf{0}+b.\mathbf{0}\) does not satisfy this formula. Therefore an extra requirement is needed for the weak diamond operator \(\langle \epsilon \rangle \).

The following theorem gives sufficient requirements for a modal characterization to induce a congruence with respect to alternative composition. Note that the requirements below involve root-level contexts only—this stronger restriction of root-level behaviour is also present in process semantics from the literature, in the form of rooted versions of weak bisimulation semantics. For concrete semantics only the first requirement is relevant, as their modal characterizations do not contain the \(\langle \epsilon \rangle \varphi \) construct. Note moreover that (alt-1) is entirely syntactic (i.e., \(\varphi _i \in {{\mathcal {O}}}\)), while (alt-2) is partly syntactic (\(\varphi \in {{\mathcal {O}}}\)) and partly semantic (\(\varphi \in {\overline{{{\mathcal {O}}}}}\) and \(\varphi \equiv \langle \alpha \rangle \varphi '\)). The advantage of using these semantics parts instead of their syntactic counterparts is that it yields a more relaxed requirement. The syntactic parts are used for the structural induction hypothesis (IH) in the proof of Theorem 1.

Theorem 1

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfy the following two requirements, for all root-level contexts \(C_0[]\) and formulas \(\varphi _i,\varphi \):

\(\textsc {(alt{-}1) } \,~~~C_0[\bigwedge _{i \in I} \varphi _i] \in {{\mathcal {O}}}~\implies ~ \forall i \in I: \varphi _i \in {{\mathcal {O}}}\)

\(\textsc {(alt{-}2) } \,~~~C_0[\langle \epsilon \rangle \varphi ] \in {{\mathcal {O}}}~\implies ~ (\varphi \in {{\mathcal {O}}}\,\wedge \,\langle \tau \rangle \langle \epsilon \rangle \varphi \in {\overline{{{\mathcal {O}}}}}) ~\vee ~ \exists \alpha .\,\exists \varphi ':\varphi \equiv \langle \alpha \rangle \varphi '\)

Then \(\sim _{{{\mathcal {O}}}}\) is a congruence with respect to the alternative composition operator.

Proof

Suppose that the language \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfies \(\textsc {(alt{-}1)}\) and \(\textsc {(alt{-}2)}\). Suppose further that \(p \sim _{{\mathcal {O}}}p'\) and \(q \sim _{{\mathcal {O}}}q'\). We need to show that \(p + q \sim _{{\mathcal {O}}}p' + q'\), that is, for all \(\varphi \in {{\mathcal {O}}}\) we have \(p + q \models \varphi \Longleftrightarrow p' + q' \models \varphi \). The proof proceeds with structural induction on \(\varphi \). The base case, \(\varphi = \textsf {T}\), is covered by the first inductive case, taking \(I=\emptyset \). Where appropriate, facts that are used in a derivation step are denoted at the right-hand side of the \(\Longleftrightarrow \) sign.
  • \(\varphi = \bigwedge _{i \in I} \varphi _i\):

    \(p + q \models \bigwedge _{i \in I} \varphi _i ~~\Longleftrightarrow \)

    \(\forall {i \in I}: \, p + q \models \varphi _i ~~\Longleftrightarrow \) ((alt-1) + IH)

    \(\forall {i \in I}: \, p' + q' \models \varphi _i ~~\Longleftrightarrow \)

    \(p' + q' \models \bigwedge _{i \in I} \varphi _i\)

  • \(\varphi = \langle \alpha \rangle \psi \):

    \(p + q \models \langle \alpha \rangle \psi ~~\Longleftrightarrow \) (Lemma 1)

    \(p \models \langle \alpha \rangle \psi ~\vee ~ q \models \langle \alpha \rangle \psi ~~\Longleftrightarrow \) (\(p \sim _{{\mathcal {O}}}p' \wedge q\sim _{{\mathcal {O}}}q'\))

    \(p' \models \langle \alpha \rangle \psi ~\vee ~ q' \models \langle \alpha \rangle \psi ~~\Longleftrightarrow \) (Lemma 1)

    \(p' + q' \models \langle \alpha \rangle \psi \)

  • \(\varphi = \langle \epsilon \rangle \psi :\) We consider two subcases:
    • \(\psi \equiv \langle \alpha \rangle \psi '\) for some \(\alpha \) and \(\psi '\): \(p+q \models \langle \epsilon \rangle \langle \alpha \rangle \psi ' ~~\Longleftrightarrow \) (Lemma 2)

      \(p \models \langle \epsilon \rangle \langle \alpha \rangle \psi ' ~\vee ~ q \models \langle \epsilon \rangle \langle \alpha \rangle \psi ' ~~\Longleftrightarrow ~ (p \sim _{{\overline{{{\mathcal {O}}}}}} p' \wedge q \sim _{{\overline{{{\mathcal {O}}}}}} q')\)

      \(p' \models \langle \epsilon \rangle \langle \alpha \rangle \psi ' ~\vee ~ q' \models \langle \epsilon \rangle \langle \alpha \rangle \psi ' ~~\Longleftrightarrow \) (Lemma 2)

      \(p'+q' \models \langle \epsilon \rangle \langle \alpha \rangle \psi '\)

    • \(\psi \not \equiv \langle \alpha \rangle \psi '\) for all \(\alpha \) and \(\psi '\), so by (alt-2), \(\psi \in {{\mathcal {O}}}\) and \(\langle \tau \rangle \langle \epsilon \rangle \psi \in {\overline{{{\mathcal {O}}}}}\): \(p+q \models \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (Lemma 3)

      \(p+q \models \psi ~\vee ~ p+q \models \langle \tau \rangle \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (\(\psi \in {{\mathcal {O}}}\) + IH,  Lemma 1)

      \(p'+q' \models \psi \,\vee \, p \models \langle \tau \rangle \langle \epsilon \rangle \psi \,\vee \, q \models \langle \tau \rangle \langle \epsilon \rangle \psi \)  \(\Longleftrightarrow \) (\(\langle \tau \rangle \langle \epsilon \rangle \psi \in {\overline{{{\mathcal {O}}}}}\) + \(p \sim _{{\overline{{{\mathcal {O}}}}}} p' \wedge \,q \sim _{{\overline{{{\mathcal {O}}}}}} q'\))

      \(p'+q' \models \psi ~\vee ~ p' \models \langle \tau \rangle \langle \epsilon \rangle \psi ~ \vee ~ q' \models \langle \tau \rangle \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (Lemma 1)

      \(p'+q' \models \psi ~\vee ~ p'+q' \models \langle \tau \rangle \langle \epsilon \rangle \psi ~~ \Longleftrightarrow \) (Lemma 3)

      \(p'+q' \models \langle \epsilon \rangle \psi \)

      In the first application of (alt-2), we use that \(\psi \not \equiv \langle \alpha \rangle \psi '\) implies \(\psi \in {{\mathcal {O}}}\). In the second application of (alt-2), we use that \(\psi \not \equiv \langle \alpha \rangle \psi '\) implies \(\langle \tau \rangle \langle \epsilon \rangle \psi \in {\overline{{{\mathcal {O}}}}}\).

  • \(\varphi = \lnot \psi \):

    Let \(\psi '\) be the outermost subformula of \(\psi \) that does not have \(\lnot \) at its root, that is, \(\psi = (\lnot )^{n} \psi '\). Clearly, \(\varphi \) is logically equivalent to either \(\psi '\) or \(\lnot \psi '\). The case \(\varphi \equiv \psi '\) was covered by the three inductive cases above, with regard to \(\psi '\) instead of \(\varphi \). Here it is important to observe that \((\lnot )^{n}[]\) is a root-level context, which implies that requirements (alt-1) and (alt-2) apply to \(\psi '\) as well. Finally, if \(\varphi \equiv \lnot \psi '\), then it suffices to observe that \(p+q\models \psi '~\Longleftrightarrow ~p'+q'\models \psi '\) yields \(p+q\models \lnot \psi '\Longleftrightarrow p'+q'\models \lnot \psi '\). So this case basically coincides with the case \(\varphi \equiv \psi '\). \(\square \)

To satisfy (alt-1), \({{\mathcal {O}}}_{ CT}\) needs to be syntactically enriched (outside the BNF grammar) with formulas \(\lnot \langle a\rangle \textsf {T}\). This enrichment clearly does not change the distinguishing power of the modal characterization. With this enrichment, the modal characterizations of the concrete semantics in Sect. 2 all satisfy (alt-1). Therefore Theorem 1 yields:

Corollary 1

\(\sim _{ T}\), \(\sim _{ CT}\), \(\sim _{ F}\), \(\sim _{ R}\), \(\sim _{ FT}\), \(\sim _{ RT}\), \(\sim _{ I\!F}\), \(\sim _{ P\!F}\), \(\sim _{ nS}\ (\)for \(n\ge 1)\), \(\sim _{ RS}\), and \(\sim _{ B}\) are congruences for the alternative composition operator.

Likewise, to satisfy (alt-1), the modal characterization \({{\mathcal {O}}}_{ WCT}\) needs to be enriched with formulas \(\lnot \langle \epsilon \rangle \langle a\rangle \textsf {T}\). Again, this enrichment does not change the distinguishing power of the modal characterization. With this enrichment, the modal characterizations of the weak semantics mentioned in the following theorem satisfy (alt-1) and (alt-2).

Corollary 2

\(\sim _{ WT}\), \(\sim _{ WCT}\), \(\sim _{ WF}\), \(\sim _{ RWB}\), \(\sim _{ RDB}\), \(\sim _{ R\eta B}\), and \(\sim _{ RBB}\) are congruences for the alternative composition operator.

The unrooted versions of weak, delay, \(\eta \)-, and branching bisimulation semantics do not constitute congruences for the alternative composition operator. Their modal characterizations indeed violate (alt-2). For example, let \(\varphi =\lnot (\langle \epsilon \rangle \langle a\rangle \langle \epsilon \rangle \textsf {T})\). Then \(\langle \epsilon \rangle \varphi \) is in \({{\mathcal {O}}}_{ WB}\), but \(\langle \tau \rangle \langle \epsilon \rangle \varphi \notin {\overline{{{\mathcal {O}}}}}_{ WB}\) and there do not exist an \(\alpha \) and \(\varphi '\) such that \(\varphi \equiv \langle \alpha \rangle \varphi '\).

3.2 Action prefix

Action prefix is a unary operator which represents execution of a single action followed by the process given as the argument. It is defined by a family of transition rules, with one rule for each \(\alpha \in Act \cup \{\tau \}\):We can arrive at a proper congruence requirement using the following simple lemma that lists all the possible cases when a process of the form \(\alpha .p\) satisfies modalities \(\langle \alpha '\rangle \varphi \) and \(\langle \epsilon \rangle \varphi \).

Lemma 4

For all \(\alpha , \alpha ' \in Act \cup \{ \tau \}\) and \(a \in Act\):
  1. 1.

    \(\alpha . p \models \langle \alpha ' \rangle \varphi ~~\Longleftrightarrow ~~ p \models \varphi ~\wedge ~ \alpha = \alpha '\)

     
  2. 2.

    \(\tau . p \models \langle \epsilon \rangle \varphi ~~\Longleftrightarrow ~~ p \models \langle \epsilon \rangle \varphi ~\vee ~ \tau . p \models \varphi \)

     
  3. 3.

    \(a . p \models \langle \epsilon \rangle \varphi ~~\Longleftrightarrow ~~ a . p \models \varphi \)

     

The following theorem gives sufficient requirements for a modal characterization to induce a congruence with respect to action prefix. Note that (act-1) is syntactic (\(\varphi \in {{\mathcal {O}}}\)), while (act-2) is semantic (\(\langle \epsilon \rangle \varphi \in {\overline{{{\mathcal {O}}}}}\)).

Theorem 2

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfy, for all contexts C[] and formulas \(\varphi \):
(act-1)

\(~~~~~C[\langle \alpha \rangle \varphi ] \in {{\mathcal {O}}}~\implies ~ \varphi \in {{\mathcal {O}}}\)

(act-2)

\(~~~~~C[\langle \epsilon \rangle \varphi ] \in {{\mathcal {O}}}~\implies ~ \langle \epsilon \rangle \varphi \in {\overline{{{\mathcal {O}}}}}\)

Then \(\sim _{{{\mathcal {O}}}}\) is a congruence with respect to the action prefix operator.

Proof

Let \(p \sim _{{\mathcal {O}}}q\). We need to show that for all \(\psi \in {{\mathcal {O}}}\) and \(\alpha \in Act \cup \{\tau \}\), \(\alpha .p \models \psi \Longleftrightarrow \alpha .q \models \psi \). This can be achieved by proving a stronger statement: for all \(\psi \in {{\mathcal {O}}}\), all subformulas\(\varphi \)of\(\psi \), and all \(\alpha \in Act \cup \{\tau \}\), \(\alpha .p \models \varphi \Longleftrightarrow \alpha .q \models \varphi \).

Let \(\varphi \) be a subformula of some \(\psi \in {{\mathcal {O}}}\). Since requirements (act-1) and (act-2) are formulated for general contexts C[], they are guaranteed to hold for \(\varphi \). The proof employs structural induction on \(\varphi \). Clearly, \(\varphi \) is of the form \(C_0[\langle \xi _i\rangle \varphi _i]_{i \in I}\) with \(\xi _i \in Act \cup \{\tau ,\epsilon \}\), where \(C_0[]_{i \in I}\) is a root-level multicontext with the additional property that it does not contain diamond operators. Since \(C[]_{i\in I}\) is built from only conjunction and negation, whether a process satisfies \(\varphi \) is completely determined by the satisfaction of \(\langle \xi _i\rangle \varphi _i\) for \(i \in I\) by this process. In other words, if \(\forall {i \in I}: (r_1 \models \langle \xi _i\rangle \varphi _i \Longleftrightarrow r_2 \models \langle \xi _i\rangle \varphi _i)\), then \(r_1 \models \varphi \Longleftrightarrow r_2\models \varphi \). Thus, in order to prove the main statement, it suffices to show that
$$\begin{aligned} \forall i \in I:\,(\alpha .p \models \langle \xi _i\rangle \varphi _i ~~\Longleftrightarrow ~~ \alpha .q \models \langle \xi _i\rangle \varphi _i). \end{aligned}$$
We consider the following two cases:
  • \(\xi _i = \alpha _i\), with \(\alpha _i \in Act \cup \{\tau \}\):

    \(\alpha .p \models \langle \alpha _i\rangle \varphi _i ~~\Longleftrightarrow \) (case 1 of Lemma 4)

    \(\alpha = \alpha _i ~\wedge ~ p \models \varphi _i ~~\Longleftrightarrow \) ((act-1) + \(p \sim _{{\mathcal {O}}}q\))

    \(\alpha = \alpha _i ~\wedge ~ q\models \varphi _i ~~\Longleftrightarrow \) (case 1 of Lemma 4)

    \(\alpha .q \models \langle \alpha _i\rangle \varphi _i\)

  • \(\xi _i = \epsilon \): There are two subcases to consider.
    • \(\alpha = \tau \):

      \(\tau .p \models \langle \epsilon \rangle \varphi _i ~~\Longleftrightarrow \) (case 2 of Lemma 4)

      \(p \models \langle \epsilon \rangle \varphi _i \,\vee \, \tau .p\models \varphi _i ~~\Longleftrightarrow \) ((act-2) + \(p \sim _{{\overline{{{\mathcal {O}}}}}} q\))

      \(q \models \langle \epsilon \rangle \varphi _i \,\vee \, \tau .p\models \varphi _i ~~\Longleftrightarrow \) (IH)

      \(q \models \langle \epsilon \rangle \varphi _i \,\vee \, \tau .q \models \varphi _i ~~\Longleftrightarrow \) (case 2 of Lemma 4)

      \(\tau .q \models \langle \epsilon \rangle \varphi _i\)

    • \(\alpha = a \in Act\):

      \(a.p \models \langle \epsilon \rangle \varphi _i ~~\Longleftrightarrow \) (case 3 of Lemma 4)

      \(a.p \models \varphi _i ~~\Longleftrightarrow \) (IH)

      \(a.q \models \varphi _i ~~\Longleftrightarrow \) (case 3 of Lemma 4)

      \(a.q \models \langle \epsilon \rangle \varphi _i \)\(\square \)

That requirement (act-1) is essential to guarantee the congruence property for the action prefix operator is shown by the following counterexample. \({{\mathcal {O}}}= \{\langle a\rangle \langle b\rangle \textsf {T}\}\) violates (act-1) because \(\langle b\rangle \textsf {T}\not \in {{\mathcal {O}}}\). We have \(b.\mathbf{0} \sim _{{\mathcal {O}}}\mathbf{0} \), but \(a.b.\mathbf{0} \not \sim _{{\mathcal {O}}}a.\mathbf{0}\), because \(a.b.\mathbf{0} \models \langle a\rangle \langle b\rangle \textsf {T}\) while \(a.\mathbf{0}\) does not satisfy this formula. That requirement (act-2) is essential is shown by the following counterexample. \({{\mathcal {O}}}= \{\langle \epsilon \rangle \langle a\rangle \textsf {T}\wedge \lnot \langle b\rangle \textsf {T},\textsf {T}\}\) satisfies (act-1), but violates (act-2) because \(\langle a\rangle \textsf {T}\not \in {{\mathcal {O}}}\). We have \(a.\mathbf{0}+b.\mathbf{0} \sim _{{\mathcal {O}}}b.\mathbf{0} \), but \(\tau .(a.\mathbf{0}+b.\mathbf{0}) \not \sim _{{\mathcal {O}}}\tau .b.\mathbf{0}\), because \(\tau .(a.\mathbf{0}+b.\mathbf{0}) \models \langle \epsilon \rangle \langle a\rangle \textsf {T}\wedge \lnot \langle b\rangle \textsf {T}\) while \(\tau .b.\mathbf{0}\) does not satisfy this formula.

The modal characterizations of the concrete semantics in Sect. 2 all satisfy (act-1).

Corollary 3

\(\sim _{ T}\), \(\sim _{ CT}\), \(\sim _{ F}\), \(\sim _{ R}\), \(\sim _{ FT}\), \(\sim _{ RT}\), \(\sim _{ I\!F}\), \(\sim _{ P\!F}\), \(\sim _{ nS}\ (\)for \(n\ge 1)\), \(\sim _{ RS}\), and \(\sim _{ B}\) are congruences for the action prefix operator.

The modal characterizations of the weak semantics in Sect. 2 all satisfy (act-1) and (act-2).

Corollary 4

\(\sim _{ WT}\), \(\sim _{ WCT}\), \(\sim _{ WF}\), \(\sim _{ WB}\), \(\sim _{ RWB}\), \(\sim _{ DB}\), \(\sim _{ RDB}\), \(\sim _{ \eta B}\), \(\sim _{ R\eta B}\), \(\sim _{ BB}\) and \(\sim _{ RBB}\) are congruences for the action prefix operator.

3.3 Restriction operators: projection and encapsulation

In this section, we consider operators that can restrict the behaviour of a process. We focus on two such operators: projection and encapsulation.

The nth projection \(\pi _n\), for each \(n\ge 0\), mimics the behaviour of a process up to level n [4]. The family of projection operators is defined by the following transition rules (where a ranges over Act):Note that \(\pi _0(x)\) cannot perform any a-transitions.
The second restriction operator, encapsulation \(\partial _B\), with \(B \subseteq Act\), disables all transitions whose labels are in B. Its defining transition rules are (one for each \(\alpha \in Act \cup \{\tau \}\)):Given any \({ HML}_\tau \) formula, we can deduce which of its subformulas of the form \(\langle a\rangle \varphi \) always yield \(\textsf {F}\) after applying a projection or encapsulation operator. Indeed, for a process \(\pi _n(p)\), any subformula \(\langle a\rangle \varphi \) at level n (i.e., any subformula within the scope of n diamond operators labelled with visible actions) can be replaced by \(\textsf {F}\). In the case of a process \(\partial _B(p)\), any subformula \(\langle b\rangle \varphi \) with \(b \in B\) can be replaced by \(\textsf {F}\).

We shall now define the special property of the class of unary restriction operators such as \(\pi _n\) or \(\partial _B\) that allows us to immediately deduce the satisfaction status of certain subformulas after applying such an operator. That is, we consider unary restriction operators f such that for each formula \(\varphi \in { HML}_\tau \) there is a corresponding formula \({ cut}_{f}(\varphi )\) in which each subformula \(\langle \alpha \rangle \varphi '\) of \(\varphi \) that is known in advance not to be satisfied when evaluating \(\varphi \) for any process f(p), is replaced by \(\textsf {F}\). Actually this means that either we can replace a larger subformula by \(\textsf {T}\), or the entire formula becomes \(\textsf {F}\). We can replace the first innermost negation symbol (closest to the introduced \(\textsf {F}\)) and the following subformula by \(\textsf {T}\); if the \(\textsf {F}\) symbol does not appear within the scope of a negation symbol, then the whole formula yields \(\textsf {F}\). Note that this reasoning is valid due to the chosen syntax of \({ HML}_\tau \), which in particular lacks disjunctions and box modalities. If a language \({{\mathcal {O}}}\subseteq { HML}_\tau \) is closed under \({ cut}_f\), then it induces a congruence with respect to f. The whole idea is formalized below.

Lemma 5

Let f be a unary process operator. Suppose there exists a function \({ cut}_{f}: { HML}_\tau \rightarrow { HML}_\tau \) such that for each process p and formula \(\varphi \),
$$\begin{aligned} \textsc {(cut{-}1)} ~~~~~~~~ f(p) \models \varphi ~~\Longleftrightarrow ~~ p \models { cut}_f(\varphi ) \end{aligned}$$
If \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfies \(\varphi \in {{\mathcal {O}}}\implies { cut}_f(\varphi ) \in {\overline{{{\mathcal {O}}}}}\), then \(\sim _{{\mathcal {O}}}\) is a congruence with respect to f.

Proof

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \) and \(p \sim _{{\mathcal {O}}}q\). We have:  \(f(p) \models \varphi ~~\Longleftrightarrow \) (cut-1)   \(p \models { cut}_f(\varphi ) ~~\Longleftrightarrow \) (\(p \sim _{{\mathcal {O}}}q\) and \({ cut}_f(\varphi ) \in {\overline{{{\mathcal {O}}}}}\))   \(q \models { cut}_f(\varphi ) ~~\Longleftrightarrow \) (cut-1)   \(f(q) \models \varphi \). \(\square \)

The next proposition gives an explicit requirement for a modal language to induce a congruence in case the \({ cut}_f\) formulas are obtained from the original ones by turning certain subformulas into \(\textsf {F}\).

Proposition 1

Let f be a unary process operator. Let \({ cut}_{f}: { HML}_\tau \rightarrow { HML}_\tau \) satisfy (cut-1) as well as
$$\begin{aligned} \begin{array}{ll} \textsc {(cut{-}2)}~~~~~~~ &{} \text{ for } \text{ each } \text{ formula } \varphi , { cut}_f(\varphi ) \hbox { is obtained by replacing}\\ &{} \hbox {(zero or more) subformulas of}\ \varphi \ \hbox {by}\ \textsf {F}\end{array} \end{aligned}$$
If \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfies, for each context C[] and formula \(\varphi \),
$$\begin{aligned} \textsc {(res)}~~~~~~~~C[\lnot \varphi ] \in {{\mathcal {O}}}~~\implies ~~ C[\textsf {T}] \in {\overline{{{\mathcal {O}}}}} \end{aligned}$$
then \(\sim _{{\mathcal {O}}}\) is a congruence with respect to f.

Proof

By Lemma 5 it suffices to prove that \({ cut}_f(\varphi ) \in {\overline{{{\mathcal {O}}}}}\) for all \(\varphi \in {{\mathcal {O}}}\). If \({ cut}_f(\varphi ) \equiv \textsf {F}\), then trivially it is in \({\overline{{{\mathcal {O}}}}}\). Consider the case \({ cut}_f(\varphi ) \not \equiv \textsf {F}\). By (cut-2), \({ cut}_f(\varphi ) \equiv C'[\textsf {F}]_{i \in I}\) for some multicontext \(C'[]_{i \in I}\). Since \({ cut}_f(\varphi ) \not \equiv \textsf {F}\), and given that formulas contain only conjunctions, existential diamond operators, and negations, clearly each occurrence of \(\textsf {F}\) in this formula must be within the scope of a negation symbol. Hence \({ cut}_f(\varphi ) \equiv C'[\lnot D_i[\textsf {F}]]_{i \in I}\), where for each \(i\in I\) we can choose the context \(D_i[]\) such that [] is not within the scope of a negation. (That is, we choose the negation symbols for all \(i\in I\) as low as possible in the parse tree of the formula.) Then \(C'[\lnot D_i[\textsf {F}]]_{i \in I} \equiv C'[\lnot \textsf {F}]_{i \in I} \equiv C'[\textsf {T}]_{i \in I}\). Since \({{\mathcal {O}}}\) satisfies (res), \(C'[\textsf {T}]_{i \in I} \in {\overline{{{\mathcal {O}}}}}\). Hence \({ cut}_f(\varphi ) \in {\overline{{{\mathcal {O}}}}}\). \(\square \)

We provided a general congruence framework for restriction operators. We now proceed to define specific \({ cut}_{f}\) functions for projection and encapsulation.

Proposition 2

The functions \({ cut}_n\) and \({ cut}_B\) defined below satisfy (cut-1) and (cut-2).
  1. 1.

    For the projection operators \(\pi _n\), with \(n\ge 0\):

    \({ cut}_n(\bigwedge _{i \in I} \varphi _i)\)\(=\)\(\bigwedge _{i \in I} { cut}_n(\varphi _i)\)

    \({ cut}_n(\lnot \varphi )\)\(=\)\(\lnot { cut}_n(\varphi )\)

    \({ cut}_{n}(\langle \epsilon \rangle \varphi )\)\(=\)\(\langle \epsilon \rangle { cut}_{n}(\varphi )\)

    \({ cut}_0(\langle a\rangle \varphi )\)\(=\)\(\textsf {F}\)

    \({ cut}_{n+1}(\langle a\rangle \varphi )\)\(=\)\(\langle a\rangle {} { cut}_n(\varphi )\)

    \({ cut}_{n}(\langle \tau \rangle \varphi )\)\(=\)\(\langle \tau \rangle { cut}_{n}(\varphi )\)

     
  2. 2.

    For the encapsulation operators \(\partial _B\), with \(B \subseteq { Act}\):

    \({ cut}_B(\bigwedge _{i \in I} \varphi _i)\)\(=\)\(\bigwedge _{i \in I} { cut}_B(\varphi _i)\)

    \({ cut}_B(\lnot \varphi )\)\(=\)\(\lnot { cut}_B(\varphi )\)

    \({ cut}_B(\langle \alpha \rangle \varphi )\)\(=\)\(\langle \alpha \rangle { cut}_B(\varphi )\)   if \(\alpha \not \in B\)

    \({ cut}_B(\langle \alpha \rangle \varphi )\)\(=\)\(\textsf {F}\)   if \(\alpha \in B\)

    \({ cut}_B(\langle \epsilon \rangle \varphi )\)\(=\)\(\langle \epsilon \rangle {} { cut}_B(\varphi )\)

     

Proof

  1. 1.

    That \({ cut}_n\) and \({ cut}_B\) satisfy (cut-2) follows immediately from their inductive definitions. We need to show that \(\pi _n(p) \models \varphi \Longleftrightarrow p \models { cut}_{n}(\varphi )\). The proof proceeds by induction on the structure of \(\varphi \). We consider the following cases:

     
  • \(\varphi = \bigwedge _{i \in I} \psi _i\): \(\pi _n(p) \models \bigwedge _{i \in I} \psi _i ~~\Longleftrightarrow \)

    \( \forall _{i \in I}: \pi _n(p) \models \psi _i ~~\Longleftrightarrow \) (IH)

    \( \forall _{i \in I}: p \models { cut}_n(\psi _i) ~~\Longleftrightarrow \)

    \(p \models \bigwedge _{i \in I} { cut}_n(\psi _i) ~~\Longleftrightarrow \) (definition of \({ cut}_n\))

    \(p \models { cut}_n(\bigwedge _{i \in I} \psi _i)\)

  • \(\varphi = \langle a\rangle \psi \):

    We clearly have \(\pi _0(p) \not \models \langle a\rangle \psi \) and \(p\not \models { cut}_0(\langle a\rangle \psi )=\textsf {F}\). Hence the statement holds for \(n=0\).

    \(\pi _{n+1}(p) \models \langle a\rangle \psi ~~\Longleftrightarrow \) (rule R-pro-act + semantics diamond)

    \(\exists p':\,(p {\mathop {\longrightarrow }\limits ^{a}} p' ~\wedge ~ \pi _{n}(p') \models \psi ) ~~\Longleftrightarrow \) (IH)

    \(\exists p':\,(p {\mathop {\longrightarrow }\limits ^{a}} p' ~\wedge ~ p' \models { cut}_{n}(\psi )) ~~\Longleftrightarrow \) (semantics diamond)

    \(p \models \langle a\rangle {} { cut}_{n}(\psi ) ~~\Longleftrightarrow \) (definition of \({ cut}_n\))

    \( p \models { cut}_{n+1}(\langle a\rangle \psi )\)

  • \(\varphi = \langle \epsilon \rangle \psi \):

    \(\pi _n(p) \models \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (semantics weak diamond)

    \(\exists k \ge 0. \exists pp_0, \dots , pp_k:~ \pi _n(p) = pp_0 {\mathop {\longrightarrow }\limits ^{\tau }} \dots {\mathop {\longrightarrow }\limits ^{\tau }} pp_k ~\wedge ~ pp_k \models \psi \)

    \(\Longleftrightarrow \) (\(\tau \)-steps can be derived only from rule R-pro-tau)

    \(\exists k \ge 0. \exists p_0, \dots , p_k:~ p = p_0 ~\wedge ~ p_0 {\mathop {\longrightarrow }\limits ^{\tau }} \dots {\mathop {\longrightarrow }\limits ^{\tau }} p_k ~\wedge ~ \pi _n(p_k) \models \psi ~~\Longleftrightarrow \) (IH)

    \(\exists k \ge 0. \exists p_0, \dots , p_k:~ p = p_0 ~\wedge ~ p_0 {\mathop {\longrightarrow }\limits ^{\tau }} \dots {\mathop {\longrightarrow }\limits ^{\tau }} p_k ~\wedge ~ p_k \models { cut}_{n}(\psi )\)

    \(\Longleftrightarrow \) (semantics weak diamond)

    \(p \models \langle \epsilon \rangle { cut}_{n}(\psi ) ~~\Longleftrightarrow \) (definition of \({ cut}_n\))

    \(p \models { cut}_{n}(\langle \epsilon \rangle \psi )\)

  • \(\varphi = \lnot \psi \):

    \(\pi _n(p) \models \lnot \psi ~~\Longleftrightarrow \)

    \(\pi _n(p) \not \models \psi ~~\Longleftrightarrow \) (IH)

    \( p \not \models { cut}_n(\psi ) ~~\Longleftrightarrow \)

    \(p \models \lnot { cut}_n(\psi ) ~~\Longleftrightarrow \) (definition of \({ cut}_n\))

    \( p \models { cut}_n(\lnot \psi )\)

  1. 2.

    We need to show that for all \(B \subseteq Act\), \(\partial _B(p) \models \varphi \Longleftrightarrow p \models { cut}_{B}(\varphi )\). This proof follows the same line of reasoning as the one for the \(\pi _{n}\) operators. The three cases, conjunction, weak diamond, and negation, are almost the same as the corresponding ones above. (In the weak diamond case, we use the fact that \(\tau \notin B\).) Therefore, we only give an explicit proof for the case of the diamond operator.

     
  • \(\varphi = \langle \alpha \rangle \psi \). We consider two cases:
    • \(\alpha \in B\):

      Then \(\partial _B(p) \not \models \langle \alpha \rangle \psi \) (rule R-enc) and \(p \not \models { cut}_B(\langle \alpha \rangle \psi )=\textsf {F}\) (by the definition of \({ cut}_B\)).

    • \(\alpha \notin B\):

      \(\partial _B(p) \models \langle \alpha \rangle \psi ~~\Longleftrightarrow \) (rule R-enc + semantics diamond)

      \(\exists p': p {\mathop {\longrightarrow }\limits ^{\alpha }} p' ~\wedge ~ \partial _B(p') \models \psi ~~\Longleftrightarrow \) (IH)

      \(\exists p': p {\mathop {\longrightarrow }\limits ^{\alpha }} p' ~\wedge ~ p' \models { cut}_B(\psi ) ~~\Longleftrightarrow \)

      \(p \models \langle \alpha \rangle {} { cut}_B(\psi ) ~~\Longleftrightarrow \) (definition of \({ cut}_B\) + \(\alpha \notin B\))

      \( p \models { cut}_B(\langle \alpha \rangle \psi )\)\(\square \)

Theorem 3

For each \({{\mathcal {O}}}\subseteq { HML}_\tau \) that satisfies (res), \(\sim _{{\mathcal {O}}}\) is a congruence with respect to the projection operators \(\pi _n\) (for \(n\ge 0\)) and the encapsulation operators \(\partial _B\) (for \( B \subseteq { Act}\)).

Proof

By Proposition 2, \({ cut}_n\) and \({ cut}_B\) satisfy (cut-1) with respect to the \(\pi _n\) and the \(\partial _B\), and satisfy (cut-2) as well. Since moreover \({{\mathcal {O}}}\) satisfies (res), the congruence property follows by Proposition 1. \(\square \)

That requirement (res) in Proposition 1 is essential is shown by the following counterexamples.
  • For the projection operator, take \({{\mathcal {O}}}= \{ \langle a\rangle \lnot \langle a\rangle \textsf {T}\}\), which violates (res) because \(\langle a\rangle \textsf {T}\not \in \,{\overline{{{\mathcal {O}}}}}\). We have \(a.a.\mathbf{0} \sim _{{\mathcal {O}}}\mathbf{0}\), but \(\pi _1(a.a.\mathbf{0}) \not \sim _{{\mathcal {O}}}\pi _1(\mathbf{0})\), because \(\pi _1(a.a.\mathbf{0}) \models \langle a\rangle \lnot \langle a\rangle \textsf {T}\) while \(\pi _1(\mathbf{0})\) does not satisfy this formula.

  • For encapsulation, take \({{\mathcal {O}}}= \{ \langle a\rangle \lnot \langle b\rangle \textsf {T}\}\). We have \(a.b.\mathbf{0} \sim _{{\mathcal {O}}}\mathbf{0}\), but \(\partial _{\{b\}}(a.b.\mathbf{0}) \not \sim _{{\mathcal {O}}}\partial _{\{b\}}(\mathbf{0})\), because \(\partial _{\{b\}}(a.b.\mathbf{0}) \models \langle a\rangle \lnot \langle b\rangle \textsf {T}\) while \(\partial _{\{b\}}(\mathbf{0})\) does not satisfy this formula.

(res) is satisfied by every modal characterization from Sect. 2, except for (concrete and weak) completed trace observations. Completed trace equivalence is a congruence with respect to the projection operators \(\pi _n\), but not with respect to the encapsulation operators \(\partial _B\) (if \(B\ne \emptyset \)). For instance, we clearly have \(a.b.\mathbf{0}+a.c.\mathbf{0}\,\sim _{CT}\,a.(b.\mathbf{0}+c.\mathbf{0})\), but Open image in new window, because the first process has completed trace a, while the second process does not.

Corollary 5

\(\sim _{ T}\), \(\sim _{ F}\), \(\sim _{ R}\), \(\sim _{ FT}\), \(\sim _{ RT}\), \(\sim _{ I\!F}\), \(\sim _{ P\!F}\), \(\sim _{ nS}\) (for \(n\ge 1\)), \(\sim _{ RS}\), and \(\sim _{ B}\) are congruences for the projection operators \(\pi _n\) as well as the encapsulation operators \(\partial _B\).

Corollary 6

\(\sim _{ WT}\), \(\sim _{ WF}\), \(\sim _{ WB}\), \(\sim _{ RWB}\), \(\sim _{ DB}\), \(\sim _{ RDB}\), \(\sim _{ \eta B}\), \(\sim _{ R\eta B}\), \(\sim _{ BB}\) and \(\sim _{ RBB}\) are congruences for the projection operators \(\pi _n\) as well as the encapsulation operators \(\partial _B\).

3.4 Modal decomposition technique

Sufficient congruence requirements for process operators may be obtained via the modal decomposition method from [9, 15]. This technique was introduced in the context of structural operational semantics for developing congruence formats with respect to specific preorders and equivalences [7, 10].

We employ a simplified definition of a modal decomposition. Given an n-ary process operator \(\bigtriangleup \), a (valid) modal decomposition with respect to \(\bigtriangleup \) is a mapping of the form:
$$\begin{aligned} \bigtriangleup ^{-1}: { HML}_\tau \rightarrow {{\mathcal {P}}}(\{1,\ldots ,n\} \rightarrow { HML}_\tau ) \end{aligned}$$
with the property that for all process terms \(p_1, \dots ,p_n\),
$$\begin{aligned} \bigtriangleup (p_1, \dots , p_n) \models \varphi \,\Longleftrightarrow \, \exists \varPsi \in \bigtriangleup ^{-1}(\varphi ).\,\, \forall i \in \{1, \dots , n\}:\,\, p_i \models \varPsi (i) \end{aligned}$$
In other words, a modal decomposition provides a sound and complete method to infer satisfaction of a given formula by a composite process \(\bigtriangleup (p_1, \dots , p_n)\) from the satisfaction of certain formulas by its components \(p_1, \dots , p_n\). The utility of modal decomposition in the context of congruence requirements is established by the following proposition.

Proposition 3

Let \(\bigtriangleup \) be a process operator of arity n and \(\bigtriangleup ^{-1}\) a modal decomposition with respect to \(\bigtriangleup \). Suppose further that \({{\mathcal {O}}}\subseteq { HML}_\tau \) satisfies, for each formula \(\varphi \):
$$\begin{aligned} \hbox { for all } \varPsi \in \bigtriangleup ^{-1}(\varphi ) \hbox { and all } i \in \{1, \dots , n\}, \varPsi (i) \in {\overline{{{\mathcal {O}}}}}. \end{aligned}$$
Then \(\bigtriangleup \) is a congruence with respect to \(\sim _{{\mathcal {O}}}\).

Proof

Let \(p_i\sim _{{\mathcal {O}}}q_i\) for \(i=1,\ldots ,n\). Consider any \(\varphi \in {{\mathcal {O}}}\). Then \(\bigtriangleup (p_1,\ldots ,p_n)\models \varphi \Longleftrightarrow \exists \varPsi \in \bigtriangleup ^{-1}(\varphi ).\,\forall i\in \{1,\ldots ,n\}:\,p_i\models \varPsi (i)\Longleftrightarrow \) (since \(\varPsi (i)\in {\overline{{{\mathcal {O}}}}}\) and \(p_i\sim _{{\mathcal {O}}}q_i\) for \(i=1,\ldots ,n\)) \(\exists \varPsi \in \bigtriangleup ^{-1}(\varphi ).\,\forall i\in \{1,\ldots ,n\}:\,q_i\models \varPsi (i)\Longleftrightarrow \bigtriangleup (q_1,\ldots ,q_n)\models \varphi \). So \(\bigtriangleup (p_1,\ldots ,p_n)\sim _{{\mathcal {O}}}\bigtriangleup (q_1,\ldots ,q_n)\). \(\square \)

The reasoning in the previous section that allows us to provide congruence requirements for certain restriction operators can be seen as a particular, though rather trivial, instance of the modal decomposition method from [9]. For instance, for the projection operator we can define \(\pi _n^{-1}(\varphi )\) as \(\{ 1 \mapsto { cut}_{n}(\varphi ) \}\).

The modal decomposition method will prove useful in the following sections, where we shall consider renaming and abstraction operators.

3.5 Renaming

The renaming operator \(\rho _{f}\) from [3] changes labels of concrete actions performed by a given process, according to a relabeling function \(f : Act \rightarrow Act\). For convenience, we shall always consider an extended relabeling function \(f : Act \cup \{\tau \} \rightarrow Act \cup \{\tau \}\) such that \(f(\tau ) = \tau \). The operator is defined by the following transition rule:The modal decomposition approach is particularly suitable for renaming. We first need to provide a proper modal decomposition function \(\rho _{f}^{-1}\). Since renaming is unary, the decomposition can be defined as a function \(\rho _{f}^{-1}: { HML}_\tau \rightarrow {{\mathcal {P}}}({ HML}_\tau )\).
  • \(\rho _{f}^{-1}(\bigwedge _{i \in I} \varphi _i) ~=~ \{ \bigwedge _{i \in I} \varphi '_i ~|~ \varphi '_i \in \rho _{f}^{-1}(\varphi _i)\}\)

  • \(\rho _{f}^{-1}(\langle \alpha \rangle \varphi ) ~=~ \{ \langle \beta \rangle \varphi ' ~|~ f(\beta ) = \alpha \wedge \varphi ' \in \rho _{f}^{-1}(\varphi )\}\)

  • \(\rho _{f}^{-1}(\langle \epsilon \rangle \varphi ) ~=~ \{\langle \epsilon \rangle \varphi ' ~|~ \varphi ' \in \rho _{f}^{-1}(\varphi )\}\)

  • \(\rho _{f}^{-1}(\lnot \varphi ) ~=~ \{ \bigwedge _{\varphi ' \in \rho _{f}^{-1}(\varphi )} \lnot \varphi '\}\)

We show that \(\rho _{f}^{-1}\) is a valid modal decomposition.

Proposition 4

For each renaming function f, process p, and formula \(\varphi \),
$$\begin{aligned} \rho _{f}(p) \models \varphi ~~\Longleftrightarrow ~~ \exists \varphi ' \in \rho _{f}^{-1}(\varphi ):~ p \models \varphi ' \end{aligned}$$

Proof

We apply structural induction on \(\varphi \). We consider the following inductive cases:
  • \(\varphi = \bigwedge _{i \in I} \psi _i\):

    \(\rho _{f}(p) \models \bigwedge _{i \in I} \psi _i ~~\Longleftrightarrow \)

    \(\forall i \in I: \rho _{f}(p) \models \psi _i ~~\Longleftrightarrow \) (IH)

    \(\forall i \in I: \exists \psi '_i \in \rho _{f}^{-1}(\psi _i) : p \models \psi '_i ~~\Longleftrightarrow \)

    \(p \models \bigwedge _{i \in I} \psi '_i\) where for all \(i \in I\), \(\psi '_i \in \rho _{f}^{-1}(\psi _i) ~~\Longleftrightarrow \) (definition of \(\rho _{f}^{-1}\))

    \(\exists \psi ' \in \rho _{f}^{-1}(\bigwedge _{i \in I} \psi _i) : p \models \psi '\)

  • \(\varphi = \langle a\rangle \psi \) where \(a \not \in f(Act)\):

    The statement holds, since \(a \not \in f(Act)\) implies \(\rho _{f}(p) \not \models \langle a\rangle \psi \), and on the other hand \(f^{-1}(a)=\emptyset \) implies \(\rho _{f}^{-1}(\langle a\rangle \psi ) = \emptyset \).

  • \(\varphi = \langle \alpha \rangle \psi \) where \(\alpha \in f(Act \cup \{\tau \})\):

    \(\rho _{f}(p) \models \langle \alpha \rangle \psi ~~\Longleftrightarrow \) (semantics diamond + R-ren)

    \(\exists p'.\,\exists \beta :\,f(\beta ) = \alpha \wedge p {\mathop {\longrightarrow }\limits ^{\beta }} p' \wedge \rho _{f}(p') \models \psi ~~\Longleftrightarrow \) (IH)

    \(\exists p'.\,\exists \beta :\,f(\beta ) = \alpha \wedge p {\mathop {\longrightarrow }\limits ^{\beta }} p' \wedge \exists \psi ' \in \rho _{f}^{-1}(\psi ): p' \models \psi ' ~~\Longleftrightarrow \) (semantics diamond)

    \(\exists \beta : f(\beta ) = \alpha \wedge \exists \psi ' \in \rho _{f}^{-1}(\psi ): p \models \langle \beta \rangle \psi ' ~~\Longleftrightarrow \) (definition of \(\rho _{f}^{-1}\))

    \(\exists \psi ' \in \rho _{f}^{-1}(\langle \alpha \rangle \psi ): p \models \psi '\)

  • \(\varphi = \langle \epsilon \rangle \psi \):

    \(\rho _{f}(p) \models \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (semantics weak diamond+ R-ren)

    \(\exists p':\,p {\mathop {\Longrightarrow }\limits ^{\epsilon }}p' \wedge \rho _{f}(p') \models \psi ~~\Longleftrightarrow \) (IH)

    \(\exists p':\,p {\mathop {\Longrightarrow }\limits ^{\epsilon }}p' \wedge \exists \psi ' \in \rho _{f}^{-1}(\psi ): p' \models \psi ' ~~\Longleftrightarrow \) (semantics weak diamond)

    \(\exists \psi ' \in \rho _{f}^{-1}(\psi ): p \models \langle \epsilon \rangle \psi ' ~~\Longleftrightarrow \) (definition of \(\rho _{f}^{-1}(\psi )\))

    \(\exists \psi ' \in \rho _{f}^{-1}(\langle \epsilon \rangle \psi ) : p \models \psi '\)

  • \(\varphi = \lnot \psi \):

    \(\rho _{f}(p) \models \lnot \psi ~~\Longleftrightarrow \)

    \(\rho _{f}(p) \not \models \psi ~~\Longleftrightarrow \) (IH)

    \(\forall \psi ' \in \rho _{f}^{-1}(\psi ) : p \not \models \psi ' ~~\Longleftrightarrow \)

    \(\forall \psi ' \in \rho _{f}^{-1}(\psi ) : p \models \lnot \psi ' ~~\Longleftrightarrow \)

    \(p \models \bigwedge _{ \psi ' \in \rho _{f}^{-1}(\psi )} \lnot \psi ' ~~\Longleftrightarrow \) (definition of \(\rho _{f}^{-1}\))

    \(\exists \psi '' \in \rho _{f}^{-1}(\lnot \psi ) : p \models \psi ''\)\(\square \)

The proposition above, combined with Proposition 3, yields the following result.

Theorem 4

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \) and \(f:Act\rightarrow Act\). If for all formulas \(\varphi \)
$$\begin{aligned} \textsc {(ren)} ~~~~~ \varphi \in {{\mathcal {O}}}~~\implies ~~ \rho _{f}^{-1}(\varphi ) \subseteq {\overline{{{\mathcal {O}}}}} \end{aligned}$$
then \(\sim _{{\mathcal {O}}}\) is a congruence with respect to the relabeling operator \(\rho _{f}\).

The requirement (ren) is satisfied by every modal characterization from Sect. 2.

Corollary 7

\(\sim _{ T}\), \(\sim _{ CT}\), \(\sim _{ F}\), \(\sim _{ R}\), \(\sim _{ FT}\), \(\sim _{ RT}\), \(\sim _{ I\!F}\), \(\sim _{ P\!F}\), \(\sim _{ nS}\) (for \(n\ge 1\)), \(\sim _{ RS}\), and \(\sim _{ B}\) are congruences for the relabeling operator \(\rho _{f}\).

Corollary 8

\(\sim _{ WT}\), \(\sim _{ WCT}\), \(\sim _{ WF}\), \(\sim _{ WB}\), \(\sim _{ RWB}\), \(\sim _{ DB}\), \(\sim _{ RDB}\), \(\sim _{ \eta B}\), \(\sim _{ R\eta B}\), \(\sim _{ BB}\), and \(\sim _{ RBB}\) are congruences for the relabeling operator \(\rho _{f}\).

3.6 Abstraction

The abstraction operator \(\mathcal {T}_{H}\) from [5], also known as the hiding operator, converts concrete actions from a set \(H \subseteq Act\) into internal ones.We proceed to define a modal decomposition function \(\mathcal {T}_{H}^{-1}\).
  • \(\mathcal {T}_{H}^{-1}(\bigwedge _{i \in I} \varphi _i) ~=~ \{\bigwedge _{i \in I} \varphi '_i\ | \ \varphi _i' \in \mathcal {T}_{H}^{-1}(\varphi _i)\}\)

  • \(\mathcal {T}_{H}^{-1}(\langle \tau \rangle \varphi ) ~=~ \{ \langle \alpha \rangle \varphi ' \ | \ \alpha \in H \cup \{\tau \} \wedge \varphi ' \in \mathcal {T}_{H}^{-1}(\varphi ) \}\)

  • \(\mathcal {T}_{H}^{-1}(\langle a\rangle \varphi )) ~=~ {\left\{ \begin{array}{ll} \{\langle a\rangle \varphi '\ | \ \varphi ' \in \mathcal {T}_{H}^{-1}(\varphi )\} &{} \text{ if } a \notin H \\ \emptyset &{} \text{ if } a \in H\end{array}\right. }\)

  • \(\mathcal {T}_{H}^{-1}(\langle \epsilon \rangle \varphi ) = \{ \langle \epsilon \rangle \langle a_1\rangle \cdots \langle \epsilon \rangle \langle a_n\rangle \langle \epsilon \rangle \varphi '\ |\ n\ge 0 \wedge a_1,\ldots ,a_n \in H \wedge \varphi ' \in \mathcal {T}_{H}^{-1}(\varphi ) \}\)

  • \(\mathcal {T}_{H}^{-1}(\lnot \varphi ) ~=~ \{\bigwedge _{\varphi ' \in \mathcal {T}_{H}^{-1}(\varphi )} \lnot \varphi '\}\)

We show that \(\mathcal {T}_{H}^{-1}\) is a valid modal decomposition.

Proposition 5

Let \(H\subseteq Act\). For each process p and formula \(\varphi \),
$$\begin{aligned} \mathcal {T}_{H}(p) \models \varphi ~~\Longleftrightarrow ~~ \exists \varphi ' \in \mathcal {T}_{H}^{-1}(\varphi ):~ p \models \varphi '\end{aligned}$$

Proof

We apply induction on the structure of \(\varphi \).
  • \(\psi = \bigwedge _{i \in I} \psi _i\):

    \(\mathcal {T}_{H}(p) \models \bigwedge _{i \in I} \psi _i ~~\Longleftrightarrow \)

    \(\forall i \in I: \,\mathcal {T}_{H}(p) \models \psi _i ~~\Longleftrightarrow \) (IH)

    \(\forall i \in I. \exists \psi '_i \in \mathcal {T}_{H}^{-1}(\psi _i): \,p \models \psi '_i ~~\Longleftrightarrow \)

    \( p \models \bigwedge _{i \in I} \psi '_i\) where for all \(i \in I\)\(\psi '_i \in \mathcal {T}_{H}^{-1}(\psi _i)\)\(~~\Longleftrightarrow \) (definition of \(\mathcal {T}_{H}^{-1}\))

    \(\exists \psi ' \in \mathcal {T}_{H}^{-1}(\bigwedge _{i \in I} \psi _i): \,p \models \psi '\)

  • \(\varphi = \langle a\rangle \psi \). We distinguish two cases.
    • \(a \in H\):

      The statement holds, since for all p, \(\psi \), and \(a\in H\) we have \(\mathcal {T}_{H}(p) \not \models \langle a\rangle \psi \), and on the other hand \(\mathcal {T}_{H}^{-1}(\langle a\rangle \psi ) = \emptyset \) by the definition of \(\mathcal {T}_{H}^{-1}\).

    • \(a \notin H\):

      \(\mathcal {T}_{H}(p) \models \langle a\rangle \psi ~~\Longleftrightarrow \) (semantics diamond + R-abs-1)

      \(\exists p':\,p {\mathop {\longrightarrow }\limits ^{a}} p' ~\wedge ~ \mathcal {T}_{H}(p') \models \psi ~~\Longleftrightarrow \) (IH)

      \(\exists p':\,p {\mathop {\longrightarrow }\limits ^{a}} p' ~\wedge ~ \exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ): p' \models \psi ' ~~\Longleftrightarrow \) (semantics diamond)

      \(\exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ):\,p \models \langle a\rangle \psi ' ~~\Longleftrightarrow \) (definition of \(\mathcal {T}_{H}^{-1}\))

      \(\exists \psi ' \in \mathcal {T}_{H}^{-1}(\langle a\rangle \psi ):\,p \models \psi '\)

  • \(\varphi = \langle \tau \rangle \psi \):

    \(\mathcal {T}_{H}(p) \models \langle \tau \rangle \psi ~~\Longleftrightarrow \) (semantics diamond + rules of \(\mathcal {T}_{H}\))

    \(\exists p'.\,\exists \alpha \in H\cup \{\tau \}:\,p {\mathop {\longrightarrow }\limits ^{\alpha }} p' ~\wedge ~ \mathcal {T}_{H}(p') \models \psi ~~\Longleftrightarrow \) (IH)

    \(\exists p'.\,\exists \alpha \in H\cup \{\tau \}:\,p {\mathop {\longrightarrow }\limits ^{\alpha }} p' \wedge \, \exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ):p' \models \psi ' ~~\Longleftrightarrow \) (semantics diamond)

    \(\exists \alpha \in H \cup \{\tau \}.\,\exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ):\,p \models \langle \alpha \rangle \psi ' ~~\Longleftrightarrow \) (definition of \(\mathcal {T}_{H}^{-1}\))

    \(\exists \psi ' \in \mathcal {T}_{H}^{-1}(\langle \tau \rangle \psi ): \,p \models \psi '\)

  • \(\varphi = \langle \epsilon \rangle \psi \):

    \(\mathcal {T}_{H}(p) \models \langle \epsilon \rangle \psi ~~\Longleftrightarrow \) (semantics weak diamond)

    \(\exists p':\,\mathcal {T}_{H}(p) {\mathop {\Longrightarrow }\limits ^{\epsilon }}\mathcal {T}_{H}(p') ~\wedge ~ \mathcal {T}_{H}(p') \models \psi ~~\Longleftrightarrow \) (IH)

    \(\exists p':\,\mathcal {T}_{H}(p) {\mathop {\Longrightarrow }\limits ^{\epsilon }}\mathcal {T}_{H}(p') ~\wedge ~ \exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ):\,p' \models \psi ' ~~\Longleftrightarrow \) (rules of \(\mathcal {T}_{H}\))

    \(\exists n\ge 0.~\exists p_0,\ldots ,p_n:\,(p{\mathop {\Longrightarrow }\limits ^{\epsilon }}p_0~\wedge ~ \exists a_1,\ldots ,a_n\in H.~\forall 0\le i<n:\,(p_i {\mathop {\longrightarrow }\limits ^{a_{i+1}}}\,{\mathop {\Longrightarrow }\limits ^{\epsilon }}p_{i+1}~\wedge \exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ):\,\mathcal {T}_{H}(p_n) \models \psi '))\)

    \(\Longleftrightarrow \) (semantics diamond and weak diamond operators)

    \(\exists n\ge 0.\,\exists a_1,\ldots ,a_n {\in } H.\,\exists \psi ' \in \mathcal {T}_{H}^{-1}(\psi ): p \models \langle \epsilon \rangle \langle a_1\rangle \cdots \langle \epsilon \rangle \langle a_n\rangle \langle \epsilon \rangle \psi '\)

    \(\Longleftrightarrow \) (definition of \(\mathcal {T}_{H}^{-1}\))

    \(\exists \psi '' \in \mathcal {T}_{H}^{-1}(\langle \epsilon \rangle \psi ): \,p \models \psi ''\)

  • \(\varphi = \lnot \psi \):

    \(\mathcal {T}_{H}(p) \models \lnot \psi ~~\Longleftrightarrow \)

    \(\mathcal {T}_{H}(p) \not \models \psi ~~\Longleftrightarrow \) (IH)

    \(\forall \psi ' \in \mathcal {T}_{H}^{-1}(\psi ): \,p \not \models \psi '~~\Longleftrightarrow \)

    \(\forall \psi ' \in \mathcal {T}_{H}^{-1}(\psi ): \,p \models \lnot \psi ' ~~\Longleftrightarrow \)

    \(p \models \bigwedge _{\psi ' \in \mathcal {T}_{H}^{-1}(\psi )}\lnot \psi ' ~~\Longleftrightarrow \) (definition of \(\mathcal {T}_{H}^{-1}\))

    \(\exists \psi '' \in \mathcal {T}_{H}^{-1}(\lnot \psi ): \,p \models \psi ''\)\(\square \)

The proposition above, combined with Proposition 3, yields the following result.

Theorem 5

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \) and \(H\subseteq Act\). If for all formulas \(\varphi \)
$$\begin{aligned} \textsc {(abs)} ~~~~~ \varphi \in {{\mathcal {O}}}~~\implies ~~ \mathcal {T}_{H}^{-1}(\varphi ) \subseteq {\overline{{{\mathcal {O}}}}} \end{aligned}$$
then \(\sim _{{\mathcal {O}}}\) is a congruence with respect to the abstraction operator \(\mathcal {T}_H\).

The requirement (abs) is satisfied by every weak modal characterization from Sect. 2.

Corollary 9

\(\sim _{ WT}\), \(\sim _{ WCT}\), \(\sim _{ WF}\), \(\sim _{ WB}\), \(\sim _{ RWB}\), \(\sim _{ DB}\), \(\sim _{ RDB}\), \(\sim _{ \eta B}\), \(\sim _{ R\eta B}\), \(\sim _{ BB}\), and \(\sim _{ RBB}\) are congruences for the abstraction operator \(\mathcal {T}_H\).

3.7 Parallel composition

The parallel composition operator interleaves the behavior of its two arguments, and also allows synchronous communication between two concurrent actions of its two arguments. Let \(\gamma :Act\times Act\rightarrow Act\) define a partially defined, symmetric function, representing the result of the communication between two actions. The parallel composition operator is defined by the following transition rules.We note that allowing \(\tau \) in the range of \(\gamma \) would lead to a more strict version of the syntactic congruence requirement (par) in Theorem 6. A CCS-like parallel operator can be obtained by combining the parallel composition operator from this section with the abstraction operator from Sect. 3.6.

To build some intuition for the upcoming syntactic congruence requirement for the parallel composition operator, let us restrict for a moment to only trace formulas (meaning that conjunctions are disregarded) and ignore \(\tau \). The following example shows that requirement (act-1) from Theorem 2 and even being closed under substrings does not guarantee congruence for the parallel composition operator. (By a substring of a string w we mean a subsequence of elements appearing consecutively in w.) Take \({{\mathcal {O}}}= \{\textsf {T}, \langle a\rangle \textsf {T},\langle b\rangle \textsf {T},\langle a\rangle \langle b\rangle \textsf {T},\langle a\rangle \langle b\rangle \langle a\rangle \textsf {T},\langle b\rangle \langle a\rangle \textsf {T}\}\). This language satisfies (act-1) and is also closed under prefixes and substrings (but not arbitrary subsequences). However, we have \(a.a.\mathbf{0} \sim _{{\mathcal {O}}}a.\mathbf{0}\), but \((a.a.\mathbf{0}) \,||\, (b.\mathbf{0}) \models \langle a\rangle \langle b\rangle \langle a\rangle \textsf {T}\) while \((a.\mathbf{0}) \,||\, (b.\mathbf{0})\) does not satisfy this formula. This example suggests that if a trace \(\sigma \) belongs to \({{\mathcal {O}}}\), then all subsequences of \(\sigma \) must belong to the language as well. This is not unexpected; the behaviour of parallel composition consists of all possible interleavings of the component processes, and all of these interleavings should be described in the modal characterization.

It is also necessary to close the language on subconjunctions. Indeed, take \({{\mathcal {O}}}= \{ \langle a\rangle \textsf {T}\wedge \langle b\rangle \textsf {T}\}\), a language which does not meet this condition. We have \(a.\mathbf{0} \sim _{{\mathcal {O}}}b.\mathbf{0}\), but \((a.\mathbf{0}) \,||\, (b.\mathbf{0})\models \langle a\rangle \textsf {T}\wedge \langle b\rangle \textsf {T}\) while \((b.\mathbf{0}) \,||\, (b.\mathbf{0})\) does not satisfy this formula. This concludes the intermezzo to strengthen the intuition for the (admittedly syntactically rather complex) technical developments in the remainder of this section.

For all the operators and semantics considered so far, we have worked with standard modal characterisations that use the base \({ HML}_\tau \) syntax. However, for the parallel composition operator it is beneficial to include certain additional constructs. Namely, we introduce three operators \(\emptyset ,{\widetilde{\emptyset }}, \langle {\hat{\tau }}\rangle \) which, while redundant from the expressiveness point of view, facilitate providing congruence requirements. Their semantics are:
  • \(p \models \emptyset ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ p \models \bigwedge _{a \in { Act}} \lnot \langle a\rangle \textsf {T}\)

  • \(p \models {\widetilde{\emptyset }}~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ p \models \bigwedge _{a \in { Act}} \lnot \langle \epsilon \rangle \langle a\rangle \textsf {T}\)

  • \(p \models \langle {\hat{\tau }}\rangle \varphi ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ p \models \varphi \vee \langle \tau \rangle \varphi \)

The three operators are not shorthands, but separate syntactic entities. We shall use the notation \({ HML}_\tau \cup \{\emptyset ,{\widetilde{\emptyset }},\langle {\hat{\tau }}\rangle \}\) to denote the language obtained by endowing \({ HML}_\tau \) with these additional constructs.
Below are the alternative modal characterisations of completed trace, weak completed trace, and (rooted) branching bisimulation semantics:
  • alternative completed trace observations\({\widehat{{{\mathcal {O}}}}}_{CT}\)\(\varphi {:}{:}= \langle a\rangle \varphi '\,|\, \textsf {T}\,|\, \emptyset \)

  • alternative weak completed trace observations\({\widehat{{{\mathcal {O}}}}}_{ WCT}\)\(\varphi {:}{:}= \langle \epsilon \rangle \langle a\rangle \langle \epsilon \rangle \varphi '\,|\, \textsf {T}\,|\, {\widetilde{\emptyset }}\)

  • alternative branching bisimulation observations\({\widehat{{{\mathcal {O}}}}}_{ BB}\): \(\varphi {:}{:}= \langle \epsilon \rangle \varphi '\langle a\rangle \varphi '' \,|\, \langle \epsilon \rangle \varphi '\langle {\hat{\tau }}\rangle \varphi '' \,| \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

  • alternative rooted branching bisimulation observations\({\widehat{{{\mathcal {O}}}}}_{ RBB}\): \(\varphi {:}{:}= \langle \alpha \rangle \psi ~(\psi \in {\widehat{{{\mathcal {O}}}}}_{BB}) \,|\, \psi ~(\psi \in {\widehat{{{\mathcal {O}}}}}_{BB}) \,|\, \bigwedge _{i \in I} \varphi _{i}\,|\, \lnot \varphi '\)

Let \(\varphi ^{\Rightarrow }\) denote the set of formulas logically entailed by \(\varphi \), i.e., \(\varphi ^{\Rightarrow } = \{ \psi \in { HML}_\tau ~|~ \lnot \varphi \vee \psi \equiv \textsf {T}\}\). The function \(\textsf {Par}\), defined below, can be seen as an inverse modal decomposition: for a pair of simpler formulas, it yields a set of more complex formulas that are supposed to be satisfied by a composite process.

Definition 1

\(\textsf {Par}: {{ HML}_\tau } \times {{ HML}_\tau } \rightarrow {{\mathcal {P}}}({ HML}_\tau )\) is defined inductively by:
  • \(\bigwedge _{i \in I} \varphi _i \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ \forall i \in I. \exists \varphi ^i_A \in \varphi _A^{\Rightarrow }, \varphi ^i_B \in \varphi _B^{\Rightarrow }: ~\varphi _i \in \textsf {Par}(\varphi ^i_A,\varphi ^i_B)\)

  • \(\langle \alpha \rangle \varphi \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ \exists \psi _{C}: ~\langle \alpha \rangle \psi _{C} \in \varphi _A^{\Rightarrow } ~\wedge ~ \varphi \in \textsf {Par}(\psi _C,\varphi _B)\)

    \(\vee ~~ \exists \psi _{D}: ~\langle \alpha \rangle \psi _{D} \in \varphi _B^{\Rightarrow } ~\wedge ~ \varphi \in \textsf {Par}(\varphi _A,\psi _D) ~~\vee ~~ \exists c,d \in Act. \exists \psi _C,\psi _D:\)

    \(\gamma (c,d) = \alpha \,\wedge \, \langle c\rangle \psi _C \in \varphi _A^{\Rightarrow } \,\wedge \, \langle d\rangle \psi _D \in \varphi _B^{\Rightarrow } \,\wedge \, \varphi \in \textsf {Par}(\psi _C,\psi _D)\)

  • \(\langle {\hat{\tau }}\rangle \varphi \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ \exists \psi _{C}: ~\langle {\hat{\tau }}\rangle \psi _{C} \in \varphi _A^{\Rightarrow } ~\wedge ~ \varphi \in \textsf {Par}(\psi _C,\varphi _B)\)

    \(\vee ~ \exists \psi _{D}: ~\langle {\hat{\tau }}\rangle \psi _{D} \in \varphi _B^{\Rightarrow } ~\wedge ~ \varphi \in \textsf {Par}(\varphi _A,\psi _D)\)

  • \(\langle \epsilon \rangle \varphi \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}\)

    \(\exists \psi _{C}, \psi _D: ~\langle \epsilon \rangle \psi _{C} \in \varphi _A^{\Rightarrow } ~\wedge ~ \langle \epsilon \rangle \psi _{D} \in \varphi _B^{\Rightarrow } ~\wedge ~ \varphi \in \textsf {Par}(\psi _C,\psi _D)\)

  • \(\lnot \varphi \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}\)

    \(\forall \varphi _C,\varphi _D: ~\varphi \in \textsf {Par}(\varphi _C,\varphi _D) \implies (\lnot \varphi _C \in \varphi _A^{\Rightarrow } ~\vee ~ \lnot \varphi _D \in \varphi _B^{\Rightarrow })\)

  • \(\emptyset \in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ \emptyset \in \varphi _A^{\Rightarrow } ~\wedge ~\emptyset \in \varphi _B^{\Rightarrow }\)

  • \({\widetilde{\emptyset }}\in \textsf {Par}(\varphi _A,\varphi _B) ~~{\mathop {\Longleftrightarrow }\limits ^\mathrm{def}}~~ {\widetilde{\emptyset }}\in \varphi _A^{\Rightarrow } ~\wedge ~{\widetilde{\emptyset }}\in \varphi _B^{\Rightarrow }\)

The significance of the function \(\textsf {Par}\) is explained by the proposition below.

Proposition 6

For all processes pq and formulas \(\varphi \),
$$\begin{aligned} p \,||\, q \models \varphi ~~\Longleftrightarrow ~~ \exists \varphi _A,\varphi _B:~ p \models \varphi _A ~\wedge ~ q \models \varphi _B ~\wedge ~ \varphi \in \textsf {Par}(\varphi _A,\varphi _B) \end{aligned}$$

Proof

In both directions we apply structural induction on \(\varphi \).

\(\implies \)”: Let \(p \,||\, q \models \varphi \). We need to consider the following cases:
  • \(\varphi = \bigwedge _{i \in I} \psi _i\):

    \(p \,||\, q \models \bigwedge _{i \in I} \psi _i ~~\Longleftrightarrow ~~ \forall i \in I: p \,||\, q \models \psi _i ~~\Longleftrightarrow \) (IH)

    \(\forall i \in I.\,\exists \psi _A^i,\psi _B^i: \,p \models \psi _A^i \,\wedge \, q \models \psi _B^i \,\wedge \, \psi _i \in \textsf {Par}(\psi _A^i,\psi _B^i) ~\implies \) (definition of \(\textsf {Par}\))

    \(p \models \bigwedge _{i \in I} \psi _A^i ~\wedge ~ q \models \bigwedge _{i \in I} \psi _B^i~\wedge ~\bigwedge _{i \in I} \psi _i \in \textsf {Par}(\bigwedge _{i \in I} \psi _A^i,\bigwedge _{i \in I} \psi _B^i)\)

  • \(\varphi = \langle \alpha \rangle \psi \):

    \(p \,||\, q \models \langle \alpha \rangle \psi \) gives rise to three possible cases:
    • \(p {\mathop {\longrightarrow }\limits ^{\alpha }} p_1\) and \(p_1 \,||\, q \models \psi \): By the IH, there are formulas \(\psi _1,\psi _q\) such that \(p_1 \models \psi _1\), \(q \models \psi _q\), and \(\psi \in \textsf {Par}(\psi _1,\psi _q)\). Then \(p \models \langle \alpha \rangle \psi _1\). Moreover, by the definition of \(\textsf {Par}\), \(\langle \alpha \rangle \psi \in \textsf {Par}(\langle \alpha \rangle \psi _1,\psi _q)\).

    • \(q {\mathop {\longrightarrow }\limits ^{\alpha }} q_1\) and \(p \,||\, q_1 \models \psi \): The proof mirrors the previous case.

    • \(p {\mathop {\longrightarrow }\limits ^{b}} r\), \(q {\mathop {\longrightarrow }\limits ^{c}} s\), \(\gamma (b,c)=\alpha \), and \(r \,||\, s \models \psi \):

      By the IH, there are formulas \(\psi _r,\psi _s\) such that \(r \models \psi _r\), \(s \models \psi _s\), and \(\psi \in \textsf {Par}(\psi _r,\psi _s)\). Then \(p \models \langle b\rangle \psi _r\) and \(q \models \langle c\rangle \psi _s\). And by the definition of \(\textsf {Par}\), \(\langle \alpha \rangle \psi \in \textsf {Par}(\langle b\rangle \psi _r,\langle c\rangle \psi _s)\).

  • \(\varphi = \langle {\hat{\tau }}\rangle \psi \): \(p \,||\, q \models \langle {\hat{\tau }}\rangle \psi \) gives rise to the following cases:
    • \(p \,||\, q \models \psi \):

      By the IH, there are formulas \(\psi _p,\psi _q\) such that \(p \models \psi _p\), \(q \models \psi _q\), and \(\psi \in \textsf {Par}(\psi _p,\psi _q)\). Since obviously \(\langle {\hat{\tau }}\rangle \psi _p \in \psi _p^\Rightarrow \), from the first case of the definition of \(\textsf {Par}\) for \(\langle {\hat{\tau }}\rangle \) we obtain \(\langle {\hat{\tau }}\rangle \psi \in \textsf {Par}(\langle {\hat{\tau }}\rangle \psi _p,\psi _q)\)

    • \(p \,||\, q \models \langle \tau \rangle \psi \): This case can be split further into two subcases:
      • \(p {\mathop {\longrightarrow }\limits ^{\tau }} p_1\) and \(p_1 \,||\, q \models \psi \): By the IH, there are formulas \(\psi _1,\psi _q\) such that \(p_1 \models \psi _1\), \(q \models \psi _q\), and \(\psi \in \textsf {Par}(\psi _1,\psi _q)\). Then \(p \models \langle \tau \rangle \psi _1\), and hence \(p \models \langle {\hat{\tau }}\rangle \psi _1\). Thus, by the definition of \(\textsf {Par}\), \(\langle {\hat{\tau }}\rangle \psi \in \textsf {Par}(\langle {\hat{\tau }}\rangle \psi _1,\psi _q)\).

      • \(q {\mathop {\longrightarrow }\limits ^{\tau }} q_1\) and \(p \,||\, q_1 \models \psi \): The proof mirrors one from the previous case

  • \(\varphi = \langle \epsilon \rangle \psi \):

    Since \(p \,||\, q \models \langle \epsilon \rangle \psi \), there is a process r such that \(p \,||\, q {\mathop {\Longrightarrow }\limits ^{\epsilon }}r\), and \(r \models \psi \). By the transition rules for the parallel operator, r is of the form \(r_1 \,||\, r_2\) for some processes \(r_1,r_2\) such that \(p {\mathop {\Longrightarrow }\limits ^{\epsilon }}r_1\) and \(q {\mathop {\Longrightarrow }\limits ^{\epsilon }}r_2\). By the IH there are formulas \(\psi _1,\psi _2\) such that \(r_1 \models \psi _1\), \(r_2 \models \psi _2\), and \(\psi \in \textsf {Par}(\psi _1,\psi _2)\). Clearly, \(p \models \langle \epsilon \rangle \psi _1\) and \(q \models \langle \epsilon \rangle \psi _2\). Moreover, by the definition of \(\textsf {Par}\), \(\langle \epsilon \rangle \psi \in \textsf {Par}(\langle \epsilon \rangle \psi _1,\langle \epsilon \rangle \psi _2)\).

  • \(\varphi = \lnot \psi \):

    \(p \,||\, q \models \lnot \psi ~~\Longleftrightarrow ~~ p \,||\, q \not \models \psi ~~\Longleftrightarrow \) (IH)

    \(\lnot (\exists \psi _A,\psi _B:\,\, p \models \psi _A ~\wedge ~ q \models \psi _B ~\wedge ~ \psi \in \textsf {Par}(\psi _A,\psi _B)) ~~\Longleftrightarrow \)

    \(\forall \psi _A,\psi _B:\,\, \psi \in \textsf {Par}(\psi _A,\psi _B) \implies (p \not \models \psi _A ~\vee ~ q \not \models \psi _B)\)      (*)

    Let us define

    \({{\mathcal {A}}} ~=~ \{ \psi _A \in { HML}_\tau ~|~ \exists \psi _B: ~\psi \in \textsf {Par}(\psi _A,\psi _B) ~\wedge ~ p \not \models \psi _A \}\)

    \({{\mathcal {B}}} ~=~ \{ \psi _B \in { HML}_\tau ~|~ \exists \psi _A: ~\psi \in \textsf {Par}(\psi _A,\psi _B) ~\wedge ~ q \not \models \psi _B \}\)

    \(\varPsi _{{\mathcal {A}}} ~=~ \bigwedge _{\psi _A \in {{\mathcal {A}}}} \lnot \psi _A\)

    \(\varPsi _{{\mathcal {B}}} ~=~ \bigwedge _{\psi _B \in {{\mathcal {B}}}} \lnot \psi _B\)

    By the definition of \(\varPsi _{{\mathcal {A}}}\) and \(\varPsi _{{\mathcal {B}}}\), \(p \models \varPsi _{{\mathcal {A}}}\) and \(q \models \varPsi _{{\mathcal {B}}}\). Moreover, from (*) and the definition of \(\textsf {Par}\) we obtain \(\lnot \psi \in \textsf {Par}(\varPsi _{{\mathcal {A}}},\varPsi _{{\mathcal {B}}})\).

  • \(\varphi = \emptyset \):

    Observe that \(p \,||\, q \models \emptyset \) if and only if \(p \models \emptyset \) and \(q \models \emptyset \). Moreover, by the definition of \(\textsf {Par}\), we have \(\emptyset \in \textsf {Par}(\emptyset ,\emptyset )\).

  • \(\varphi = {\widetilde{\emptyset }}\): The proof is similar to the one above.

\(\Longleftarrow \)”: We first show that the statement holds in the two base cases, i.e., \(\varphi =\emptyset \) and \(\varphi ={\widetilde{\emptyset }}\). For \(\varphi =\emptyset \), suppose that \(\exists \varphi _A,\varphi _B: p \models \varphi _A \wedge q \models \varphi _B \wedge \emptyset \in \textsf {Par}(\varphi _A,\varphi _B)\). By the definition of \(\textsf {Par}\), \(\emptyset \in \varphi _A^\Rightarrow \) and \(\emptyset \in \varphi _B^\Rightarrow \), from which in turn we obtain that \(p \models \emptyset \) and \(q \models \emptyset \). From these it follows that \(p \,||\, q \models \emptyset \). The proof for \(\varphi ={\widetilde{\emptyset }}\) is analogous.
In each of the following cases, we assume that \(\exists \varphi _A,\varphi _B: p \models \varphi _A \wedge q \models \varphi _B \wedge \varphi \in \textsf {Par}(\varphi _A,\varphi _B)\), and show that \(p \,||\, q \models \varphi \).
  • \(\varphi = \bigwedge _{i \in I} \psi _i\): Since \(\bigwedge _{i \in I} \psi _i\in \textsf {Par}(\varphi _A,\varphi _B)\), by the definition of \(\textsf {Par}\), for each \(i \in I\) there are formulas \(\psi _A^i \in \varphi _A^{\Rightarrow },\psi _B^i \in \varphi _B^{\Rightarrow }\) such that \(\psi _i \in \textsf {Par}(\psi _A^i,\psi _B^i)\). Since \(p \models \psi _A\) and \(q \models \psi _B\), we have \(p \models \psi _A^i\) and \(q \models \psi _B^i\) for all \(i \in I\). By the IH, \(p \,||\, q \models \psi _i\) for all \(i \in I\). So \(p \,||\, q \models \bigwedge _{i\in I}\psi _i\).

  • \(\varphi = \langle \alpha \rangle \psi \): There are three possible cases, depending on which alternative in the definition of \(\textsf {Par}\) is used to derive that \(\langle \alpha \rangle \psi \in \textsf {Par}(\varphi _A,\varphi _B)\).
    • \(\exists \psi _C:\,\langle \alpha \rangle \psi _C \in \varphi _A^{\Rightarrow }\wedge \psi \in \textsf {Par}(\psi _C,\varphi _B)\). Since \( \langle \alpha \rangle \psi _C \in \varphi _A^{\Rightarrow }\) and \(p\models \varphi _A\), we have \(p \models \langle \alpha \rangle \psi _C\). So there is a process \(p'\) such that \(p{\mathop {\longrightarrow }\limits ^{\alpha }}p'\) and \(p' \models \psi _C\). Then \(p \,||\, q {\mathop {\longrightarrow }\limits ^{\alpha }}p' \,||\, q\). Moreover, by the IH, \(p' \,||\, q \models \psi \). Hence, \(p \,||\, q \models \langle \alpha \rangle \psi \).

    • \(\exists \psi _D:\,\langle \alpha \rangle \psi _D \in \varphi _B^{\Rightarrow }\wedge \psi \in \textsf {Par}(\varphi _A,\psi _D)\). The proof mirrors the previous case.

    • \(\exists c,d \in Act.\, \exists \psi _C,\psi _D: \,\gamma (c,d) = \alpha \wedge \langle c\rangle \psi _C \in \varphi _A^{\Rightarrow } \wedge \langle d\rangle \psi _D \in \varphi _B^{\Rightarrow } \wedge \psi \in \textsf {Par}(\psi _C,\psi _D)\). Since \(\langle c\rangle \psi _C \in \varphi _A^{\Rightarrow }\) and \(\langle d\rangle \psi _D \in \varphi _B^{\Rightarrow }\), we have \(p \models \langle c\rangle \psi _C\) and \(q \models \langle d\rangle \psi _D\). Hence there are processes \(p',q'\) such that \(p {\mathop {\longrightarrow }\limits ^{c}} p'\), \(p' \models \psi _C\), \(q {\mathop {\longrightarrow }\limits ^{d}} q'\), and \(q' \models \psi _D\). Since \(\gamma (c,d)=\alpha \), we have \(p \,||\, q {\mathop {\longrightarrow }\limits ^{\alpha }} p' \,||\, q'\). Moreover, since \(\psi \in \textsf {Par}(\psi _C,\psi _D)\), by the IH, \(p' \,||\, q'\models \psi \). Hence, \(p \,||\, q \models \langle \alpha \rangle \psi \).

  • \(\varphi = \langle {\hat{\tau }}\rangle \psi \): There are two possible cases:
    • \(\exists \psi _{C}: ~\langle {\hat{\tau }}\rangle \psi _{C} \in \varphi _A^{\Rightarrow } ~\wedge ~ \psi \in \textsf {Par}(\psi _C,\varphi _B)\): Since \(\langle {\hat{\tau }}\rangle \psi _C\in \varphi _A^\Rightarrow \), we have \(p \models \langle {\hat{\tau }}\rangle \psi _C\). This means that either \(p \models \psi _C\), or \(p {\mathop {\longrightarrow }\limits ^{\tau }} p' \wedge p' \models \psi _C\). In the first case, since \(p \models \psi _C\), \(q \models \varphi _B\), and \(\psi \in \textsf {Par}(\psi _C,\varphi _B)\), we have \(p \,||\, q \models \psi \), and hence \(p \,||\, q \models \langle {\hat{\tau }}\rangle \psi \). In the second case, by a similar line of reasoning we obtain \(p' \,||\, q \models \psi \), and since \(p {\mathop {\longrightarrow }\limits ^{\tau }} p'\), it follows that \(p \,||\, q \models \langle \tau \rangle \psi \). This obviously yields \(p \,||\, q \models \langle {\hat{\tau }}\rangle \psi \).

    • \(\exists \psi _{D}: ~\langle {\hat{\tau }}\rangle \psi _{D} \in \varphi _B^{\Rightarrow } ~\wedge ~ \psi \in \textsf {Par}(\varphi _A,\psi _D)\): proof mirrors one in the case above

  • \(\varphi = \langle \epsilon \rangle \psi \): By the definition of \(\textsf {Par}\), there are formulas \(\psi _C,\psi _D\) such that \(\langle \epsilon \rangle \psi _C \in \varphi _A^{\Rightarrow }\), \(\langle \epsilon \rangle \psi _D \in \varphi _B^{\Rightarrow }\), and \(\psi \in \textsf {Par}(\psi _C,\psi _D)\). Since \(\langle \epsilon \rangle \psi _C \in \varphi _A^{\Rightarrow }\), \(\langle \epsilon \rangle \psi _D \in \varphi _B^{\Rightarrow }\), and on the other hand \(p \models \varphi _A\) and \(q \models \varphi _B\), we also have \(p \models \langle \epsilon \rangle \psi _C\) and \(q \models \langle \epsilon \rangle \psi _D\). Then there are processes \(p',q'\) such that \(p {\mathop {\Longrightarrow }\limits ^{\epsilon }}p'\), \(p' \models \psi _C\), \(q {\mathop {\Longrightarrow }\limits ^{\epsilon }}q'\), and \(q' \models \psi _D\). So \(p \,||\, q {\mathop {\Longrightarrow }\limits ^{\epsilon }}p' \,||\, q'\). Moreover, since \(\psi \in \textsf {Par}(\psi _C,\psi _D)\), by the IH, \(p' \,||\, q' \models \psi \). Hence, \(p \,||\, q \models \langle \epsilon \rangle \psi \).

  • \(\varphi = \lnot \psi \): By the definition of \(\textsf {Par}\), for all formulas \(\varphi _C,\varphi _D\) such that \(\psi \in \textsf {Par}(\varphi _C,\varphi _D)\) we have \(\lnot \varphi _C \in \varphi _A^{\Rightarrow }\) or \(\lnot \varphi _D \in \varphi _B^{\Rightarrow }\). Since \(p \models \varphi _A\) and \( q \models \varphi _B\), this implies \(p \not \models \varphi _C \vee p \not \models \varphi _D\) for all \(\varphi _C,\varphi _D\) as above. Hence,
    $$\begin{aligned} \lnot \exists \varphi _C, \varphi _D:~p \models \varphi _C ~\wedge ~ q \models \varphi _D ~\wedge ~ \psi \in \textsf {Par}(\varphi _C,\varphi _D) \end{aligned}$$
    By the IH this entails \( p \,||\, q \not \models \psi \), and thus \( p \,||\, q \models \lnot \psi \). \(\square \)

The semantic nature of \(\textsf {Par}\) hinders the formulation of congruence requirements. We therefore restrict (syntactically) the set from which the witness formulas \(\varphi _A\) and \(\varphi _B\) from Proposition 6 can be taken. To this end, we define a set \(\textsf {Comp}^{+}(\varphi )\) of formulas into which formula \(\varphi \) may be syntactically decomposed.

Definition 2

Given a formula \(\varphi \), the set \(\textsf {Comp}^{+}(\varphi )\) of formulas is defined by:
  • \(\textsf {Comp}^{+}(\bigwedge _{i \in I} \varphi _i) ~=~ \{ \bigwedge _{i \in I} \varphi _i' ~|~ \varphi _i' \in \textsf {Comp}^{+}(\varphi _i)\}\)

  • \(\textsf {Comp}^{+}(\langle \alpha \rangle \varphi ) ~=~ \textsf {Comp}^{+}(\varphi ) ~\cup ~ \{ \langle a \rangle \varphi ' ~|~ \varphi ' \in \textsf {Comp}^{+}(\varphi )\}\)

    \(\cup ~ \{ \langle a \rangle \varphi ' ~|~ (\exists b \in Act. \gamma (a,b)=\alpha ) \,\wedge \, \varphi ' \in \textsf {Comp}^{+}(\varphi )\} \)

  • \(\textsf {Comp}^{+}(\langle {\hat{\tau }}\rangle \varphi ) ~=~ \textsf {Comp}^{+}(\varphi ) ~\cup ~ \{ \langle {\hat{\tau }}\rangle \varphi ' ~|~ \varphi ' \in \textsf {Comp}^{+}(\varphi )\}\)

  • \(\textsf {Comp}^{+}(\langle \epsilon \rangle \varphi ) ~=~ \{\langle \epsilon \rangle \varphi ' ~|~ \varphi ' \in \textsf {Comp}^{+}(\varphi ) \} \)

  • \(\textsf {Comp}^{+}(\lnot \varphi ) ~=~ \{ \bigwedge _{i \in I} \lnot \varphi _i ~|~ \varphi _i \in \textsf {Comp}^{+}(\varphi )\}\)

  • \(\textsf {Comp}^{+}(\emptyset ) ~=~\{\emptyset \} \)

  • \(\textsf {Comp}^{+}({\widetilde{\emptyset }}) ~=~\{{\widetilde{\emptyset }}\} \)

The proposition below states that the witness formulas from Proposition 6 can be always found within the set \(\textsf {Comp}^{+}\) of the formula in question.

Proposition 7

For all processes pq and formulas \(\varphi \),
$$\begin{aligned} p \,||\, q \models \varphi ~~\Longleftrightarrow ~~ \exists \varphi _A,\varphi _B \in \textsf {Comp}^{+}(\varphi ):\,\, p \models \varphi _A ~\wedge ~ q \models \varphi _B ~\wedge ~ \varphi \in \textsf {Par}(\varphi _A,\varphi _B) \end{aligned}$$

Proof

The implication from right to left is a specific instance of Proposition 6. To show that the converse implication holds, one needs to observe that all the witness formulas constructed in the proof of the weaker statement from Proposition 6 meet the syntactic requirements for being included in \(\textsf {Comp}^{+}(\varphi )\), provided that the simpler witness formulas in the IH belong to sets \(\textsf {Comp}^{+}\) of certain subformulas of \(\varphi \). Below, we analyse the specific cases in the proof of Proposition 6.
  • \(\varphi = \bigwedge _{i \in I} \psi _i\): By the IH, \(\psi ^i_A,\psi ^i_B \in \textsf {Comp}^{+}(\psi _i)\) for all \(i \in I\), so by the definition of \(\textsf {Comp}^{+}\) we obtain \(\bigwedge _{i \in I}\psi ^i_A,\bigwedge _{i \in I}\psi ^i_B \in \textsf {Comp}^{+}(\bigwedge _{i \in I}\psi _i)\)

  • \(\varphi =\langle \alpha \rangle \psi \): there are three possible cases:
    • \(p {\mathop {\longrightarrow }\limits ^{\alpha }} p_1\) and \(p_1 \,||\, q \models \psi \): By the IH, \(\psi _1,\psi _q \in \textsf {Comp}^{+}(\psi )\), so by the definition of \(\textsf {Comp}^{+}\), \(\langle \alpha \rangle \psi _1,\psi _q \in \textsf {Comp}^{+}(\langle \alpha \rangle \psi )\).

    • \(q {\mathop {\longrightarrow }\limits ^{\alpha }} q_1\) and \(p \,||\, q_1 \models \psi \): The proof is very similar to the previous case.

    • \(p {\mathop {\longrightarrow }\limits ^{b}} r\), \(q {\mathop {\longrightarrow }\limits ^{c}} s\), \(\gamma (b,c)=\alpha \), and \(r \,||\, s \models \psi \): By the IH, \(\psi _r,\psi _s \in \textsf {Comp}^{+}(\psi )\). Since \(\gamma (b,c) = \alpha \), by the definition of \(\textsf {Comp}^{+}\) (third component of the sum), \(\langle b\rangle \psi _r,\langle c\rangle \psi _s \in \textsf {Comp}^{+}(\langle \alpha \rangle \psi )\).

  • \(\varphi = \langle {\hat{\tau }}\rangle \psi \): There are two possible cases:
    • \(p \,||\, q \models \psi \): By the IH, \(\psi _p,\psi _q \in \textsf {Comp}^{+}(\psi )\); hence, by the definition of \(\textsf {Comp}^{+}\), \(\langle {\hat{\tau }}\rangle \psi _p, \psi _q \in \textsf {Comp}^{+}(\langle {\hat{\tau }}\rangle \psi )\).

    • \(p \,||\, q \models \langle {\hat{\tau }}\rangle \psi \):
      • \(p {\mathop {\longrightarrow }\limits ^{\tau }} p_1\) and \(p_1 \,||\, q \models \psi \): By the IH, \(\psi _1,\psi _q \in \textsf {Comp}^{+}(\psi )\); hence, by the definition of \(\textsf {Comp}^{+}\), \(\langle {\hat{\tau }}\rangle \psi _1,\psi _q \in \textsf {Comp}^{+}( \langle {\hat{\tau }}\rangle \psi )\).

      • \(q {\mathop {\longrightarrow }\limits ^{\tau }} q_1\) and \(p \,||\, q_1 \models \psi \): The proof is similar to the previous case.

  • \(\varphi = \langle \epsilon \rangle \psi \): By the IH, \(\psi _1,\psi _2 \in \textsf {Comp}^{+}(\psi )\); hence, by the definition of \(\textsf {Comp}^{+}\) we obtain \(\langle \epsilon \rangle \psi _1,\langle \epsilon \rangle \psi _2 \in \textsf {Comp}^{+}(\langle \epsilon \rangle \psi )\).

  • \(\varphi = \lnot \psi \): Following the corresponding case in the proof of Proposition 6 with the IH now strengthened, we obtain that \(p || q \models \lnot \psi \) is equivalent to:
    We can thus modify the definitions of \({{\mathcal {A}}}\), \({{\mathcal {B}}}\), \(\varPsi _{{\mathcal {A}}}\), and \(\varPsi _{{\mathcal {B}}}\) as follows:

    \({{\mathcal {A}}}^+ ~=~ \{ \psi _A \in \textsf {Comp}^{+}(\psi ) ~|~ \exists \psi _B \in \textsf {Comp}^{+}(\psi ): ~\psi \in \textsf {Par}(\psi _A,\psi _B) ~\wedge ~ p \not \models \psi _A \}\)

    \({{\mathcal {B}}}^+ ~=~ \{ \psi _B \in \textsf {Comp}^{+}(\psi ) ~|~ \exists \psi _A \in \textsf {Comp}^{+}(\psi ): ~\psi \in \textsf {Par}(\psi _A,\psi _B) ~\wedge ~ q \not \models \psi _B \}\)

    \(\varPsi ^+_{{\mathcal {A}}} ~=~ \bigwedge _{\psi _A \in {{\mathcal {A}}}^+} \lnot \psi _A\)

    \(\varPsi ^+_{{\mathcal {B}}} ~=~ \bigwedge _{\psi _B \in {{\mathcal {B}}}^+} \lnot \psi _B\)

    Since all formulas in \({{\mathcal {A}}}^+\) and \({{\mathcal {B}}}^+\) belong to \(\textsf {Comp}^{+}(\psi )\), from the definition of \(\textsf {Comp}^{+}\) we obtain \(\varPsi ^+_{{\mathcal {A}}},\varPsi ^+_{{\mathcal {B}}} \in \textsf {Comp}^{+}(\lnot \psi )\).

  • \(\varphi = \emptyset \) and \(\varphi ={\widetilde{\emptyset }}\): Immediate. \(\square \)

Theorem 6

If \({{\mathcal {O}}}\subseteq { HML}_\tau \cup \{\emptyset ,{\widetilde{\emptyset }},\langle {\hat{\tau }}\rangle \}\) satisfies
$$\begin{aligned} \textsc {(par)} ~~~~~ \varphi \in {{\mathcal {O}}}\,\implies \, \textsf {Comp}^{+}(\varphi ) \subseteq {\overline{{{\mathcal {O}}}}} \end{aligned}$$
then \(\sim _{{\mathcal {O}}}\) is a congruence with respect to the parallel composition operator.

Proof

Let \({{\mathcal {O}}}\subseteq { HML}_\tau \cup \{\emptyset ,{\widetilde{\emptyset }},\langle {\hat{\tau }}\rangle \}\) satisfy \(\textsc {(par)}\), and \(p \sim _{{\mathcal {O}}}p'\) and \(q \sim _{{\mathcal {O}}}q'\). For all \(\varphi \in {{\mathcal {O}}}\): \(p \,||\, q \models \varphi ~\Longleftrightarrow \) (Proposition 7) \(\exists \varphi _A,\varphi _B \in \textsf {Comp}^{+}(\varphi ): p \models \varphi _A \wedge q \models \varphi _B \wedge \varphi \in \textsf {Par}(\varphi _A,\varphi _B)\)\(\Longleftrightarrow \) (\(\textsc {(par)}\), \(p \sim _{{\mathcal {O}}}p'\), \(q \sim _{{\mathcal {O}}}q'\)) \(\exists \varphi _A,\varphi _B \in \textsf {Comp}^{+}(\varphi ): p' \models \varphi _A \wedge q' \models \varphi _B \wedge \varphi \in \textsf {Par}(\varphi _A,\varphi _B) \Longleftrightarrow \) (Proposition 7) \(p' \,||\, q' \models \varphi \)\(\square \)

The only modal characterizations from Sect. 2 that violate (par) are \({{\mathcal {O}}}_{CT}\), \({{\mathcal {O}}}_{WCT}\), \({{\mathcal {O}}}_{ BB}\), and \({{\mathcal {O}}}_{ RBB}\). However, the alternative characterizations \({\widehat{{{\mathcal {O}}}}}_{CT}\), \({\widehat{{{\mathcal {O}}}}}_{WCT}\), \({\widehat{{{\mathcal {O}}}}}_{ BB}\), and \({\widehat{{{\mathcal {O}}}}}_{ RBB}\) all meet (par).

Corollary 10

\(\sim _{ T}\), \(\sim _{ CT}\), \(\sim _{ F}\), \(\sim _{ R}\), \(\sim _{ FT}\), \(\sim _{ RT}\), \(\sim _{ I\!F}\), \(\sim _{ P\!F}\), \(\sim _{ nS}\) (for \(n\ge 1\)), \(\sim _{ RS}\), and \(\sim _{ B}\) are congruences for the parallel composition operator.

Corollary 11

\(\sim _{ WT}\), \(\sim _{ WCT}\), \(\sim _{ WF}\), \(\sim _{ WB}\), \(\sim _{ RWB}\), \(\sim _{ DB}\), \(\sim _{ RDB}\), \(\sim _{ \eta B}\), \(\sim _{ R\eta B}\), \(\sim _{ BB}\), and \(\sim _{ RBB}\) are congruences for the parallel composition operator.

4 Conclusions

So far, in the literature, congruence formats have been approached from the angle of the process semantics. Carving out such a congruence format for a particular semantics is very hard work, and there is an overwhelming number of weak semantics (see [16]). This paper offers an entirely different perspective by presenting, for a number of process operators from the literature, general syntactic requirements that guarantee congruence of process equivalences defined by means of a modal characterization. To the best of our knowledge it is the first such attempt. Our requirements are sufficient, but by no means necessary; we aimed at clear and comprehensible rather than slightly relaxed but more complicated requirements. We covered the concrete semantics in [17]; an exhaustive investigation in how far modal characterizations of the 155 weak semantics in [16] satisfy the requirements we formulated remains as future research. In particular, we have focused on what are called unstable weak semantics in the spectrum from [16]. Weak semantics that are sensitive to stability, meaning the absence of a \(\tau \)-transition, or to divergence, meaning the presence of an infinite sequence of \(\tau \)-transitions, tend to have better congruence properties, with regard to the aforementioned priority operator as well as recursive operators. Checking our syntactic congruence requirements with respect to stability-preserving and divergence-respecting weak semantics would be interesting future work.

A key question that requires further research is whether reasonable requirements on modal characterizations can be formulated for other widely used operators such as recursive operators and the priority operator. In particular, the unary priority operator \(\theta \) assumes a partial order < on actions. It allows execution of an action by its argument only if no action with a higher priority is enabled:There is no operator \({ cut}_\theta \) for which condition (cut-2) from Proposition 1 holds. Namely, let \(\alpha < \beta \). Whether a subformula \(\langle \alpha \rangle \varphi '\) of a formula \(\varphi \) can be replaced by \(\textsf {F}\) depends on whether this subformula is checked at a point where a \(\beta \)-transition is possible. In contrast to branching bisimulation semantics, stability-respecting branching bisimulation semantics is a congruence for \(\theta \). Hence the modal characterization for the latter semantics (see e.g. [11]) may provide inspiration on the formulation of requirements with regard to \(\theta \). Another interesting candidate is the action refinement operator, which allows to refine a single action into process behavior. It is a congruence for rooted branching bisimulation semantics but not for rooted \(\eta \)-bisimulation semantics (see e.g. [10]).

By extending the results in this paper to Hennessy–Milner logic with recursion or the \(\mu \)-calculus, it could be attempted to combine our work with existing results on characteristic formulas [2]. In that setting, instead of modal language properties, one could focus on compositionality of a single characteristic formula.

More generally, the current paper could serve as a starting point for developing a theory that allows one to obtain conditions on modal characterisations from the transition rules for an operator in a systematic way.

Notes

References

  1. 1.
    Aceto, L., Fokkink, W.J., Verhoef, C.: Structural operational semantics. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 197–292. Elsevier, Amsterdam (2001)CrossRefGoogle Scholar
  2. 2.
    Aceto, L., Ingolfsdottir, A., Sack, J.: Characteristic formulae for fixed-point semantics: a general framework. In Proc. EXPRESS’09. EPTCS 8, 1–15 (2009)CrossRefGoogle Scholar
  3. 3.
    Baeten, J.C.M., Bergstra, J.A.: Global renaming operators in concrete process algebra. Inf. Comput. 78(3), 205–245 (1988)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: On the consistency of Koomen’s fair abstraction rule. Theoret. Comput. Sci. 51(1/2), 129–176 (1987)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoret. Comput. Sci. 37, 77–121 (1985)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)CrossRefGoogle Scholar
  7. 7.
    Bloom, B., Fokkink, W.J., van Glabbeek, R.J.: Precongruence formats for decorated trace semantics. ACM Trans. Comput. Logic 5, 26–78 (2004)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Fokkink, W.J.: Introduction to Process Algebra. Springer, New York (2000)CrossRefGoogle Scholar
  9. 9.
    Fokkink, W.J., van Glabbeek, R.J., de Wind, P.: Compositionality of Hennessy–Milner logic by structural operational semantics. Theoret. Comput. Sci. 354(3), 421–440 (2006)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Fokkink, W.J., van Glabbeek, R.J., de Wind, P.: Divide and congruence: from decomposition of modal formulas to preservation of branching and \(\eta \)-bisimilarity. Inf. Comput. 214, 59–85 (2012)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Fokkink, W.J., van Glabbeek, R.J., Luttik, B.: Divide and congruence III: stability & divergence. In Proc. CONCUR’17, LIPIcs 85, pp. 15:1–15:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)Google Scholar
  12. 12.
    Gazda, M., Fokkink, W.J.: Congruence from the operator’s point of view: compositionality requirements on process semantics. In Proc. SOS’10. EPTCS 32, 15–25 (2010)CrossRefGoogle Scholar
  13. 13.
    Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100, 202–260 (1992)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Hennessy, M., Milner, R.: Algebraic laws for non-determinism and concurrency. J. ACM 32, 137–161 (1985)CrossRefGoogle Scholar
  15. 15.
    Larsen, K.G., Liu, X.: Compositionality through an operational semantics of contexts. J. Logic Comput. 1(6), 761–795 (1991)MathSciNetCrossRefGoogle Scholar
  16. 16.
    van Glabbeek, R.J.: The linear time—branching time spectrum II: the semantics of sequential systems with silent moves. In Proc. CONCUR’93, LNCS 715, pp. 66–81. Springer (1993)Google Scholar
  17. 17.
    van Glabbeek, R.J.: The linear time—branching time spectrum I: the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier (2001)Google Scholar
  18. 18.
    Verhoef, C.: A congruence theorem for structured operational semantics with predicates and negative premises. Nordic J Comput. 2, 274–302 (1995)MathSciNetzbMATHGoogle Scholar

Copyright information

© The Author(s) 2019

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.University of LeicesterLeicesterUK
  2. 2.Vrije Universiteit AmsterdamAmsterdamThe Netherlands
  3. 3.Google ZürichZürichSwitzerland

Personalised recommendations