Skip to main content
SpringerLink
Log in

Ideal specification formalism = expressivity + compositionality + decidability + testability + ...

  • Invited Lectures
  • Conference paper
  • First Online:
CONCUR '90 Theories of Concurrency: Unification and Extension (CONCUR 1990)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 458))

Included in the following conference series:

Abstract

For the comparison of specification formalisms several criteria may be applied. In this paper we concentrate on the formalization of expressivity and compositionality. We apply these criteria to a number of specification formalisms ranging from behavioural formalisms (based on labelled transition systems) to logical formalisms (based on Hennessy-Milner logic). A main result of the paper is that a specification formalism must be at least as expressive as Hennessy-Milner Logic in order for specifications to be decomposable. Another main result is that implicit behavioural specifications are at least as expressive as logical specifications and do allow specifications to be decomposed. We also present specification formalisms for probabilistic processes, and evaluate these with respect to compositionality.

On leave from Aalborg University, Denmark

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77–121, 1985.

    Google Scholar 

  2. Gérard Boudol and Kim G. Larsen. Graphical versus logical specifications. Lecture Notes in Computer Science, 431, 1990. In Proceedings of CAAP90.

    Google Scholar 

  3. Meyer Bloom, Istrail. bisimulation can't be traced. Proceedings of Principles of Programming Languages, 1988.

    Google Scholar 

  4. G. Boudol. Calcul de processus et verification. Technical Report 424, INRIA, 1985.

    Google Scholar 

  5. Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. Lecture Notes in Computer Science, 1990. In Proceedings of CONCUR'90.

    Google Scholar 

  6. R. de Simone. Higher-level synchronising devices in MEIJE-CCS. Theoretical Computer Science, 37, 1985.

    Google Scholar 

  7. A. Giacalone, C.C. Jou, and S.A. Smolka. Algebraic reasoning for probabilistic concurrent systems. 1990. In Proceedings of Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990, IFIP TC 2.

    Google Scholar 

  8. J.F. Groote and F. Vaandrager. Structured operational semantics and bisimulation as a congruence. Lecture Notes in Computer Science, 372, 1989. In Proceedings of ICALP'89.

    Google Scholar 

  9. 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 

  10. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery, pages 137–161, 1985.

    Google Scholar 

  11. C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8), 1978.

    Google Scholar 

  12. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.

    Google Scholar 

  13. C.C. Jou and S.A. Smolka. Equivalences, congruences, and complete axiomatizations for probabilistic processes. Lecture Notes in Computer Science, 1990. In Proceedings of CONCUR'90.

    Google Scholar 

  14. K.G. Larsen. Context-Dependent Bisimulation Between Processes. PhD thesis, University of Edinburgh, Mayfield Road, Edinburgh, Scotland, 1986.

    Google Scholar 

  15. K.G. Larsen. A context dependent bisimulation between processes. Theoretical Computer Science, 49, 1987.

    Google Scholar 

  16. Kim G. Larsen. Compositional theories based on an operational semantics of contexts. Lecture Notes in Computer Science, 430, 1989. In proceedings of REX workshop on Stepwise Refinement of Distributed Systems.

    Google Scholar 

  17. K.G. Larsen. Modal specifications. Lecture Notes in Computer Science, 407, 1990.

    Google Scholar 

  18. K.G. Larsen and R. Milner. Verifying a protocol using relativized bisimulation. Lecture Notes in Computer Science, 267, 1987. In Proceedings of ICALP'87.

    Google Scholar 

  19. K.G. Larsen and A. Skou. Bisimulation through probabilistic testing. Proceedings of Principles of Programming Languages, 1989.

    Google Scholar 

  20. Kim G. Larsen and Bent Thomsen. A modal process logic. In Proceedings on Logic in Computer Science, 1988.

    Google Scholar 

  21. 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 

  22. K.G. Larsen and L. Xinxin. Equation solving using modal transition systems. In Proceedings on Logic in Computer Science, 1990.

    Google Scholar 

  23. R. Milner. Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer Verlag, 1980.

    Google Scholar 

  24. R. Milner. Calculi for synchrony and asynchrony. Theoretical Computer Science, 25, 1983.

    Google Scholar 

  25. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  26. D. Park. Concurrency and automata on infinite sequences. Lecture Notes in Computer Science, 104, 1981. in Proc. of 5th GI Conf.

    Google Scholar 

  27. G. Plotkin. A structural approach to operational semantics. FN 19, DAIMI, Aarhus University, Denmark, 1981.

    Google Scholar 

  28. 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. S.A. Smolka R. van Glabbeek, B. Steffen and C.M.N. Tofts. Reactive, generative, and stratified models of probabilistic processes. Logic in Computer Science, 1990.

    Google Scholar 

  30. Arne Skou. Validation of Concurrent Processes, with emphasis on testing. PhD thesis, Aalbog University Center, Denmark, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SICS, Box 1263, S-164 28, Kista, Sweden

    Kim Guldstrand Larsen

Authors
  1. Kim Guldstrand Larsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. C. M. Baeten J. W. Klop

Rights and permissions

Reprints and permissions

Copyright information

© 1990 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Guldstrand Larsen, K. (1990). Ideal specification formalism = expressivity + compositionality + decidability + testability + .... In: Baeten, J.C.M., Klop, J.W. (eds) CONCUR '90 Theories of Concurrency: Unification and Extension. CONCUR 1990. Lecture Notes in Computer Science, vol 458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039050

Download citation

  • DOI: https://doi.org/10.1007/BFb0039050

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-53048-0

  • Online ISBN: 978-3-540-46395-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation