Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Problem Solving Using Process Algebra Considered Insightful

  • Chapter
  • First Online:
ModelEd, TestEd, TrustEd

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10500))

Abstract

Process algebras with data, such as LOTOS, PSF, FDR, and mCRL2, are very suitable to model and analyse combinatorial problems. Contrary to more traditional mathematics, many of these problems can very directly be formulated in process algebra. Using a wide range of techniques, such as behavioural reductions, model checking, and visualisation, the problems can subsequently be easily solved. With the advent of probabilistic process algebras this also extends to problems where probabilities play a role. In this paper we model and analyse a number of very well-known – yet tricky – problems and show the elegance of behavioural analysis.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 15.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

Similar content being viewed by others

Notes

  1. 1.

    The tools are by Olav Bunte (evaluation of modal formulas on probabilistic transition systems) and Ferry Timmers (probabilistic trace reduction).

References

  1. Hadley, J., Singmaster, D.: Problems to sharpen the young. Math. Gaz. 76(475), 102–126 (1992). doi:10.2307/3620384

    Article  Google Scholar 

  2. Bekič, H.: Towards a mathematical theory of processes. Technical report TR25.125, IBM Laboratory, Vienna (1971). Also appeared in Jones, C.B. (ed.) Programming Languages and Their Definition, Lecture Notes in Computer Science, vol. 177. Springer (1984)

    Google Scholar 

  3. Bergstra, J.A., Klop, J.W.: Fixed point semantics in process algebras. Report IW 206, Mathematisch Centrum, Amsterdam (1982)

    Google Scholar 

  4. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Comput. 60(1/3), 109–137 (1984)

    MathSciNet  MATH  Google Scholar 

  5. Biemans, F., Blonk, P.: On the formal specification and verification of CIM architectures using LOTOS. Comput. Ind. 7(6), 491–504 (1986)

    Article  Google Scholar 

  6. Blackburn, P., van Benthem, J., Wolter, F. (eds.): Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier, Amsterdam (2007)

    MATH  Google Scholar 

  7. Brinksma, E., Karjoth, G.: A specification of the OSI transport service in LOTOS. In: Yemini, Y., Strom, R.E., Yemini, S. (eds.) Protocol Specification, Testing and Verification IV, pp. 227–251. North-Holland, Amsterdam (1984)

    Google Scholar 

  8. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774

    Chapter  Google Scholar 

  9. van Ditmarsch, H., van der Hoek, W., Kooij, B.: Dynamic Epistemic Logic. Studies in Epistemology, Logic, Methodology, and Philosophy of Science, vol. 337. Springer, Heidelberg (2008). doi:10.1007/978-1-4020-5839-4

    MATH  Google Scholar 

  10. Dijkstra, E.W.: Pruning the search tree. EWD1255. www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1255.html. Accessed June 2017

  11. van Emde Boas, P., Groenendijk, J., Stokhof, M.: The conway paradox: its solution in an epistemic framework. In: Groenendijk, J., Janssen, T.M.V., Stokhof, M. (eds.) Truth, Interpretation, and Information: Selected Papers from the Third Amsterdam Colloquium, pp. 159–182. Foris Publications, New York (1984)

    Google Scholar 

  12. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013)

    Article  MATH  Google Scholar 

  13. Gardner, M.: My Best Mathematical and Logic Puzzles. Dover, Downers Grove (1994)

    MATH  Google Scholar 

  14. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_13

    Chapter  Google Scholar 

  15. Cranen, S., Groote, J.F., Reniers, M.A.: A linear translation from CTL* to the first-order modal \(\mu \)-calculus. Theoret. Comput. Sci. 412(28), 3129–3139 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  16. Groote, J.F., van Ham, F.: Interactive visualization of large state spaces. Int. J. Softw. Tools Technol. Transf. 8(1), 77–91 (2006)

    Article  Google Scholar 

  17. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communication Systems. The MIT Press, Cambridge (2014). (See for the toolset www.mcrl2.org)

    MATH  Google Scholar 

  18. Groote, J.F., Ponse, A.: The syntax and semantics of \(\mu \)CRL. Report CS-R9076, CWI, Amsterdam (1990)

    Google Scholar 

  19. Grünwald, P., Halpern, J.Y.: Updating probabilities. In: Darwiche, A., Friedman, N. (eds.) Uncertainty in Artificial Intelligence, pp. 187–196. Morgan Kaufman, Burlington (2002)

    Google Scholar 

  20. Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980). doi:10.1007/3-540-10003-2_79

    Chapter  Google Scholar 

  21. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  MATH  Google Scholar 

  22. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall International, Upper Saddle River (1985)

    MATH  Google Scholar 

  23. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theoret. Comput. Sci. 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  24. ISO 8807:1989. Information processing systems - Open Systems Interconnection - LOTOS - A formal description technique based on the temporal ordering of observational behaviour. ISO/IECJTC1/SC7 (1989)

    Google Scholar 

  25. Milner, R.: An approach to the semantics of parallel programs. In: Proceedings Convegno di Informatica Teorica, pp. 283–302, Pisa (1973)

    Google Scholar 

  26. Mauw, S., Veltink, G.J.: A process specification formalism. Fundam. Inform. XIII, 85–139 (1990)

    MATH  Google Scholar 

  27. Milner, R.: Processes: a mathematical model of computing agents. In: Rose, H.E., Shepherdson, J.C. (eds.) Proceedings Logic Colloquium 1972, pp. 158–173. North-Holland, Amsterdam (1973)

    Google Scholar 

  28. Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  29. Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46–57. IEEE, Piscataway (1977)

    Google Scholar 

  30. Prior, A.N.: Time and Modality. Oxford University Press, Oxford (1957)

    MATH  Google Scholar 

  31. Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010). doi:10.1007/978-1-84882-258-0

    Book  MATH  Google Scholar 

  32. van Sinderen, M., Ajubi, I., Caneschi, F.: The application of LOTOS for the formal description of the ISO session layer. In: Turner, K.J. (ed.) Formal Description Techniques, pp. 263–277. North-Holland, Amsterdam (1989)

    Google Scholar 

  33. Winkler, P.: Mathematical Puzzles. A Connaisseur’s Collection. A.K. Peters, Natick (2004)

    MATH  Google Scholar 

Download references

Acknowledgment

The authors are grateful to the reviewers for their constructive and inspiring comments.

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands

    Jan Friso Groote & Erik P. de Vink

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erik P. de Vink
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Friso Groote .

Editor information

Editors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  2. University of Twente, Enschede, The Netherlands

    Rom Langerak

  3. University of Twente, Enschede, The Netherlands

    Arend Rensink

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Groote, J.F., de Vink, E.P. (2017). Problem Solving Using Process Algebra Considered Insightful. In: Katoen, JP., Langerak, R., Rensink, A. (eds) ModelEd, TestEd, TrustEd. Lecture Notes in Computer Science(), vol 10500. Springer, Cham. https://doi.org/10.1007/978-3-319-68270-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-68270-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-68269-3

  • Online ISBN: 978-3-319-68270-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation