Logical Characterisation of Parameterised Bisimulations

Abstract

We explore the relationship between bisimulations and logic. The link between them is formed by logical characterisations, which have been given for well-known bisimulation equivalences and preorders. Parameterised bisimulations allow us to incorporate notions of abstraction or efficiency into behavioural equivalences. This generalised framework of parameterised bisimulations is used to develop a parameterised logical characterisation, thereby, unifying the existing logical characterisations as well as paving the way for characterisation of novel bisimulations. Methods for generating distinguishing formulae and characteristic formulae in the parameterised logic are also discussed.

1 Introduction

Bisimulation checking and model checking are among the two major approaches to the verification of concurrent processes. Both model behaviour using labelled transition systems but differ in specification. Bisimulation checking expresses specification also as a labelled transition system, whereas model checking expresses specification as a collection of logical formulas. Both have their advantages. Model checking allows for partial specifications and its refinements by adding more properties. Bisimulation checking gives us modularity as it is often closed under most of the process constructors [9]. Therefore, both approaches have their own applications.

But there is an interesting connection between them - formalized as logical characterisations - one of the most important being Hennessy-Milner logic (HML) [16], which gives a modal logic characterisation for strong bisimulation. Any two processes are strongly bisimilar if and only if they satisfy the same set of HML formulae¹. Consequently, for any two non-bisimilar processes, there must exist a distinguishing formula which is satisfied by exactly one of the given processes, and can be very useful for debugging.

Sometimes, it is possible to construct a single formula capable of distinguishing a process from every other non-bisimilar process. Known as characteristic formula, it facilitates the reduction of bisimulation checking to model checking, which may yield efficient algorithms for deciding behavioural preorders [10]. The existence of a characteristic formula is therefore, central to the study of logical characterisations [14].

The importance of logical characterisations can be gauged from the work done towards showing their existence for many other bisimulation equivalences besides strong bisimulation, e.g., timed bisimulations [19], probabilistic bisimulations and preorders such as prebisimulation preorder [27], efficiency preorders [17], contravariant simulation [1], etc. In this paper, we develop a logical characterisation of parameterised bisimulations. As shown in [4], various bisimulation relations can be expressed as instances of parameterised bisimulation. By working in a general framework of parameterised bisimulations, we achieve two goals. Firstly, we unify the results on obtaining the logical characterisations for different bisimulation relations. Secondly, this gives us a systematic way of obtaining a logical characterisation of any novel bisimulation relation, which may be expressed as an instance of parameterised bisimulation. As one would expect, the logical characterisation of the parameterised bisimulations should also depend on the same parameters. Since our logic generalises HML, we refer to it as parameterised Hennessy-Milner logic.

The contributions of this paper may be summarized as follows:

• We propose parameterised HML, in Sect. 3, and show that it is a logical characterisation of all bisimulation equivalences and preorders which can be expressed in the framework of parameterised bisimulations.

• We study the conditions required to ensure that the distinguishing formula is always finite. We also give procedures for model checking and generating distinguishing formulae.

• We extend our logical characterisation with fixed point operators, in Sect. 4, which allows us to derive the characteristic formula for any finite-state process, and possibly some infinite-state systems, using suitable abstractions.

2 Background

To model process behaviours, both bisimulation and model checking use labelled transition systems, which is one of the most widely used models of computation.

Definition 1

A labelled transition system (LTS) $\mathfrak {L}$ is a triple ${{\langle \mathcal {P}, {\mathcal Act}, \longrightarrow \rangle }}$, where $\mathcal {P}$ is a set of process states or processes, ${\mathcal Act}$ is a set of actions and $\longrightarrow \ \subseteq \mathcal {P} \times {\mathcal Act} \times \mathcal {P}$ is the transition relation. We use $p \overset{a}{\longrightarrow } q$ to denote $(p, a, q) \in \longrightarrow$.

2.1 Parameterised Bisimulations

The origin of bisimulations can be traced back to logic [24], where it serves an important role in establishing modal logic as a fragment of first order logic [30]. It was first proposed in [7], as relations which preserve satisfiability of modal logic formulas. Its discovery in computer science and fixed point characterisation is attributed to [23] and is central to Milner’s theory of CCS [21]. Being the finest behavioural equivalence [31], its importance in the theory of verification is undeniable.

One can think of interesting behavioural relations, which may relate one process with another behaviourally equivalent but more efficient process. Efficiency need not be only in terms of time, it may also refer to other quantitative measures like probability, energy, etc. One approach to defining these relations is by incorporating efficiency into bisimulation, which is the idea behind efficiency preorder [5] or timed prebisimulation [15]. The key idea behind them is to allow an action to be matched with a functionally equivalent but more efficient one. The same approach is used to incorporate abstraction into bisimulation, e.g. weak bisimulation, where an action can be matched with another non-identical but equivalent under the given abstraction. These bisimulations can be unified under the general framework of parameterised bisimulations, which allow the relations over actions to be parameters in the definition of bisimulation. The parameter relations incorporates the desired notion of efficiency or abstraction.

Definition 2

[4]. Let $\mathcal {P}$ be the set of processes and $\rho$ and $\sigma$ be binary relations on ${\mathcal Act}$. A binary relation $R \subseteq \mathcal {P} \times \mathcal {P}$ is a $(\rho ,\sigma )$ -bisimulation if $p\mathrel {R} q$ implies the following conditions for all $a, b\in {\mathcal Act}$.

$$\begin{aligned} p \overset{a}{\longrightarrow } p' \Rightarrow \exists b, q'[ a \mathbin {\rho } b \wedge q \overset{b}{\longrightarrow } q' \wedge p'\mathrel {R}q'] \end{aligned}$$

(1)

$$\begin{aligned} q \overset{b}{\longrightarrow } q' \Rightarrow \exists a, p'[ a \mathbin {\sigma } b \wedge p \overset{a}{\longrightarrow } p'\wedge p'\mathrel {R}q'] \end{aligned}$$

(2)

The largest $(\rho ,\sigma )$-bisimulation, denoted $\mathrel {\underline{\Box }}_{(\rho , \sigma )}$, is called $(\rho ,\sigma )$ -bisimilarity.

This generalization captures a number of useful bisimulations. Strong bisimulation is obtained by simply setting $\rho$ and $\sigma$ as identity relation over actions, ${\mathcal Id}_{\mathcal Act}$. Other interesting relations are defined by exploiting semantic relationships between actions. For example, in Timed LTS, a special class of LTS with labels from the set ${\mathcal Act}\mathbin {\cup }\mathbb {R}_{\ge 0}$, one may differ in matching delay actions $d \in \mathbb {R}_{\ge 0}$. We obtain time-abstracted bisimulation [20] by not distinguishing between delay quantities. It is an instance of a parameterised bisimulation where $\rho = \sigma = {\mathcal Id}_{\mathcal Act} \cup (\mathbb {R}_{\ge 0} \mathbin {\times } \mathbb {R}_{\ge 0})$. We can also capture delay based efficiency, to define timed prebisimulation [15], where a delay d can be matched by a faster delay $d' \le d$, by setting $\rho = \sigma = {\mathcal Id}_{\mathcal Act}\mathbin {\cup }\le _{\mathbb R}$.

Another class of interesting relations emerge when we model internal actions, in the LTS, as transitions labeled with $\tau$. These $\tau$-actions cannot be observed, and the behavioural equivalence must ignore them. This behavioural equivalence is captured by weak bisimulation [16]. One may also view $\tau$ as a measure of internal activity, to define efficiency preorders [5]. These relations can also be expressed as an instance of parameterised bisimulations, which is described in Sect. 5.

We will obtain the logical characterisations for these bisimilarities, by developing results for parameterised bisimilarities. However, we will limit ourselves to parameterised bisimilarities which become preorders (or equivalences), by placing suitable restrictions on the underlying relations over actions.

Fixed Point Characterisation: The fixed point characterisation of $(\rho ,\sigma )$-bisimilarity, over the complete lattice of binary relations on $\mathcal {P}$ under the $\subseteq$ ordering serves an important role as the starting point for the derivation of characteristic formulae.

Lemma 1

The relation $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ over processes $\mathcal {P}$ may be expressed as the greatest fixed point of the monotonic function $\mathscr {F}_{(\rho ,\sigma )}: \mathbbm {2}^{\mathcal {P} \times \mathcal {P}} \rightarrow \mathbbm {2}^{\mathcal {P} \times \mathcal {P}}$, defined as

$$ \begin{array}{lcll} \mathscr {F}_{(\rho ,\sigma )}(R) &{}=&{} \{ (p,q)\ | &{} [\forall a,p': p \overset{a}{\longrightarrow } p' \Rightarrow \exists b, q'[ a \mathrel {\rho } b \wedge q \overset{b}{\longrightarrow } q' \wedge p'\mathrel {R}q']] \wedge \\ &{} &{} &{} [\forall b,q': q \overset{b}{\longrightarrow } q' \Rightarrow \exists a, p'[ a \mathrel {\sigma } b \wedge p \overset{a}{\longrightarrow } p' \wedge p'\mathrel {R}q']] \} \end{array} $$

