# On the complexity of equation solving in process algebra

CAAP Colloquium On Trees In Algebra And Programming

First Online:

## Abstract

The problem of designing a system which in a given environment where

*C*should satisfy a given specification*S*can be formulated as “find a system*P*such that*C*(*P*) satisfies the specification*S*”. In process algebra, such problems take the form of equations. We investigate the complexity of solving such equations in process algebra. We consider the problem of deciding whether there is a process*P*which satisfies an equation of one of the following forms:$$C(P) \sim QC(P) \triangleleft S(A|P)\backslash L \sim B(A|P)\backslash L \approx B$$

*C*is an arbitrary context of some process algebra,*A, B*and*Q*are given processes,*S*is a modal specification, ∼ (≈) is (weak) bisimulation equivalence, ⊲ is refinement between modal specifications (a generalization of bisimulation equivalence), and | and ∖L is the parallel and restriction operator of CCS respectively. The main result is that all four problems are PSPACE-hard in the size of the given contexts, processes and specifications. We also give constraints under which the first and third problem can be solved in polynomial time.## Keywords

Polynomial Time Transition System Inference Rule Winning Strategy Label Transition System
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.

Download
to read the full conference paper text

## References

- [BHR84]S.D. Brookes, C.A.R. Hoare, and A.W. Roscoe. A theory of communicating sequential processes.
*J. ACM*, 31(3):560–599, 1984.Google Scholar - [BK84]J Bergstra and J Klop. Verification of an alternating bit protocol by means of process algebra. Technical report, Centrum voor Wiskunde en Informatica, 1984.Google Scholar
- [BK85]J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction.
*Theoretical Computer Science*, 37:77–121, 1985.Google Scholar - [BL90]Gérard Boudol and Kim G. Larsen. Graphical versus logical specifications.
*Lecture Notes in Computer Science*, 431, 1990. In Proceedings of CAAP90.Google Scholar - [Bou85]G. Boudol. Calcul de processus et verification. Technical Report 424, INRIA, 1985.Google Scholar
- [CE82]E. Clarke and E.A. Emerson. Using branching time temporal logic to synthesize synchronization skeletons.
*Science of Computer Programming*, 2:241–266, 1982.Google Scholar - [GJ79]Garey and Johnson.
*Computers and Intractability: A guide to the Theory of NP-Completeness*. Freeman, 1979.Google Scholar - [HL89]Hans Hüttel and Kim G. Larsen. The use of static constructs in a modal process logic.
*Lecture Notes in Computer Science*, 363, 1989.Google Scholar - [Hoa78]C.A.R. Hoare. Communicating sequential processes.
*Communications of the ACM*, 21(8), 1978.Google Scholar - [JL91]B. Jonsson and K.G. Larsen. On the complexity of equation solving in process algebra. Technical report, Swedish Institute of Computer Science, 1991.Google Scholar
- [Koo85]C. Koomen. Algebraic specification and verification of protocols.
*Science of Computer Programming*, 5(1):1–36, 1985.Google Scholar - [KS]Kannellakis and Smolka. CCS expressions, finite state processes, and three problems of equivalence. To appear in Information and Computation.Google Scholar
- [Lar90]K.G. Larsen. Modal specifications.
*Lecture Notes in Computer Science*, 407, 1990.Google Scholar - [LM87]Kim G. Larsen and Robin Milner. Verifying a protocol using relativized bisimulation. In
*Proc. ICALP '87*, volume 267 of*Lecture Notes of Computer Science*. Springer Verlag, 1987.Google Scholar - [LQ90]P. Lewis and H. Qin. Factorization of finite state machines under observational equivalence.
*Lecture Notes in Computer Science*, 458, 1990.Google Scholar - [LT88]Kim G. Larsen and Bent Thomsen. A modal process logic. In
*Proceedings on Logic in Computer Science*, 1988.Google Scholar - [LX90a]K.G. Larsen and L. Xinxin. Compositionality through an operational semantics of contexts.
*Lecture Notes in Computer Science*, 1990. To appear in Proceedings of ICALP90.Google Scholar - [LX90b]K.G. Larsen and L. Xinxin. Equation solving using modal transition systems. In
*Proceedings on Logic in Computer Science*, 1990.Google Scholar - [MB83]Philip Merlin and Gregor von Bochmann. On the construction of submodule specifications and communication protocols.
*ACM Transactions on Programming Languages and Systems*, 5(1):1–25, 1983.Google Scholar - [Mil80]R. Milner.
*Calculus of Communicating Systems*, volume 92 of*Lecture Notes in Computer Science*. Springer Verlag, 1980.Google Scholar - [Mil83]R. Milner. Calculi for synchrony and asynchrony.
*Theoretical Computer Science*, 25, 1983.Google Scholar - [Mil89]R. Milner.
*Communication and Concurrency*. Prentice-Hall, 1989.Google Scholar - [MW84]Zohar Manna and Pierre Wolper. Synthesis of communicating processes from temporal logic specifications.
*ACM Transactions on Programming Languages and Systems*, 6(1):68–93, 1984.Google Scholar - [Par81]D. Park. Concurrency and automata on infinite sequences.
*Lecture Notes in Computer Science*, 104, 1981. in Proc. of 5th GI Conf.Google Scholar - [Par87]Joachim Parrow. Verifying a csma/cd-protocol with ccs. Technical Report ECS-LFCS-87-18, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, 1987. To appear in
*Protocol Specification, Testing, and Verification VIII (1988)*.Google Scholar - [Par89]J. Parrow. Submodule construction as equation solving in CCS.
*Theoretical Computer Science*, 68:175–202, 1989.Google Scholar - [Plo81]G. Plotkin. A structural approach to operational semantics. FN 19, DAIMI, Aarhus University, Denmark, 1981.Google Scholar
- [Pnu85]A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems.
*Lecture Notes in Computer Science*, 194, 1985. in Proc. of ICALP'87.Google Scholar - [PR89]A. Pnueli and R. Rossner. On the synthesis of a reactive module. In
*Proc. 16:th ACM Symp. on Principles of Programming Languages*, pages 179–190, 1989.Google Scholar - [SFD85]S.A. Smolka, A.J. Frank, and S.K. Debray. Testing protocol robustness the CCS way. In
*Protocol Specification, Testing, and Verification IV (1984)*, pages 93–108, 1985. North-Holland.Google Scholar - [Shi89]M.W. Shields. A note on the simple interface equation.
*The Computer Journal*, 32(5), 1989.Google Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1991