Characteristic Formulae

A piece of classic concurrency theory that is perhaps not so well known as it deserves to be concerns the characterization of the equivalence class of a process p (modulo a suitable notion of behavioural equivalence) by means of a single formula F(p) in a logic. This means that, no matter what process q we consider, q is equivalent to p iff it satisfies the formula F(p). The formula F(p), when it exists, is usually referred to as the characteristic formula of p (modulo the chosen notion of equivalence). Of course, the formula F(p) is unique up to logical equivalence, and that's why we allow ourselves the liberty to talk about the characteristic formula for p.

Why is this notion interesting at all? A classic result in the theory of concurrency is the characterization theorem of bisimulation equivalence in terms of Hennessy-Milner logic (HML) due to Matthew Hennessy and Robin Milner. (See this paper.) This theorem states that two bisimilar processes satisfy the same formulae in Hennessy-Milner logic, and if the processes satisfy a technical "image finiteness condition", then they are also bisimilar when they satisfy the same formulae in the logic. This means that, for bisimilarity and HML, logical equivalence coincides with behavioural equivalence, and that whenever two processes are not equivalent, then we can always find a formula in HML that witnesses a reason why they are not. This distinguishing formula is useful for debugging purposes, and can be algorithmically constructed for finite processes. (Algorithms for computing such distinguishing formulae for strong and weak bisimilarity are implemented in tools like the Edinburgh Concurrency Workbench.)

The characterization theorem of Hennessy and Milner is, however, less useful if we are interested in using it directly to establish when two processes are behaviourally equivalent using the logic. Indeed, that theorem seems to indicate that to show that two processes are equivalent we need to check that they satisfy the same formulae expressible in the logic, and there are countably many such formulae, even modulo logical equivalence. Isn't it possible to find a single formula that characterizes the equivalence of a process p?

To the best of my knowledge, this natural question was first addressed by Susanne Graf and Joseph Sifakis in their paper

Susanne Graf and Joseph Sifakis. A modal characterization of observational congruence on finite terms of CCS. Inform. and Control, 60 (1986), no. 1-3, pp. 125--145.

In that paper, they offered a translation from recursion-free terms of Milner's CCS into formulas of a modal language representing their equivalence class with respect to observational congruence.

Can one characterize the equivalence class of an arbitrary finite process---for instance one described in the regular fragment of CCS---up to bisimilarity using HML? The answer is negative because each formula in that logic can only describe a finite fragment of the initial behaviour of a process. (The "sight" of a formula is limited by the maximum nesting of modal operators occurring in it.)

Consider, for instance, the automaton over set of labels {a,b} with only one state p and a self-loop edge labelled a. The characteristic formula for p modulo bisimulation should state the following properties, which together completely characterize the behavior of p.

1. Process p affords an a-labelled transition leading to itself (that is, to a process that is bisimilar to p).
   
2. No matter how p makes an a-labelled transition, it always ends up in a state that is bisimilar to p.
3. Process p affords only a-labelled transitions.

If we let F(p) stand for the characteristic formula for p, then we can express the above properties in HML by means of the following recursively defined formula:

F(p) = diamond(a) F(p) AND [a]F(p) AND [b] False,

where I write diamond(a) for the a-labelled may modality in HML to prevent the blogging software from interpreting the standard notation as a HTML tag :-)

The right-hand side of the above formula determines a monotonic endofunction over the collection of sets of processes. The famous Knaster-Tarski fixed-point theorem yields a complete lattice of fixed-points for that function. It turns out that the largest fixed-point is the collection of all processes that are bisimilar to p. So, we can give characteristic formulae modulo bisimulation for states of finite labelled transition systems using HML enriched with a facility for the recursive definition of formulae, where recursively defined formulae are interpreted using largest fixed-points.

I believe that this characteristic formula construction was first noticed in the relatively unknown MSc thesis

Anna Ingolfsdottir, Jens Christian Godskesen and Michael Zeeberg. Fra Hennessy-Milner Logik til CCS-Processer. Department of Computer Science, Aalborg University, 1987

The thesis, supervised by Kim G. Larsen, was unfortunately encrypted in Danish, and this is one of the reasons why it is not as well known as it deserves to be. Some of ideas and technical developments from that work then appeared in the paper

Bernhard Steffen, Anna Ingolfsdottir: Characteristic Formulae for Processes with Divergence Inf. Comput. 110(1): 149-163 (1994),

which is by now the standard reference for the development of characteristic formulae for bisimulation-like behavioural relations over finite processes.