One approach to computing the greatest fixed point in a lattice, is to take the top element (the universal relation in our case), and keep on applying the function until it reaches the fixed point. Let $\mathbb {U}$ denote the universal relation, then the $i^{th}$ approximant of $(\rho ,\sigma )$-bisimilarity is defined as $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}} = \mathscr {F}^i_{(\rho ,\sigma )}(\mathbb {U})$. In general, the intersection of all the approximants, $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} = \bigcap _{i \in \mathbb {N}} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}$, will contain the greatest fixed point, $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$, and $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} = \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ when $\mathscr {F}^i_{(\rho ,\sigma )}$ is co-continuous [13].

Lemma 2

[4]. For any $i \in \mathbb {N}$, the i-th approximant, $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}$, as well as $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }}$ and $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ are preorders iff both $\rho$ and $\sigma$ are preorders. Moreover, they become an equivalence iff we also have $\rho = \sigma ^{-1}$.    $\square$

The proof for $(\rho ,\sigma )$-bisimilarity, given in [4], can be generalised for approximants using induction.

Abstracted LTS: The notion of an abstracted LTS allows us to extend our results to some infinite-state systems.

Definition 3

Given a set $S \subseteq \mathcal {P}$ and a preorder $\le \subseteq \mathcal {P} \times \mathcal {P}$, we define an initial set $S^\mathfrak {i}$ and a terminal set $S^\mathfrak {t}$ as

where $s < s'$ iff $s \le s'$ and $s \not = s'$. The set S is closed if for every $s \in S$, there exists an $s' \in S^\mathfrak {i}$ and $s'' \in S^\mathfrak {t}$ such that $s' \le s \le s''$.

Let $p \overset{a}{\longrightarrow } p_1$ and $p \overset{b}{\longrightarrow } p_2$ be two transitions such that $a \mathrel {\rho } b$ and $p_1 \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p_2$. Then matching the transition $p \overset{b}{\longrightarrow } p_2$ with $q \overset{c}{\longrightarrow } q'$, where $b \mathrel {\rho } c$ and $p_2 \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'$ holds, also matches $p \overset{a}{\longrightarrow } p_1$ due to transitivity of $\rho$ and $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$. Effectively, satisfying the condition (1) in Definition 2 only requires matching transitions to the terminal states under $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ ordering, $\{p'\ |\ p \overset{b}{\longrightarrow } p' \wedge a \mathrel {\rho } b\ \}^\mathfrak {t}$, provided it is a closed set. Similarly for satisfying the condition (2), i.e. matching a transition of q, it suffices to only look at transitions to the initial states, $\{p'\ |\ p \overset{a}{\longrightarrow } p' \wedge a \mathrel {\sigma } b \}^\mathfrak {i}$. Therefore, we define an abstracted LTS which retains only the relevant states.

Definition 4

Let $\mathfrak {L} ={{\langle \mathcal {P}, {\mathcal Act}, \longrightarrow \rangle }}$ be an LTS. For any $p \in \mathcal {P}$ and $a \in {\mathcal Act}$, let , and . Then an LTS abstracted with respect to process $p\in \mathcal {P}$ is defined as $\mathfrak {L}^\dagger _p ={{\langle Reach(p), {\mathcal Act}, \longrightarrow ^\dagger _p \rangle }}$ where

$$ Reach (p) = \{p\} \cup \bigcup _{p' \in TI(p)}Reach(p') $$

the terminal and initial sets are created with respect to $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ ordering and the transition relation $\longrightarrow ^\dagger _p$ is the restriction of $\longrightarrow$ to Reach(p).

Since $\mathfrak {L}$ and $\mathfrak {L}^\dagger _p$ have common elements, we will subscript the process state with the LTS when there is ambiguity. The following lemma formalizes this intuitive property of preservation of bisimilarity by the abstracted LTS.

Lemma 3

Let $\mathfrak {L}$ be an LTS such that the sets $\{p' \mid \exists b[p \overset{b}{\longrightarrow } p'\wedge a \mathbin {\rho } b]\}$ and $\{ p'\mid \exists [p \overset{b}{\longrightarrow } p' \wedge b\mathbin {\sigma } a]\}$ are always closed, for any state p and label a. Then, for any state p, we have $p_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p_{\mathfrak {L}^\dagger _p}$ as well as $p_{\mathfrak {L}^\dagger _p} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p_\mathfrak {L}$.

Proof

