Skip to main content
SpringerLink
Log in

Compositionality of Hennessy-Milner Logic through Structural Operational Semantics

  • Conference paper
Fundamentals of Computation Theory (FCT 2003)

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

Included in the following conference series:

Abstract

This paper presents a method for the decomposition of HML formulae. It can be used to decide whether a process algebra term satisfies a HML formula, by checking whether subterms satisfy certain formulae, obtained by decomposing the original formula. The method uses the structural operational semantics of the process algebra. The main contribution of this paper is that an earlier decomposition method from Larsen [14] for the De Simone format is extended to the more general ntyft/ntyxt format without lookahead.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Andersen, H.R., Stirling, C., Winskel, G.: Compositional proof system for the modal μ-calculus. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pp. 144–153. IEEE Computer Society Press, Paris (1994)

    Chapter  Google Scholar 

  2. Andersen, H.R., Winskel, G.: Compositional checking of satisfaction. Formal Methods in System Design 1(4), 323–354 (1992)

    Article  MATH  Google Scholar 

  3. Barringer, H., Kuiper, R., Pnueli, A.: Now you may compose temporal logic specifications. In: ACM Symposium on Theory of Computing (STOC 1984), pp. 51–63. ACM Press, Baltimore (1984)

    Chapter  Google Scholar 

  4. Bloom, B., Fokkink, W.J., van Glabbeek, R.J.:: Precongruence formats for decorated trace semantics. ACM Transactions on Computational Logic (2003) (to appear)

    Google Scholar 

  5. Bol, R., Groote, J.F.: The meaning of negative premises in transition system specifications. Journal of the ACM 43(5), 863–914 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  6. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. Journal of the ACM 31(3), 560–599 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  7. van Glabbeek, R.J.: The meaning of negative premises in transition system specifications II. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 502–513. Springer, Heidelberg (1996)

    Google Scholar 

  8. van Glabbeek, R.J.: The linear time – branching time spectrum I: The semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 1, pp. 3–99. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  9. Groote, J.F.: Transition system specifications with negative premises. Theoretical Computer Science 118(2), 263–299 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  10. Harel, D., Kozen, D., Parikh, R.: Process logic: Expressiveness, decidability, completeness. Journal of Computer and System Sciences 25(2), 144–170 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  11. Hennessy, M.C.B., Milner, R.: Algebraic laws for non-determinism and concurrency. Journal of the ACM 32(1), 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  12. Hennessy, M.C.B., Stirling, C.: The power of the future perfect in program logics. Information and Control 67(1-3), 23–52 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  13. Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27(3), 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  14. Larsen, K.G.: Context-Dependent Bisimulation between Processes. PhD thesis, University of Edinburgh, Edinburgh (1986)

    Google Scholar 

  15. Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. Journal of Logic and Computation 1(6), 761–795 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  16. Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    Google Scholar 

  17. Milner, R.: A modal characterization of observable machine-behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981. LNCS, vol. 112, pp. 25–34. Springer, Heidelberg (1981)

    Google Scholar 

  18. Milner, R.: Calculi for synchrony and asynchrony. Theoretical Computer Science 25(3), 267–310 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  19. Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark (1981)

    Google Scholar 

  20. Pnueli, A.: The temporal logic of concurrent programs. Theoretical Computer Science 13, 45–60 (1981)

    Article  MATH  MathSciNet  Google Scholar 

  21. De Simone, R.: Higher-level synchronising devices in Meije–SCCS. Theoretical Computer Science 37(3), 245–267 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  22. Stirling, C.: A proof-theoretic characterization of observational equivalence. Theoretical Computer Science 39(1), 27–45 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  23. Stirling, C.: A complete compositional modal proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 475–486. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  24. Stirling, C.: A complete modal proof system for a subset of SCCS. In: Nivat, M., Floyd, C., Thatcher, J., Ehrig, H. (eds.) CAAP 1985 and TAPSOFT 1985. LNCS, vol. 185, pp. 253–266. Springer, Heidelberg (1985)

    Google Scholar 

  25. Stirling, C.: Modal logics for communicating systems. Theoretical Computer Science 49(2-3), 311–347 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  26. Winskel, G.: A complete proof system for SCCS with modal assertions. Fundamenta Informaticae IX, 401–420 (1986)

    MathSciNet  Google Scholar 

  27. Winskel, G.: On the compositional checking of validity (extended abstract). In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 481–501. Springer, Heidelberg (1990)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Engineering, CWI, PO Box 94079, 1090 GB, Amsterdam, The Netherlands

    Wan Fokkink & Rob van Glabbeek

  2. Department of Theoretical Computer Science, Vrije Universiteit Amsterdam, De Boelelaan 1081a, 1081, Amsterdam HV, The Netherlands

    Wan Fokkink & Paulien de Wind

Authors
  1. Wan Fokkink
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rob van Glabbeek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paulien de Wind
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Lund University, 22100, Lund, Sweden

    Andrzej Lingas

  2. School of Technology and Society, Malmö University, SE-205 06, Malmö, Sweden

    Bengt J. Nilsson

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fokkink, W., van Glabbeek, R., de Wind, P. (2003). Compositionality of Hennessy-Milner Logic through Structural Operational Semantics. In: Lingas, A., Nilsson, B.J. (eds) Fundamentals of Computation Theory. FCT 2003. Lecture Notes in Computer Science, vol 2751. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45077-1_38

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45077-1_38

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40543-6

  • Online ISBN: 978-3-540-45077-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation