## Quantales, observational logic and process semantics.(English)Zbl 0823.06011

From the abstract: “Various notions of observing and testing processes are placed in a uniform algebraic framework in which observations are taken as constituting a quantale.” A quantale is a complete join semilattice with a binary associative operation $$\cdot$$ that has an identity element 1 and is both left and right distributive over arbitrary joins. Examples of quantales arise from monoids. Consider a monoid with binary operation $$*$$ and unit $$e$$. Take all subsets of this monoid with union as join. This produces a complete join semilattice. To get a quantale, define, for subsets $$X$$ and $$Y$$ of the monoid, $$X\cdot Y= \{x* y: x\in X, y\in Y\}$$ and let $$1= \{e\}$$. The quantale of all binary relations on a set, with union as join, relative multiplication as product, and the identity relation as identity element, is a special case of this construction.
A (right) module $$M$$ over a quantale $$Q$$ is a join semilattice on which the elements of the quantale $$Q$$ act as operators through an action $$\cdot: M\times Q\to M$$ satisfying $$m\cdot 1= m$$, $$m\cdot (q\cdot q')= (m\cdot q)\cdot q'$$, $$m\cdot \bigvee Q'= \bigvee \{m\cdot q: q\in Q'\}$$, $$\bigvee M'\cdot q= \bigvee \{m\cdot q: m\in M'\}$$. Every quantale is, of course, a module over itself. Modules over quantales generalize both topological spaces and labelled transition systems. A labelled transition system is a ternary relation $$\to$$, contained in $$\text{Proc}\times \text{Act}\times \text{Proc}$$, where Proc is a set whose elements are called “processes”, and Act is a set whose elements are called “actions”. Each action $$\alpha$$ determines a binary relation $$@> \alpha>>$$ on processes, namely $$@> \alpha>>= \{(p, q): p, q\in \text{Proc}, (p, \alpha, q)\in \to\}$$. Each finite sequence $$s= \alpha_ 1 \alpha_ 2\alpha_ 3\cdots \alpha_ n\in \text{Act}^*$$ also determines a binary relation $$@> s>>$$ on Proc, namely $$@> s>>= @> \alpha_ 1>>;@> \alpha_ 2>>;@> \alpha_ 3>>;\cdots;@> \alpha_ n>>$$, where ; is relational composition. The power-set algebra of the free monoid generated by Act, that is, the algebra whose elements are the subsets of $$\text{Act}^*$$, is a free quantale over Act. This quantale acts on the quantale of subsets of Proc via the module action $${\mathcal P}(\text{Proc})\times {\mathcal P}(\text{Act}^*)\to {\mathcal P}(\text{Proc})$$ that sends a subset $$P$$ of Proc and a subset $$S$$ of $$\text{Act}^*$$ to the union of the images of $$P$$ under $$@> s>>$$, where $$s$$ ranges over $$S$$, i.e., $$P\cdot S= \{q\colon p@> s>> q$$ for some $$p\in P$$, $$s\in S\}$$.
The authors consider nine equivalence relations on Proc determined by the ternary relation $$\to$$. Several of them are defined by associating a set of structures with each process and considering two processes to be equivalent if they have the same associated set of structures. Structures used this way are the “traces”, “accepts”, “failures”, “readies”, “accept-traces”, “failure-traces”, and “ready-traces” of a process. For example, the set traces$$(p)$$ of traces of $$p$$ is the set of finite sequences $$s\in \text{Act}^*$$ such that $$p$$ is in the domain of $$@> s>>$$. Two processes are trace-equivalent if they have the same set of traces. For each of these equivalences a particular quantale is shown to satisfy three completeness criteria. For example, $${\mathcal P}(\text{Act}^*)$$ satisfies these criteria for trace-equivalence. The quantales are described by generators and relations. For trace- equivalence the generators are the elements of Act, and there are no relations. For other equivalences some new generators are introduced, such as $$\alpha^ \surd$$ and $$\alpha^ \times$$, where $$@> \alpha^ \surd>>$$ is the identity relation on the domain of $$@> \alpha>>$$ and $$@> \alpha^ \times>>$$ is the identity relation on the complement of the domain of $$@> \alpha>>$$. Some of the equivalences require further complications, such as the use of $${\mathcal P}(\text{Proc}\times \text{Proc}^*)$$ in place of $${\mathcal P}(\text{Proc})$$, plus a considerable amount of additional algebraic material.