A state q is in $\mathfrak {L}$ is also in $\mathfrak {L}^\dagger _p$ iff $q_\mathfrak {L} \in Reach(p_\mathfrak {L})$. Let $R = \{(q_\mathfrak {L},q'_{\mathfrak {L}^\dagger _p}) \mid q_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'_\mathfrak {L} \wedge q'_\mathfrak {L} \in Reach(p_\mathfrak {L}) \}$.

Claim. The relation R is a $(\rho ,\sigma )$-bisimulation.

Consider an arbitrary $(q_\mathfrak {L},q'_{\mathfrak {L}^\dagger _p}) \in R$. Since $q_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'_\mathfrak {L}$, if $q_\mathfrak {L} \overset{a}{\longrightarrow } r_\mathfrak {L}$, then there must be some b, $r'$ such that $q'_\mathfrak {L} \overset{b}{\longrightarrow } r'_\mathfrak {L}$ with $a \mathrel {\rho } b$ and $r_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} r'_\mathfrak {L}$. Since the set $\{s \mid q \overset{b}{\longrightarrow } s\wedge a \mathrel {\rho } b\}$ is closed, there must be some $r''_\mathfrak {L} \in \{s \mid q \overset{b}{\longrightarrow } s\wedge a \mathrel {\rho } b\}^\mathfrak {t}$ such that $r'_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} r''_\mathfrak {L}$. Since $q'_\mathfrak {L} \in Reach(p_\mathfrak {L})$, by recursive definition of $Reach(p_\mathfrak {L})$, we will also have $r''_\mathfrak {L} \in Reach(p_\mathfrak {L})$. Hence, by definition of R, we will have $(r'_{\mathfrak {L}_p}, r''_{\mathfrak {L}^\dagger _p}) \in R$.

Conversely, for any $q'_{\mathfrak {L}^\dagger _p} \overset{b}{\longrightarrow } r'_{\mathfrak {L}^\dagger _p}$, since $\mathfrak {L}^\dagger _p$ can be embedded into $\mathfrak {L}$, we will also have $q'_\mathfrak {L} \overset{b}{\longrightarrow } r'_\mathfrak {L}$. By definition of R, $q_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'_\mathfrak {L}$, hence there must be some a, r such that $q_\mathfrak {L} \overset{a}{\longrightarrow } r_\mathfrak {L}$ with $a \mathbin {\sigma } b$ and $r_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} r'_\mathfrak {L}$. Clearly, $r'_\mathfrak {L} \in Reach(p_\mathfrak {L})$, since it is in $\mathfrak {L}^\dagger _p$, and hence $(r_{\mathfrak {L}_p}, r'_{\mathfrak {L}^\dagger _p}) \in R$.

By a symmetric argument, we can show that the relation $R' = \{(q'_{\mathfrak {L}^\dagger _p},q_\mathfrak {L}) \mid q'_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q_\mathfrak {L} \wedge q'_\mathfrak {L} \in Reach(p_\mathfrak {L}) \}$ is also a $(\rho ,\sigma )$-bisimulation. Since $p_\mathfrak {L} \in Reach(p_\mathfrak {L})$ and $p_\mathfrak {L} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p_\mathfrak {L}$, we will have $(r_{\mathfrak {L}_p}, p_{\mathfrak {L}^\dagger _p}) \in R$ and $(p_{\mathfrak {L}^\dagger _p},p_{\mathfrak {L}_p} ) \in R'$.

   $\square$

An abstracted LTS may help in reducing an infinite-state system to a finite one. In some cases, it can be obtained without computing the bisimilarity relation. An example would be Timed Prebisimulation in Timed Automata [26].

3 Parameterised Hennessy-Milner Logic

Logical characterisation gives an effective syntax for describing distinguishing behaviour, which differentiates the implementation from the specification with respect to the behavioural preorder, as the distinguishing formula. For strong bisimilarity, Hennessy-Milner Logic (HML) with the possibility modality $\langle {a}\rangle$ and the necessity modality [a], for every observation $a \in {\mathcal Act}$, suffice. But when we have a more general notion of functional equivalence, same must also be incorporated in our modalities. For that, we look closely at how these modalities describe distinguishing behaviour.

Suppose distinguishing behaviour arises because the implementation can give an observation a, leading to behaviour described by some formula $\varphi$. Since it is not allowed by the specification, there will be no observation b, such that $a \mathrel {\rho } b$, leading to a state satisfying $\varphi$. We can describe this using the modality ${\langle a\rangle }^{\rho }$.

Conversely, distinguishing behaviour may arise as the specification has an observation a, leading to behaviour described by some formula $\varphi$, but there is no functionally equivalent observation in the implementation leading to the matching behaviour. That is, for every b, such that $b \mathrel {\sigma } a$, the implementation does not yield the behaviour $\varphi$. This can be described using the modality ${[a]^{\sigma ^{-1}}}$.

Hence, we propose the following as logical characterisation,

Definition 5

The syntax of the logic $\mathcal {L}_{(\rho ,\sigma )}$ is given by the following BNF

$$ \varphi \ :=\ \top \ |\ \bot \ |\ {\langle a\rangle }^{\rho }\varphi \ |\ [a]^{\sigma ^{-1}}\varphi \ |\ \varphi _1 \wedge \varphi _2\ |\ \varphi _1 \vee \varphi _2 $$

where $a \in {\mathcal Act}$. The semantics of $\varphi \in \mathcal {L}_{(\rho ,\sigma )}$ is inductively defined as

$$ \begin{array}{lclclcl} ||{\top }||^\mathcal {P} &{}=&{} \mathcal {P} &{} &{} ||{\varphi _1 \vee \varphi _2}||^\mathcal {P} &{}=&{} ||{\varphi _1}||^\mathcal {P} \cup ||{\varphi _2}||^\mathcal {P} \\ ||{\bot }||^\mathcal {P} &{}=&{} \emptyset &{} &{} ||{\varphi _1 \wedge \varphi _2}||^\mathcal {P} &{}=&{} ||{\varphi _1}||^\mathcal {P} \cap ||{\varphi _2}||^\mathcal {P}\\ \end{array} $$

$$ \begin{array}{lcl} ||{{\langle a\rangle }^{\rho }\varphi }||^\mathcal {P} &{}=&{} \{p\ |\ \exists b,p'[ a \rho b \wedge p \overset{b}{\longrightarrow } p' \wedge p' \in ||{\varphi }||^\mathcal {P}] \} \\ ||{{[a]^{\sigma ^{-1}}}\varphi }||^\mathcal {P} &{}=&{} \{ p\ |\ \forall b,p'[ b \sigma a \wedge p \overset{b}{\longrightarrow } p' \Rightarrow p' \in ||{\varphi }||^\mathcal {P}]\} \\ \end{array} $$

These definitions can be seen as a natural generalization of those given for HML and observational HML. A process p satisfies a formula $\varphi \in \mathcal {L}_{(\rho ,\sigma )}$, denoted $p \vDash \varphi$, iff $p \in ||{\varphi }||^\mathcal {P}$. In general, this logic is not closed under complementation. However, when $\rho = \sigma ^{-1}$, the two operators ${\langle \ \rangle }^{\rho }$ and $[\ ]^{\sigma ^{-1}}$ will become dual, making it a modal logic. The satisfiability relation can be used to generate a preorder relation on processes, which brings us to the notion of logical characterisation.

Definition 6

A logic $\mathcal {L}$ characterises a preorder $\preceq _\mathcal {L}$ over $\mathcal {P}$ if for any $p,q \in \mathcal {P}$, $p \preceq _\mathcal {L} q \text { iff } \forall \varphi \in \mathcal {L} [p \vDash \varphi \Rightarrow q \vDash \varphi ]$.

The following lemma justifies $\mathcal {L}_{(\rho ,\sigma )}$ by showing its invariance under $(\rho ,\sigma )$-bisimilarity.

Lemma 4

If $\rho ,\sigma$ are transitive, then for any processes p, q such that $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, we have $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$.

Proof

(By structural induction). Conjunction and disjunction being trivial cases, we only sketch the proofs for modal operators. Suppose we are given processes p, q such that $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$ and $p \vDash \varphi$ holds.

• $\varphi = {\langle a\rangle }^{\rho }\varphi '$: There must exist an action b and state $p'$, such that $p \overset{b}{\longrightarrow } p'$, $a \rho b$, and $p' \vDash \varphi '$. But since $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, we must have some action c and state $q'$, such that $q \overset{c}{\longrightarrow } q'$, $b \rho c$, and $p' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'$. By the induction hypothesis, we will have $q' \vDash \varphi '$. Also since $\rho$ is transitive, we have $a\rho c$. Hence $q \vDash {\langle a\rangle }^{\rho }\varphi '$.

• $\varphi = {[a]^{\sigma ^{-1}}}\varphi '$: Consider any transition $q \overset{b}{\longrightarrow } q'$, such that $b \sigma a$ holds. Since $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, there must exist an action c such that $p \overset{c}{\longrightarrow } p'$, $c \sigma b$, and $p' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'$. By transitivity of $\sigma$, we must have $c \sigma a$. If $p' \vDash \varphi '$, by the induction hypothesis, we must have $q' \vDash \varphi '$. This holds for any b such that $b \sigma a$, therefore, $q \vDash {[a]^{\sigma ^{-1}}}\varphi '$.    $\square$

The other direction, that is, if $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$ then $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, requires additional constraints, one of them being image-finiteness.

3.1 Image-Finiteness

Definition 7

An LTS $\mathfrak {L} ={{\langle \mathcal {P}, {\mathcal Act}, \longrightarrow \rangle }}$ is $(\rho ,\sigma )$-image-finite iff for any $p \in \mathcal {P}$ and $a \in {\mathcal Act}$, the sets, $\{q\ |\ p \overset{b}{\longrightarrow } q \wedge a \rho b\ \}$ and $\{q\ |\ p \overset{b}{\longrightarrow } q \wedge b \sigma a \}$, are finite. An LTS $\mathfrak {L}$ is image-finite upto $(\rho ,\sigma )$-bisimilarity if $\mathfrak {L}^\dagger _p$ is $(\rho ,\sigma )$-image-finite for every $p \in \mathcal {P}$.

Image-finiteness enables the decidability of bisimulation by making the bisimulation function co-continuous, which in turn guarantees a finite distinguishing behaviour between non-bisimilar processes.

Theorem 1

Given an LTS $\mathfrak {L}$, if for every $p \in \mathcal {P}$, the sets $\{p' | p \overset{b}{\longrightarrow } p'\wedge a \rho b\}$ and $\{ p'| a\sigma b \wedge p \overset{a}{\longrightarrow } p'\}$ are closed and $\mathfrak {L}^\dagger _p$ is $(\rho ,\sigma )$-image-finite, then $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} \subseteq \mathscr {F}_{(\rho ,\sigma )}(\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }})$, and hence $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} = {\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}}$.

