Skip to main content

Analysing AWN-specifications using mCRL2 (extended abstract)


Rob van Glabbeek, Peter Hoefner and Djurre van der Wal



We develop and implement a translation from the process Algebra for Wireless Networks (AWN) into the milli Common Representation Language (mCRL2). As a consequence of the translation, the sophisticated toolset of mCRL is now available for AWN-specifications. We show that the translation respects strong bisimilarity; hence all safety properties can be automatically checked using the toolset. To show usability of our translation we report on a case study.

BibTeX Entry

    publisher        = {Springer},
    doi              = {10.1007/978-3-319-98938-9\_23},
    series           = {Lecture Notes in Computer Science},
    booktitle        = {14th International Conference on integrated Formal Methods},
    author           = {van Glabbeek, Rob and Hoefner, Peter and van der Wal, Djurre},
    month            = sep,
    volume           = {11023},
    editor           = {{Carlo A. Furia, Kirsten Winter}},
    keywords         = {process algebra; model checking; awn; mcrl2},
    year             = {2018},
    date             = {2018-9-5},
    title            = {Analysing {AWN}-specifications using {mCRL2} (extended abstract)},
    pages            = {398-418},
    address          = {Maynooth}


Served by Apache on Linux on seL4.