Modelling MAC-Layer Communications in Wireless Systems
We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2015-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1138/pdf |
| _version_ | 1797268660567408640 |
|---|---|
| author | Andrea Cerone Matthew Hennessy Massimo Merro |
| author_facet | Andrea Cerone Matthew Hennessy Massimo Merro |
| author_sort | Andrea Cerone |
| collection | DOAJ |
| description | We present a timed process calculus for modelling wireless networks in which
individual stations broadcast and receive messages; moreover the broadcasts are
subject to collisions. Based on a reduction semantics for the calculus we
define a contextual equivalence to compare the external behaviour of such
wireless networks. Further, we construct an extensional LTS (labelled
transition system) which models the activities of stations that can be directly
observed by the external environment. Standard bisimulations in this LTS
provide a sound proof method for proving systems contextually equivalence. We
illustrate the usefulness of the proof methodology by a series of examples.
Finally we show that this proof method is also complete, for a large class of
systems. |
| first_indexed | 2024-04-25T01:36:01Z |
| format | Article |
| id | doaj.art-c837d91808b2423287ff141335c2727c |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:01Z |
| publishDate | 2015-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c837d91808b2423287ff141335c2727c2024-03-08T09:38:50ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742015-03-01Volume 11, Issue 110.2168/LMCS-11(1:18)20151138Modelling MAC-Layer Communications in Wireless SystemsAndrea Ceronehttps://orcid.org/0000-0003-1349-6693Matthew HennessyMassimo Merrohttps://orcid.org/0000-0002-1712-7492We present a timed process calculus for modelling wireless networks in which individual stations broadcast and receive messages; moreover the broadcasts are subject to collisions. Based on a reduction semantics for the calculus we define a contextual equivalence to compare the external behaviour of such wireless networks. Further, we construct an extensional LTS (labelled transition system) which models the activities of stations that can be directly observed by the external environment. Standard bisimulations in this LTS provide a sound proof method for proving systems contextually equivalence. We illustrate the usefulness of the proof methodology by a series of examples. Finally we show that this proof method is also complete, for a large class of systems.https://lmcs.episciences.org/1138/pdfcomputer science - logic in computer science |
| spellingShingle | Andrea Cerone Matthew Hennessy Massimo Merro Modelling MAC-Layer Communications in Wireless Systems Logical Methods in Computer Science computer science - logic in computer science |
| title | Modelling MAC-Layer Communications in Wireless Systems |
| title_full | Modelling MAC-Layer Communications in Wireless Systems |
| title_fullStr | Modelling MAC-Layer Communications in Wireless Systems |
| title_full_unstemmed | Modelling MAC-Layer Communications in Wireless Systems |
| title_short | Modelling MAC-Layer Communications in Wireless Systems |
| title_sort | modelling mac layer communications in wireless systems |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/1138/pdf |
| work_keys_str_mv | AT andreacerone modellingmaclayercommunicationsinwirelesssystems AT matthewhennessy modellingmaclayercommunicationsinwirelesssystems AT massimomerro modellingmaclayercommunicationsinwirelesssystems |