Proof

Let $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} q$. Then for any $a,p'$ such that $p \overset{a}{\longrightarrow } p'$, the set $Q_i = \{q' | q \overset{b}{\longrightarrow } q' \wedge a \rho b \wedge p' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}} q'\}$ is non-empty for every i. Since $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}} \subseteq {\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{j}}}$, for all $i \ge j$, we would have $Q_i \subseteq Q_j$, which gives us a decreasing sequence of sets. If some $q'$ is common to every $Q_i$, then $q \overset{b}{\longrightarrow } q' \wedge a \rho b \wedge p' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{\omega }} q'$ will hold.

We can also show that $Q_i^\mathfrak {t} \subseteq Q_j^\mathfrak {t}$, for all $i \ge j$. Suppose not, i.e., $Q_i^\mathfrak {t} \not \subseteq Q_j^\mathfrak {t}$ for some i, j with $i \ge j$. Then there must exist some $r \in Q_i^\mathfrak {t}$ such that $r \not \in Q_j^\mathfrak {t}$. Now we will also have $r \in Q_i$, and hence $r \in Q_j$, since $Q_i \subseteq Q_j$. But since r is not in $Q_j^\mathfrak {t}$, there must exist some $r' \in Q_j^\mathfrak {t}$ such that $r \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} r'$ holds. But this would mean that $r'$ must also be in $Q_i$ since $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} \subseteq {\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}}$, and hence in $Q_i^\mathfrak {t}$ in place of r by transitivity of $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}$, giving us a contradiction.

By assumption, $Q_0$ is a closed set, and hence $Q_0^\mathfrak {t}$ is non-empty. In fact, we can show that for every $i \ge 0$, $Q_i$ is a closed set, making $Q_i^\mathfrak {t}$ non-empty. Consider any $r \in Q_i$, then r is also in $Q_0$, and hence there is some $r' \in Q_0^\mathfrak {t}$ such that $r \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} r'$. But since $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} \subseteq {\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}}$ and $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}^{i}}$ is transitive, $r'$ will also be in $Q_i$ and hence in $Q_i^\mathfrak {t}$.

Now under $(\rho ,\sigma )$-image-finiteness assumption, $Q_0^\mathfrak {t}$ is a finite set, hence there will be an $i_0$ such that $Q_{i_0}^\mathfrak {t} = Q_j^\mathfrak {t}$ for all $j \ge i_0$. Also $Q_{i_0}^\mathfrak {t}$ is non-empty, hence any element from $Q_{i_0}^\mathfrak {t}$ would be common to every $Q_i$. Similar argument can be made for a transition of q.    $\square$

Lemma 5

If $\rho ,\sigma$ are reflexive and $\mathfrak {L}^\dagger _p$ is $(\rho ,\sigma )$-image-finite for every $p \in \mathcal {P}$, then the preorder $\preceq _{\mathcal {L}_{(\rho ,\sigma )}}$ is a $(\rho ,\sigma )$-bisimulation.

Proof

(Proof by Contradiction). Assume not. Then there must exist processes p, q which are not bisimilar but $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$ holds. This can happen only if some transition of p or q cannot be matched, giving us two cases

Case 1: We have $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$ and $p \overset{a}{\longrightarrow } p'$, but there is no action b and state $q'$ with $q \overset{b}{\longrightarrow } q'$, $a \rho b$, and $p' \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q'$. Let $Q = \{q' \mid \exists b[q \overset{b}{\longrightarrow } q' \wedge a \mathrel {\rho } b] \}$. Now Q has a finite terminal set $Q^\mathfrak {t}$. Moreover, for every $q' \in Q^\mathfrak {t}$, there must exist a formula $\varphi _{q'}$ such that $p' \vDash \varphi _{q'}$ but $q' \not \vDash \varphi _{q'}$. Consider the formula $\varphi = \bigwedge _{q' \in Q^\mathfrak {t}}\varphi _{q'}$. Clearly $p' \vDash \varphi$, and since $\rho$ is reflexive, we have $p \vDash {\langle a\rangle }^{\rho }\varphi$. Since $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$, q must also satisfy this formula, but this requires some state $q'' \in Q$ to satisfy $\varphi$, which in turn requires some $q' \in Q^\mathfrak {t}$ to satisfy $\varphi$, as $q'' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q'$ (Lemma 4). But $q'$ cannot satisfy $\varphi _{q'}$, and consequently $\varphi$.

Case 2: We have $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$ and $q \overset{b}{\longrightarrow } q'$, but there is no action a and state $p'$ with $p \overset{a}{\longrightarrow } p'$, $a \sigma b$, and $p' \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q'$. Let $P = \{p' \mid \exists a[p \overset{a}{\longrightarrow } p' \wedge a \mathrel {\sigma } b] \}$. Now P has a finite initial set $P^\mathfrak {i}$. Moreover, for every $p' \in P$, there must exist a formula $\varphi _{p'}$ such that $p' \vDash \varphi _{p'}$ but $q' \not \vDash \varphi _{p'}$. Consider the formula $\varphi = \bigvee _{p' \in P^\mathfrak {i}}\varphi _{p'}$. For any $p'' \in P$, there will be some $p' \in P^\mathfrak {i}$ such that $p' \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p''$, and due to Lemma 4, we will have $p'' \vDash \varphi _{p'}$, consequently $p'' \vDash \varphi$, and hence, $p \vDash {[b]^{\sigma ^{-1}}}\varphi$. Since $p \preceq _{\mathcal {L}_{(\rho ,\sigma )}} q$, q must also satisfy this formula. But this is only possible if $q'$ satisfies $\varphi$ since $\sigma$ is reflexive.    $\square$

Theorem 2 now follows from Lemmas 4 and 5.

Theorem 2

If $\rho ,\sigma$ are preorders then $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} = {\preceq _{\mathcal {L}_{(\rho ,\sigma )}}}$, i.e. $\mathcal {L}_{(\rho ,\sigma )}$ is a logical characterisation of $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$ over $(\rho ,\sigma )$-image-finite LTS.    $\square$

The proof argument uses image-finiteness to ensure finite conjunctions and disjunctions. If we allow infinite conjunctions and disjunctions in our logic, denoted $\mathcal {L}_{(\rho ,\sigma )}^\infty$, then we can obtain the logical characterisation result without requiring the constraints of image-finiteness.

Theorem 3

If $\rho ,\sigma$ are preorders then $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} = {\preceq _{\mathcal {L}_{(\rho ,\sigma )}}}$, i.e. $\mathcal {L}_{(\rho ,\sigma )}^\infty$ is a logical characterisation of $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$.    $\square$

Logical characterisation implies the existence of a distinguishing formula, which is satisfied by p but not by q, whenever $p \mathrel {\not \!\underline{\Box }_{(\rho ,\sigma )}} q$. The proof of Lemma 5 can be molded into a procedure for generating the distinguishing formula. Procedure GenerateFormula generates a distinguishing formula between the input processes, assuming a bisimulation procedure which not only tells us whether two processes are bisimilar, but also gives us the unmatched transition when they are not. Image-finiteness bounds the number of recursive calls and also the depth of recursion, by guaranteeing an i such that $p \mathrel {\not \!\underline{\Box }_{(\rho ,\sigma )}} q$ implies $p \mathrel {\not \!\underline{\Box }_{(\rho ,\sigma )}^{i}} q$ (Theorem 1), and hence ensures the termination of the procedure.

3.2 Testing Preorders Logically

We may also view the parameterised HML formulas as tests. If $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, then the $\mathcal {L}_{(\rho ,\sigma )}$ formulas satisfied by p, denoted $\mathcal {L}_{(\rho ,\sigma )}(p)$, is a subset of the $\mathcal {L}_{(\rho ,\sigma )}$ formulas satisfied by q, $\mathcal {L}_{(\rho ,\sigma )}(q)$. If q is the specification, then $\mathcal {L}_{(\rho ,\sigma )}(q)$ can be seen as the set of allowed behaviours, therefore, $\mathcal {L}_{(\rho ,\sigma )}(p) \subseteq \mathcal {L}_{(\rho ,\sigma )}(q)$ ensures the correctness of p.

We may define complementation for the parameterised HML. Given a formula $\varphi \in \mathcal {L}_{(\rho ,\sigma )}$, its complement, ${\varphi }^c \in \mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}$, is defined by following structural induction.

It may be easily seen that $p \vDash \varphi$ iff $p \not \vDash {\varphi }^c$. Therefore, if $\mathcal {L}_{(\rho ,\sigma )}(p) \subseteq \mathcal {L}_{(\rho ,\sigma )}(q)$, then $\mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}(q) \subseteq \mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}(p)$. The specification may be seen as the set of all tests that the correct implementation should pass. Then, an implementation is correct under $(\rho ,\sigma )$-bisimilarity, iff all the specification’s tests, $\mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}(q)$, are satisfied by the implementation, implying $\mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}(q) \subseteq \mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}(p)$, which by logical characterisation result implies $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$.

