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

Abramsky, Samson; Vickers, Steven

Math. Struct. Comput. Sci. 3, No. 2, 161-227 (1993).

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.

Reviewer: R.Maddux (Ames)

MSC:

06F05	Ordered semigroups and monoids
03B70	Logic in computer science
68Q55	Semantics in the theory of computing

Keywords:

observational logic; process semantics; module over a quantale; observations; quantale; labelled transition system; free quantale; module action

References:

[1]	Joyal, Memoirs of the American Mathematical Society 309 (1984)
[2]	DOI: 10.1016/0304-3975(88)90100-4 · Zbl 0648.68016
[3]	DOI: 10.1016/0020-0190(87)90106-2 · Zbl 0622.68025
[4]	DOI: 10.1007/BFb0036900
[5]	DOI: 10.1145/828.833 · Zbl 0628.68025
[6]	DOI: 10.2307/1990008 · Zbl 0021.10801
[7]	Vickers, Topology via Logic (1989) · Zbl 0668.54001
[8]	Blamey, Topology and Category Theory in Computer Science pp 29– (1991) · Zbl 0792.68089
[9]	Rosenthal, Quantales and their Applications (1990)
[10]	Baeten, Ready trace semantics for concrete process algebra with priority operator (1985)
[11]	DOI: 10.1007/BFb0015727
[12]	Abramsky, Quantales, Observational Logic and Process Semantics (1990)
[13]	DOI: 10.1016/0304-3975(87)90117-4 · Zbl 0626.68011
[14]	DOI: 10.1016/0168-0072(91)90065-T · Zbl 0737.03006
[15]	Park, Springer Lecture Notes in Computer Science 104 (1981)
[16]	DOI: 10.1016/0304-3975(87)90065-X · Zbl 0626.68016
[17]	DOI: 10.1007/BF00268075 · Zbl 0569.68019
[18]	DOI: 10.1017/S0305004100065403 · Zbl 0658.06007
[19]	Hoare, Communicating Sequential Processes (1985) · Zbl 0637.68007
[20]	Hennessy, Concurrency and Nets pp 233– (1987)
[21]	DOI: 10.1145/2455.2460 · Zbl 0629.68021
[22]	Hennessy, Algebraic Theory of Processes (1988) · Zbl 0744.68047
[23]	Girard, Proofs and Types (1989)
[24]	Girard, Contemporary Mathematics 92 pp 69– (1989)
[25]	DOI: 10.1016/0304-3975(87)90045-4 · Zbl 0625.03037
[26]	Dunn, Handbook of Philosophical Logic III: Alternatives to Classical Logic pp 117– (1986)
[27]	DeNicola, Springer Lecture Notes in Computer Science 249 pp 138– (1987)
[28]	Conway, Regular Algebra and Finite Machines (1971) · Zbl 0231.94041
[29]	DOI: 10.1016/0001-8708(72)90002-3 · Zbl 0232.18009
[30]	Milner, Communication and Concurrency (1989)
[31]	Milner, Springer Lecture Notes in Computer Science (1980)
[32]	Mac Lane, Categories for the Working Mathematician (1971)
[33]	DOI: 10.2307/2310058 · Zbl 0080.00702
[34]	Johnstone, Stone Spaces (1982)