Abstract
A key problem in mixing operational (e.g., process–algebraic) and declarative (e.g., logical) styles of specification is how to deal with inconsistencies arising when composing processes under conjunction. This paper introduces a conjunction operator on labelled transition systems capturing the basic intuition of “a and b = false”, and considers a naive preorder that demands that an inconsistent specification can only be refined by an inconsistent implementation.
The main body of the paper is concerned with characterising the largest precongruence contained in the naive preorder. This characterisation will be based on a novel semantics called ready–tree semantics, which refines ready traces but is coarser than ready simulation. It is proved that the induced ready–tree preorder is compositional and fully–abstract, and that the conjunction operator indeed reflects conjunction.
The paper’s results provide a foundation for, and an important step towards a unified framework that allows one to freely mix operators from process algebras and temporal logics.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Ready-trace semantics for concrete process algebra with the priority operator. Computer J 30(6), 498–506 (1987)
Bergstra, J.A., Ponse, A., Smolka, S.A.: Handbook of Process Algebra. Elsevier Science, Amsterdam (2001)
Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. J. ACM 42(1), 232–268 (1995)
Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)
Cleaveland, R., Lüttgen, G.: A semantic theory for heterogeneous system design. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol. 1974, pp. 312–324. Springer, Heidelberg (2000)
Cleaveland, R., Lüttgen, G.: A logical process calculus. In: EXPRESS 2002. ENTCS, vol. 68(2), Elsevier Science, Amsterdam (2002)
van Glabbeek, R.: The linear time – branching time spectrum II. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)
Graf, S., Sifakis, J.: A logic for the description of non-deterministic programs and their properties. Information and Control 68(1–3), 254–270 (1986)
Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)
Lamport, L.: The temporal logic of actions. TOPLAS 16(3), 872–923 (1994)
Lüttgen, G., Vogler, W.: Conjunction on processes: Full-abstraction via ready-tree semantics. Tech. Rep. YCS-2005-396, Dept. of Comp. Sci., Univ. of York, UK (2005)
De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes. TCS 34, 83–133 (1983)
Olderog, E.R.: Nets, Terms and Formulas. In: Cambridge Tracts in Theoretical Computer Science, vol. 23, Cambridge Univ. Press, Cambridge (1991)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lüttgen, G., Vogler, W. (2006). Conjunction on Processes: Full–Abstraction Via Ready–Tree Semantics. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_18
Download citation
DOI: https://doi.org/10.1007/11690634_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)