Procedure IsModel gives a recursive method for deciding whether a formula $\varphi$ is satisfied by a process p. It is guaranteed to terminate when $\mathfrak {L}^\dagger _p$ is $(\rho ,\sigma )$-image-finite. Note that a finite or algebraic description of the LTS is not necessary. If the LTS is described co-algebraically, then the procedure IsModel gives a co-inductive definition². To evaluate a PHML formula, you only need to look at the current state and its immediate successors, which can be done in a purely observational model. Therefore, we may also view $\preceq _{\mathcal {L}_{(\rho ,\sigma )}} = {\preceq _{\mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}}^{-1}}$ as the testing equivalence obtained by interpreting formulas of logic $\mathcal {L}_{(\sigma ^{-1},\rho ^{-1})}$ as the encoding of tests.

4 Extending Parameterised HML with Fixed Point Operators

The parameterised HML can be extended with fixed point operators [18].

Definition 8

The syntax of the logic $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ is given by the following BNF

$$ \varphi \ :=\ \top \ |\ \bot \ |\ X \ |\ {\langle a\rangle }^{\rho }\varphi \ |\ [a]^{\sigma ^{-1}}\varphi \ |\ \varphi _1 \wedge \varphi _2 \ |\ \varphi _1 \vee \varphi _2 \ |\ \nu X.\varphi \ |\ \mu X.\varphi $$

where $a \in {\mathcal Act}$ and $X \in \mathcal {X}$ ranges over a countable set of variables.

The operators $\nu X$ and $\mu X$ denote the greatest fixed point and least fixed point respectively, binding the variable X in its scope. Any variable which is not bound is called a free variable. A closed formula is one without any free variables, and the fragment of closed formulas of the logic will be denoted $cf(\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}})$. To define the semantics, we need the notion of valuations, which assigns meaning to free variables. Given a countable set of variables $\mathcal {X}$, a valuation $\mathcal {V}$ is essentially a map from $\mathcal {X}$ to $2^\mathcal {P}$.

Definition 9

The semantics of the formula $\varphi \in \mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ over some process set $\mathcal {P}$ is defined inductively as,

where ${\mathcal {V}[\mathcal {E}/X]} (Y) = \mathcal {V}(Y)$ for all $Y \not = X$ and ${\mathcal {V}[\mathcal {E}/X]} (X) = \mathcal {E}$.

The semantics of any formula depends upon the valuation supplied. Consequently, the satisfaction relation should be redefined.

Definition 10

A process p satisfies a formula $\varphi$ under $\mathcal {V}$, denoted $p \vDash _\mathcal {V} \varphi$, iff $p \in ||{\varphi }||^\mathcal {P}_\mathcal {V}$. It satisfies the formula $\varphi$, denoted $p \vDash \varphi$, iff $p \in ||{\varphi }||^\mathcal {P}_\mathcal {V}$ for all valuations $\mathcal {V}$.

A valuation can be seen as an element of $(2^\mathcal {P})^{|\mathcal {X}|}$, which is the $|\mathcal {X}|$ fold product of $2^\mathcal {P}$. Since powerset forms a complete lattice, and the direct product of a countable collection of complete lattices is also a complete lattice, this must also be a complete lattice under pointwise subset ordering [8]. More formally,

Definition 11

Let $\mathcal {V}_1$ and $\mathcal {V}_2$ be any two valuations over $\mathcal {X}$. We define a partial order $\le$ on valuations as

$$ \mathcal {V}_1 \le \mathcal {V}_2 \Leftrightarrow \forall X \in \mathcal {X}[\mathcal {V}_1(X) \subseteq \mathcal {V}_2(X)] $$

The $\le$ ordering yields a complete lattice, $(\mathcal {X} \rightarrow 2^{\mathcal {P}}, \le )$, over valuations.

The semantics of any formula is monotonic with respect to this partial order over valuations.

Lemma 6

Let $\mathcal {V}_1$ and $\mathcal {V}_2$ be any two valuations over $\mathcal {X}$ and $\varphi$ be any formula in $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$. If $\mathcal {V}_1 \le \mathcal {V}_2$ then $||{\varphi }||^\mathcal {P}_{\mathcal {V}_1} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}_2}$ (Refer [25]).    $\square$

Given a formula $\varphi$ with a free variable $X \in \mathcal {X}$, the function, $\mathcal {O}_\varphi (\mathcal {V}) = \mathcal {V}[||{\varphi }||^\mathcal {P}_\mathcal {V}/X]$, is monotonic over the complete lattice $(\mathcal {X} \rightarrow 2^{\mathcal {P}}, \le )$. Hence by Tarski’s theorem [29], the semantic definition of $\nu X$ and $\mu X$ indeed defines the greatest and the least fixed point respectively. It also makes the model checking of $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ decidable over finite-state systems. For example, to compute $||{\nu X.\varphi }||^\mathcal {P}$, we just need to apply $\mathcal {O}_\varphi$ repeatedly, starting from $\mathcal {P}$ (empty set in case of least fixed point), until we reach a fixed point.

Theorem 4

Given a finite $\mathfrak {L}^\dagger _p$, for any $\varphi \in cf(\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}})$, $p \vDash \varphi$ is decidable.   $\square$

4.1 Preservation Under Bisimulations

The characterisation result can be broken into two assertions. Firstly, if q satisfies all the formulae which are satisfied by p, then p is $(\rho ,\sigma )$-bisimilar to q. Since $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ extends $\mathcal {L}_{(\rho ,\sigma )}$, this result will continue to hold. Interestingly, the other assertion, i.e. if p is $(\rho ,\sigma )$-bisimilar to q then q satisfies all formulae which are true for p, also holds for $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$, despite it being more expressive on account of fixed point operators, provided that the valuation is $(\rho ,\sigma )$-bisimilarity-closed.

Definition 12

Given any relation $\mathcal {R}$, a set $\mathcal {E} \subseteq \mathcal {P}$ is $\mathcal {R}$-closed iff for every process p, q, whenever $p \in \mathcal {E}$ and $p \mathcal {R} q$, we have $q \in \mathcal {E}$. Naturally, a valuation $\mathcal {V}$ is $\mathcal {R}$-closed iff $\mathcal {V}(X)$ is $\mathcal {R}$-closed for every variable X.

