Advertisement

On the complexity of equation solving in process algebra

  • Bengt Jonsson
  • Kim Guldstrand Larsen
CAAP Colloquium On Trees In Algebra And Programming
Part of the Lecture Notes in Computer Science book series (LNCS, volume 493)

Abstract

The problem of designing a system which in a given environment 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$$
where 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.

References

  1. [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
  2. [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
  3. [BK85]
    J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.Google Scholar
  4. [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
  5. [Bou85]
    G. Boudol. Calcul de processus et verification. Technical Report 424, INRIA, 1985.Google Scholar
  6. [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
  7. [GJ79]
    Garey and Johnson. Computers and Intractability: A guide to the Theory of NP-Completeness. Freeman, 1979.Google Scholar
  8. [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
  9. [Hoa78]
    C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8), 1978.Google Scholar
  10. [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
  11. [Koo85]
    C. Koomen. Algebraic specification and verification of protocols. Science of Computer Programming, 5(1):1–36, 1985.Google Scholar
  12. [KS]
    Kannellakis and Smolka. CCS expressions, finite state processes, and three problems of equivalence. To appear in Information and Computation.Google Scholar
  13. [Lar90]
    K.G. Larsen. Modal specifications. Lecture Notes in Computer Science, 407, 1990.Google Scholar
  14. [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
  15. [LQ90]
    P. Lewis and H. Qin. Factorization of finite state machines under observational equivalence. Lecture Notes in Computer Science, 458, 1990.Google Scholar
  16. [LT88]
    Kim G. Larsen and Bent Thomsen. A modal process logic. In Proceedings on Logic in Computer Science, 1988.Google Scholar
  17. [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
  18. [LX90b]
    K.G. Larsen and L. Xinxin. Equation solving using modal transition systems. In Proceedings on Logic in Computer Science, 1990.Google Scholar
  19. [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
  20. [Mil80]
    R. Milner. Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.Google Scholar
  21. [Mil83]
    R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25, 1983.Google Scholar
  22. [Mil89]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  23. [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
  24. [Par81]
    D. Park. Concurrency and automata on infinite sequences. Lecture Notes in Computer Science, 104, 1981. in Proc. of 5th GI Conf.Google Scholar
  25. [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
  26. [Par89]
    J. Parrow. Submodule construction as equation solving in CCS. Theoretical Computer Science, 68:175–202, 1989.Google Scholar
  27. [Plo81]
    G. Plotkin. A structural approach to operational semantics. FN 19, DAIMI, Aarhus University, Denmark, 1981.Google Scholar
  28. [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
  29. [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
  30. [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
  31. [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

Authors and Affiliations

  • Bengt Jonsson
    • 1
  • Kim Guldstrand Larsen
    • 2
  1. 1.Swedish Institute of Computer ScienceKistaSweden
  2. 2.Department of Mathematics and Computer ScienceAalborg UniversityAalborgDenmark

Personalised recommendations