Model checking processes specified in join-calculus algebra

Sławomir Piotr Maludziński, Grzegorz Dobrowolski


This article presents a model checking tool used to verify concurrent systems specified in join-calculus algebra. The temporal properties of systems under verification are expressed in CTL logic. Join-calculus algebra with its operational semantics defined by the chemical abstract machine serves as the basic method for the specification of concurrent systems and their synchronization mechanisms, and allows the examination of more complex systems.


join-calculus, model checking, formal methods, authomatic software verification

Full Text:



Aaby A. A.: Compiler Construction using Flex and Bison. Walla Walla College, 2003.

Baier C., Katoen J. P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. ISBN 026202649X, 9780262026499.

Ben-Ari M.: Mathematical Logic for Computer Science. Prentice-Hall International Series in Computer Science. Springer, 2001. ISBN 9781852333195, URL

Ben-Ari M., Manna Z., Pnueli A.: The Temporal Logic of Branching Time. In:Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’81, pp. 164–176. ACM, New York, NY, USA, 1981. ISBN 0-89791-029-X. URL

Berry G., Boudol G.: The Chemical Abstract Machine. In: POPL ’90: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 81–94. ACM, New York, NY, USA, 1990. ISBN 0-89791-343-4. URL

Cimatti A., Clarke E., Giunchiglia E., Giunchiglia F., Pistore M., Roveri M., Sebastiani R., Tacchella A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Proc. International Conference on Computer-Aided Verification (CAV 2002), LNCS, vol. 2404. Springer, Copenhagen, Denmark, 2002.

Dennis L. A., Fisher M., Webster M. P., Bordini R. H.: Model Checking Agent Programming Languages. Automated Software Engg., 19(1): 5–63, 2012. ISSN 0928-8910. URL

Edmund M., Clarke J., Grumberg O., Peled D. A.: Model Checking. MIT Press, Cambridge, MA, USA, 1999. ISBN 0-262-03270-8.

Ferrari G. L., Montanari U., Tuosto E.: Model Checking for Nominal Calculi. In: Proceedings of the 8th International Conference on Foundations of Software Science and Computation Structures, FOSSACS’05, pp. 1–24. Springer-Verlag, Berlin, Heidelberg, 2005. ISBN 3-540-25388-2, 978-3-540-25388-4. URL

Fournet C., Gonthier G.: The Reflexive CHAM and the Join-calculus. In: POPL’96: Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 372–385. ACM, New York, NY, USA, 1996. ISBN 0-89791-769-3. URL

Fournet C., Gonthier G., Lévy J. J., Maranget L., Rémy D.: A Calculus of Mobile Agents. In: Proceedings of the 7th International Conference on Concurrency Theory (CONCUR’96), pp. 406–421. Springer-Verlag, 1996. URL

Grumberg O., Veith H., eds.: 25 Years of Model Checking – History, Achievements, Perspectives, Lecture Notes in Computer Science, vol. 5000. Springer, 2008. ISBN 978-3-540-69849-4.

Herlihy M., Shavit N.: The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2008. ISBN 0123705916, 9780123705914.

Holzmann G.: SPIN Model Checker, Primer and Reference Manual. 1 st. ed. Addison-Wesley Professional, 2003. ISBN 0-321-22862-6.

Burch J. R., Clarke E. M., McMillan K. L., Dill D. L., Hwang L. J.: Symbolic Model Checking: 10 20 States and Beyond. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C., 1990. URL

Niewiadomski A., Penczek W., Szreter M.: A Model Checker for Real Time and Multi-agent Systems. In: Proceedings of VerICS 2004, pp. 88–99. Humboldt University, 2004.



  • There are currently no refbacks.