For every $p,q \in \mathcal {P}$ with $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, $p \in ||{\varphi }||^\mathcal {P}_\mathcal {V}$ implies $q \in ||{\varphi }||^\mathcal {P}_\mathcal {V}$ is equivalent to saying that the set $||{\varphi }||^\mathcal {P}_\mathcal {V}$ is bisimilarity-closed, i.e., the counterpart of Lemma 4 here will be showing that $||{\varphi }||^\mathcal {P}_\mathcal {V}$ is bisimilarity-closed. The results given below are a generalization of a corresponding result for strong bisimulation [28].

Definition 13

• 1. Given any set $\mathcal {E} \subseteq \mathcal {P}$, its upward $(\rho ,\sigma )$-bisimilarity closure, $\mathcal {E}^u_{(\rho ,\sigma )}$, is the set $\{ q \in \mathcal {P}\ |\ \exists p[p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}q \wedge p \in \mathcal {E}] \}$.

• 2. Given any set $\mathcal {E} \subseteq \mathcal {P}$, its downward $(\rho ,\sigma )$-bisimilarity closure, $\mathcal {E}^d_{(\rho ,\sigma )}$, is the set $\{ p \in \mathcal {E}\ |\ \forall q [p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}q \Rightarrow q \in \mathcal {E} ]\}$.

Lemma 7

Let $\mathscr {E} = \{ \mathcal {E}_i \}_{i \in \mathcal {I}}$ be any collection of $(\rho ,\sigma )$-bisimilarity-closed sets. Then both $\bigcup _{i \in \mathcal {I}} \mathcal {E}_i$ and $\bigcap _{i \in \mathcal {I}} \mathcal {E}_i$ are also $(\rho ,\sigma )$-bisimilarity-closed.    $\square$

Lemma 8

If $\rho ,\sigma$ are preorders, then for any arbitrary set $\mathcal {E}$,

• 1. $\mathcal {E}^u_{(\rho ,\sigma )}$ is a $(\rho ,\sigma )$-bisimilarity-closed set containing $\mathcal {E}$.

• 2. $\mathcal {E}^d_{(\rho ,\sigma )}$ is a $(\rho ,\sigma )$-bisimilarity-closed set contained in $\mathcal {E}$ (Refer [25]).    $\square$

Lemma 9

Given preorders $\rho ,\sigma$, $(\rho ,\sigma )$-image-finite processes in $\mathcal {P}$ and a $(\rho ,\sigma )$-bisimilarity-closed valuation $\mathcal {V}$, the set $||{\varphi }||^\mathcal {P}_\mathcal {V}$ is also $(\rho ,\sigma )$-bisimilarity-closed for any formula $\varphi \in \mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$.

Proof

We extend the inductive argument of Lemma 4, which requires $(\rho ,\sigma )$-image-finiteness, with the proofs for fixed point operators. The case of the single variable X trivially follows from the fact that the valuation $\mathcal {V}$ is $(\rho ,\sigma )$-bisimilarity-closed.

• Case $\nu X.\varphi$: For any $\mathcal {E} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]}$, we have $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$ (Lemma 6), and hence $\mathcal {E} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$. By the induction hypothesis, $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$ is $(\rho ,\sigma )$-bisimilarity-closed. We can show $\mathcal {E}^u \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$, as any $q \in \mathcal {E}^u$ will have a $p \in \mathcal {E}$ with $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$. Since $\mathcal {E} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$, we will have $p \in ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$, and hence $q \in ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]}$, due to it being $(\rho ,\sigma )$-bisimilarity-closed. Since $\mathcal {E}^u \cup \mathcal {E} = \mathcal {E}^u$, we can rewrite $\bigcup \{\mathcal {E} \subseteq \mathcal {P}\ |\ \mathcal {E} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]} \}$ as $\bigcup \{\mathcal {E}^u \subseteq \mathcal {P}\ |\ \mathcal {E}^u \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^u/X]} \}$, which is a $(\rho ,\sigma )$-bisimilarity-closed set by Lemma 7, and hence $||{\nu X. \varphi }||^\mathcal {P}_\mathcal {V}$ is $(\rho ,\sigma )$-bisimilarity-closed.

• Case $\mu X.\varphi$: For any $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]} \subseteq \mathcal {E}$, we have $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]} \subseteq ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]}$ (Lemma 6), and hence $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]} \subseteq \mathcal {E}$. By the induction hypothesis, $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]}$ is $(\rho ,\sigma )$-bisimilarity-closed. Therefore, for any p, q with $p \in ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]}$ and $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$, we will have $q \in ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]}$ and hence $q \in \mathcal {E}$. This, however, implies that p must be in $\mathcal {E}^d$, and hence $||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]} \subseteq \mathcal {E}^d$. Since $\mathcal {E}^d \cap \mathcal {E} = \mathcal {E}^d$, we can rewrite $\bigcap \{\mathcal {E} \subseteq \mathcal {P}\ |\ ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}/X]} \subseteq \mathcal {E} \}$ as $\bigcap \{\mathcal {E}^d \subseteq \mathcal {P}\ |\ ||{\varphi }||^\mathcal {P}_{\mathcal {V}[\mathcal {E}^d/X]} \subseteq \mathcal {E}^d \}$, which is a $(\rho ,\sigma )$-bisimilarity-closed set by Lemma 7, and hence $||{\mu X. \varphi }||^\mathcal {P}_\mathcal {V}$ is also $(\rho ,\sigma )$-bisimilarity-closed.    $\square$

If $\varphi$ is a closed formula, i.e. $\varphi \in cf(\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}})$, then its meaning is independent of the valuation, and hence is always bisimilarity-closed.

Theorem 5

Given preorders $\rho ,\sigma$, for any $(\rho ,\sigma )$-image-finite processes p, q, $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$ iff $p \preceq _{cf(\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}})} q$, i.e., $cf(\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}})$ is a logical characterisation for $\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}$.

4.2 Characteristic Formula

Equipped with the fixed point operators, the logic $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ is powerful enough to define characteristic formulae. Given a process p, a characteristic formula is satisfied only by the processes which are $(\rho ,\sigma )$-bisimilar to p. Its existence, therefore, reduces bisimulation checking to model checking. More formally,

Definition 14

A closed formula $\varphi _p \in \mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ is characteristic of a process p, if for every $q\in \mathcal {P}$, we have $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$ iff $q \in ||{\varphi _p}||^\mathcal {P}$.

Numerous derivations of characteristic formulae share a common underlying structure [2], which encode the fixed point characterisation of the relation as a formula in the logic. We adopt the derivation in [22] for parameterised bisimulations, as it gives a step-by-step conversion of the fixed point characterisation into a characteristic formula.

We will derive an equational system from which the characteristic formula can be obtained using standard techniques [22]. Given some process set $\mathcal {P}$, an equational system $E^{\mathcal {P}}$ is a collection of mutually recursive equations of the form $X_p = \varphi _p$, where $\varphi _p \in \mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$ and $p \in \mathcal {P}$. We can also view this equational system as a function over valuations, defined as $(E^{\mathcal {P}}(\mathcal {V}))(X_p) = ||{\varphi _p}||^\mathcal {P}_\mathcal {V}$. By Lemma 6, this defines a monotonic function over the lattice $(\{X_p\}_{p \in \mathcal {P}} \rightarrow 2^{\mathcal {P}}, \le )$, which is isomorphic to the lattice of binary relations over $\mathcal {P}$.

Lemma 10

The lattice $(\{X_p\}_{p \in \mathcal {P}} \rightarrow 2^{\mathcal {P}}, \le )$ is isomorphic to $(2^{\mathcal {P} \times \mathcal {P}},\subseteq )$ under the following mapping

