Data Communicating Processes with Unreliable Channels
2016 (English)In: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), 2016, 166-175 p.Conference paper (Refereed)
We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.
Place, publisher, year, edition, pages
2016. 166-175 p.
Reachability Problem, Lossy Channel Systems
IdentifiersURN: urn:nbn:se:uu:diva-311415DOI: 10.1145/293355.2934535ISI: 000387609200017ISBN: 9781450343916OAI: oai:DiVA.org:uu-311415DiVA: diva2:1060006
31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS), JUL 05-08, 2016, New York City, NY