Logic of trace languages

Extended abstract
  • Alexander Rabinovich
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


Usually, laws established in process calculi have the format of equations and/or inequations between process-terms. Though such set of laws captures important properties of the underlying algebra it cannot reveal some basic logical properties of the algebra. From the logical point of view, the consequence relation associated with an algebra is much more fundamental than the set of laws valid in it. That is why in this paper our main concern is about consequence relation which provides the answer to questions in the following format (the formalization is in terms of sequents): what terms are equal under the assumption that some other pairs of terms are equal. We compare two algebras: algebra of linear trace languages and algebra of relations. The fundamental operations in trace algebra are synchronization (parallel composition) of two trace languages, nondeterministic choice and hiding of a port in a language. The corresponding operations in relational algebra are join, union and projection. We show that these algebras have the same laws, i.e. two terms have the same meaning in all trace interpretations iff they have the same meaning in all relational interpretations. Moreover, we show that these algebras have the same consequence relations. We embed both algebras into first order logic and through this embedding obtain sound and complete proof systems for reasoning about the consequence relations in these algebras.


Consequence Relation Inference Rule Relational Semantic Order Logic Relational Algebra 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    A. Avron. Simple Consequence Relations. In Information and Computation, volume 92, 1991Google Scholar
  2. [2]
    G. Gentzen. Investigations into logical deduction. In The collected works of Gerhard Gentzen, (M. Szabo, Ed.), North-Holland, Amsterdam, 1969.Google Scholar
  3. [3]
    J.-Y. Girard. Linear Logic. In Theoretical Computer Science, 50(1):1–102, 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  4. [4]
    J. F. Groote. A new strategy for proving ω-completeness with applications in process algebra. In Proceedings of CONCUR 90, volume 458 of Lect. Notes in Computer Science. Springer Verlag, 1990.Google Scholar
  5. [5]
    M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.Google Scholar
  6. [6]
    P. C. Kanellakis. Elements of Relational Database Theory. In Handbook of Theoretical Computer Science, North-Holland, 1989.Google Scholar
  7. [7]
    R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.zbMATHGoogle Scholar
  8. [8]
    R. Milner. A complete proof system for a class of regular behaviors. In JCSS, volume 28, pp 439–466, 1984.zbMATHMathSciNetGoogle Scholar
  9. [9]
    R. Milner. A complete axiomatisation for observational Congruence of finite state behaviors. In Information and Computation, volume 81, pp 227–247, 1989.zbMATHMathSciNetCrossRefGoogle Scholar
  10. [10]
    A. Rabinovich and B. A. Trakhtenbrot. Communication among relations. In International Conference on Automata, Languages and Programming, volume 443 of Lect. Notes in Computer Science. Springer Verlag, 1990.Google Scholar
  11. [11]
    A. Rabinovich and B. A. Trakhtenbrot. On Nets, Algebras and Modularity. In International Conference on Theoretical Aspects of Computer Software, to appear in Lect. Notes in Computer Science. Springer Verlag, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Alexander Rabinovich
    • 1
  1. 1.IBM Research DivisionT.J. Watson Research CenterYorktown Heights

Personalised recommendations