$$ \begin{array}{lcl} \mathbb {I}(\mathcal {V}) = \{ (p,q)\ |\ q \in \mathcal {V}(X_p) \}&&\mathbb {I}^{-1}(R) = \{ q \in \mathcal {V}(X_p)\ |\ (p,q) \in R \} \end{array} $$

The utility of this isomorphism lies in its ability to define a characteristic equational system as $E^{\mathcal {P}} = \mathbb {I}^{-1} \circ \mathscr {F}_{(\rho ,\sigma )} \circ \mathbb {I}$, with its greatest fixed point corresponding to $(\rho ,\sigma )$-bisimilarity. Its encoding in logic follows as

$$ \begin{array}{clr} &{} q \in (\mathbb {I}^{-1} \circ \mathscr {F}_{(\rho ,\sigma )} \circ \mathbb {I})(\mathcal {V})(X_p) &{} \\ \Longleftrightarrow &{} (p,q) \in (\mathscr {F}_{(\rho ,\sigma )} \circ \mathbb {I})(\mathcal {V}) &{} [\text {by definition of }\mathbb {I}^{-1}] \\ \Longleftrightarrow &{} (\forall a,p' : p \overset{a}{\longrightarrow } p' \Rightarrow \exists b, q'[ a\rho b \wedge q \overset{b}{\longrightarrow } q' \wedge q' \in \mathcal {V}(X_{p'}) ]) \wedge &{} \\ &{} (\forall b,q' : q \overset{b}{\longrightarrow } q' \Rightarrow \exists a, p'[ a\sigma b \wedge p \overset{a}{\longrightarrow } p' \wedge q' \in \mathcal {V}(X_{p'}) ]) &{} [\text {by definition of }\mathscr {F}_{(\rho ,\sigma )},\mathbb {I}] \\ \end{array} $$

We can translate the above two conditions to logic in the following manner

Assuming $\rho ,\sigma$ are preorders, $\forall b,q': q \overset{b}{\longrightarrow } q' \Rightarrow q' \in ||{\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'}}||^\mathcal {P}_\mathcal {V}$ is equivalent to $\forall b,c,q': c \sigma b \wedge q \overset{c}{\longrightarrow } q' \Rightarrow q' \in ||{\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'}}||^\mathcal {P}_\mathcal {V}$. First implies the second due to transitivity, which makes $\{(a, p')\ | \ a\sigma c \wedge p \overset{a}{\longrightarrow } p'\} \subseteq \{(a, p')\ |\ a\sigma b \wedge p \overset{a}{\longrightarrow } p'\}$ whenever $c \sigma b$ holds, and hence $q \in ||{\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'}}||^\mathcal {P}_\mathcal {V}$ is true whenever $q \in ||{\bigvee _{a, p': a\sigma c \wedge p \overset{a}{\longrightarrow } p'} X_{p'}}||^\mathcal {P}_\mathcal {V}$ is true. Second implies the first due to reflexivity of $\sigma$, giving us,

Combining the two, the characteristic equational system, $E^{\mathcal {P}'}_{\mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}}}$, becomes

$$ X_p = (\bigwedge _{a,p': p \overset{a}{\longrightarrow } p'} {\langle a\rangle }^{\rho }X_{p'}) \wedge (\bigwedge _{b}{[b]^{\sigma ^{-1}}}(\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'})) $$

Clearly, if $\mathfrak {L}^\dagger _p$ is finite, then the equational system will also be finite. Now for any two actions a, b with $a \rho b$, the formula ${\langle b\rangle }^{\rho } \varphi$ implies ${\langle a\rangle }^{\rho } \varphi$. Therefore, if every subset of ${\mathcal Act}$ has finitely many maximal elements under the ordering $\rho$, then we can always rewrite $\bigwedge _{a,p': p \overset{a}{\longrightarrow } p'} {\langle a\rangle }^{\rho }X_{p'}$ as a finite conjunct. Similarly, ${[b]^{\sigma ^{-1}}} \varphi$ implies ${[a]^{\sigma ^{-1}}} \varphi$ if $a \sigma b$ holds, and $\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'}$ will be finite if we have only finitely many variables. Therefore, if every subset of ${\mathcal Act}$ has finitely many maximal elements under the ordering $\sigma$, then we can always rewrite $\bigwedge _{b}{[b]^{\sigma ^{-1}}}(\bigvee _{a, p': a\sigma b \wedge p \overset{a}{\longrightarrow } p'} X_{p'})$ as a finite conjunct. The following theorem captures this idea,

Theorem 6

A process p has a finite characteristic formula in $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$, if $\rho$ and $\sigma$ are preorders with finitely many maximal elements and every action being less than some maximal element, and $\mathfrak {L}^\dagger _p$ is finite with $p_{\mathfrak {L}^\dagger _p} \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} p_\mathfrak {L}$.    $\square$

By constructing the characteristic formula of p and model checking it for q, we obtain a procedure for deciding parameterised bisimilarity, $p \mathrel {\mathrel {\underline{\Box }}_{(\rho ,\sigma )}} q$ [10]. Though this requires $\rho$ and $\sigma$ to have finitely many maximal elements, and $\mathfrak {L}^\dagger _p$, $\mathfrak {L}^\dagger _q$ to be finite, i.e., the set of reachable initial and terminal states from p and q must be finite.

5 Applications

Weak Bisimilarity and Efficiency Preorder. Expressing concrete bisimulations as parameterised bisimulations may involve LTS transformation, for e.g., weak bisimulation requires the transitive closure of the transition relation under $\tau$ actions [4], i.e. extending the action set to sequences $\tau ^ia\tau ^j$, $i,j \ge 0$. Weak bisimulation [16] is a $(\hat{=},\hat{=})$-bisimulation over this extended action set, where $\hat{=} = \{(\tau ^i,\tau ^j)\mid i,j\ge 0\} \mathbin {\cup } \{(\tau ^ia\tau ^j,\tau ^{i'}a\tau ^{j'})\mid i,j,i',j'\ge 0, a \in {\mathcal Act}\}$. This gives the logical characterisation $\mathcal {L}_{(\hat{=},\hat{=})}$, which is identical to observational HML [16]. Similarly, efficiency preorders [5] is a $({\preceq },{\preceq })$-bisimulation, where ${\preceq } = \{(\tau ^i,\tau ^j)\mid 0\le i\le j\} \mathbin {\cup } \{(\tau ^ia\tau ^j,\tau ^{i'}a\tau ^{j'})\mid 0 \le i+j \le i'+j', i,j,i',j'\ge 0, a \in {\mathcal Act}\}$. Its logical characterisation $\mathcal {L}_{({\preceq },{\preceq })}$, however, differs from the existing one [17].

Covariant-Contravariant Simulation. The classical view of process simulation assumes all actions to be input actions, which the user may trigger. The simulating process must simulate all the input actions of the process being simulated. But in the presence of output actions, this condition is reversed. This forms the intuition for defining covariant-contravariant simulations [11].

Definition 15

Let $\mathcal {P}$ be the set of process states and ${\mathcal Act}$ be the set of actions which can be partitioned into the sets $\mathcal {A}ct^r$, $\mathcal {A}ct^l$ and $\mathcal {A}ct^{bi}$. A binary relation $R \subseteq \mathcal {P} \times \mathcal {P}$ is a covariant-contravariant simulation if $p\mathrel {R}q$ implies the following conditions

$$ \begin{aligned} \forall a \in \mathcal {A}ct^r \cup \mathcal {A}ct^{bi}[ p \overset{a}{\longrightarrow } p'&\Rightarrow \exists q'[ q \overset{a}{\longrightarrow } q' \wedge p'\mathrel {R}q']] \\ \forall a \in \mathcal {A}ct^l \cup \mathcal {A}ct^{bi}[q \overset{a}{\longrightarrow } q'&\Rightarrow \exists p'[ p \overset{a}{\longrightarrow } p'\wedge p'\mathrel {R}q'] \end{aligned} $$

We will write $p \lesssim _{CC} q$, if there is a covariant-contravariant simulation R such that $p \mathrel {R} q$.

The covariant-contravariant simulation, defined above, ignores the $\mathcal {A}ct^l$ transitions for p and $\mathcal {A}ct^r$ transitions for q. To specify it as an instance of parameterised bisimulation, we introduce a special state $\mathbf {0}$, such that from every process p there is a transition $p \overset{!}{\longrightarrow } \mathbf {0}$, and there is only one transition from $\mathbf {0}$, that is to itself as $\mathbf {0} \overset{*}{\longrightarrow } \mathbf {0}$, where !, $*$ are new action labels. Now covariant-contravariant simulation can be instantiated as parameterised bisimulation by setting $\rho = Id^{\mathcal {A}ct} \cup \{(a,!) | a \in \mathcal {A}ct^l\} \cup \{(a,*)|a \in \mathcal {A}ct \} \cup \{(!,!),(*,*),(*,!\}$ and $\sigma ^{-1} = Id^{\mathcal {A}ct} \cup \{(a,!) | a \in \mathcal {A}ct^r\} \cup \{(a,*)|a \in \mathcal {A}ct \} \cup \{(!,!),(*,*),(*,!\}$. All processes will be $(\rho ,\sigma )$-bisimilar to $\mathbf {0}$. Also, $\mathbf {0}$ satisfies every formula $\psi \in \mathcal {L}_{(\rho ,\sigma ^{-1})}$. As a consequence, every process p will satisfy any formula of the form ${\langle !\rangle }^{\rho }\psi$, and hence ${\langle a\rangle }^{\rho }\psi$ where $a \in \mathcal {A}ct^l$, as well as ${\langle *\rangle }^{\rho }\psi$, for any $\psi \in \mathcal {L}_{(\rho ,\sigma ^{-1})}$. Similar argument also holds for ${[!]^{\sigma ^{-1}}}\psi$, ${[*]^{\sigma ^{-1}}}\psi$ and ${[a]^{\sigma ^{-1}}}\psi$, where $a \in \mathcal {A}ct^r$ and $\psi$ is any formula in $\mathcal {L}_{(\rho ,\sigma )}$. If we remove these modalities, we are only left with ${\langle a\rangle }^{\rho }$, where $a \in \mathcal {A}ct^r \cup \mathcal {A}ct^{bi}$ and ${[a]^{\sigma ^{-1}}}$, where $a \in \mathcal {A}ct^l \cup \mathcal {A}ct^{bi}$, and $\rho$, $\sigma$ are identity relations over these actions. This is exactly the logical characterisation given in [12] for covariant-contravariant simulation.

Time Abstracted Bisimilarity and Timed Prebisimulation. Timed LTS is a special class of LTS, where the label set is of the form ${\mathcal Act}\cup \mathbb {R}_{\ge 0}$, where the labels in $\mathbb {R}_{\ge 0}$ correspond to delay observations. The strong bisimulation over Timed LTS is also referred as Timed bisimulation. In general, the timed bisimilarity over arbitrary Timed LTS is undecidable, but it becomes decidable when restricted to Timed LTS generated from Timed Automata [3]. The Timed LTS generated from Timed Automata has deterministic delays, that is, there is a unique successor state for every delay transition. This, in turn, implies image-finiteness, and hence the logical characterisation for strong bisimilarity also works for timed bisimilarity.

Time abstracted bisimulation [20], which relaxes the condition of matching a delay transition with any other delay transition, irrespective of the delay amount, is another interesting behavioural equivalence over Timed LTS. As noted in Sect. 3, time abstracted bisimulation [16] is a $({\simeq },{\simeq })$-bisimulation, where ${\simeq } = {\mathcal Id}_{\mathcal Act} \mathbin {\cup } (\mathbb {R}_{\ge 0} \mathbin {\times } \mathbb {R}_{\ge 0})$. It is also decidable for TLTS generated from timed automata. In fact one can apply zone abstraction [6] to obtain a finite abstracted LTS, as all states in the same zone are time abstracted bisimilar. Since a finite abstracted LTS is always image-finite, we obtain $\mathcal {L}_{(\simeq ,\simeq )}$ as the logical characterisation for time abstracted bisimilarity.

Similarly, timed prebisimulation [15] is a $({\gtrsim },{\gtrsim })$-bisimulation, where ${\gtrsim } = Id_{\mathcal Act}\mathbin {\cup }\ge _{\,\,\mathbb R}$. Again we can apply zone abstraction, and use zone endpoints to obtain a finite abstracted LTS for TLTS generated from timed automata. However we require infinitesimal $\delta$-delays, of the form $d + \delta$ or $d - \delta$, to define zone endpoints when zone boundaries are given by strict inequalities. This is also why the decidability result for timed prebisimilarity based on zone abstraction is restricted to one clock timed automata [15]. This technique can only be applied to one clock timed automata, as $\delta$ delays for multiple clocks are incomparable. We can remove the $\delta$-delays from our logical characterisation, by noting that ${\langle d-\delta \rangle }^{\ge } = {\langle d\rangle }^{\ge }$, ${\langle d+\delta \rangle }^{\ge } = {\langle d\rangle }^{>}$, ${[d-\delta ]^{\le }} = {[d]^{<}}$, and ${[d+\delta ]^{\le }} = {[d]^{\le }}$. Hence we obtain the following as logical characterisation for timed prebisimilarity over TLTS generated from one clock timed automata.

$$ \varphi \ :=\ \langle {a}\rangle \varphi \ |\ [a]\varphi \ |\ {\langle d\rangle }^{\ge }\varphi \ |\ [d]^{\le }\varphi \ |\ {\langle d\rangle }^{>}\varphi \ |\ [d]^{<}\varphi \ |\ \varphi _1 \wedge \varphi _2\ |\ \varphi _1 \vee \varphi _2 $$

where $a \in {\mathcal Act}$ and $d \in \mathbb {R}_{\ge 0}$. We refer the reader to [26] for detailed proof.

6 Conclusion and Future Work

Parameterised HML, $\mathcal {L}_{(\rho ,\sigma )}$, generalises HML as the logical characterisation for parameterised bisimulations. By selecting suitable relations on actions, one readily obtains the existing characterisations of strong and weak bisimulation, covariant-contravariant simulation [12], and novel characterisations for prebisimilarity relations like efficiency preorder [17], timed prebisimulation [15], etc.

The characterisation immediately yields distinguishing formulae between non-bisimilar processes. However it requires $(\rho ,\sigma )$-image-finiteness upto $(\rho ,\sigma )$-bisimilarity, in which case non-bisimilar processes have a finite distinguishing behaviour. Consequently, we obtain the algorithm for generating distinguishing formulae when the processes are $(\rho ,\sigma )$-image-finite and have a decidability procedure for $(\rho ,\sigma )$-bisimilarity.

The extension of parameterised HML with fixed point operators, $\mathcal {L}_{(\rho ,\sigma )}^{\mathcal {X}}$, remains invariant under the corresponding parameterised bisimulation, while increasing its power to allow expressing characteristic formulae for finite-state processes. Model checking of characteristic formula may yield efficient algorithms for deciding behavioural relations [10], and is worth studying in the context of parameterised bisimulations.

Generating distinguishing formula requires image-finiteness; similarly the existence of finite characteristic formula is only guaranteed for finite-state systems. Interestingly, these results may be extended to infinite-state systems through abstracted LTS. Infinite-state systems with quantitative aspects, like time, may offer interesting instantiations of parameterised bisimulations, and can become a good application domain for these results.

The expressive power of parameterised HML is another area worth investigating. This may involve generalizing the correspondence results for modal logic and strong bisimulation [7], and may help in relating this logic to $(\rho ,\sigma )$-bisimulation invariant fragments of classical logics. This will enable us to compare our logical characterisation with the existing ones, where they differ.