uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Undecidable verification problems for programs with unreliable channels
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Computer Systems.
1996 (English)In: Automata, Languages and Programming: Proceedings of ICALP 94 / [ed] Serge Abiteboul, Eli Shamir, 1996, Vol. 130, no 1, 71-90 p.Conference paper, Published paper (Refereed)
Abstract [en]

We consider the verification of a particular class of infinite-state systems, namely systems consisting of finite-state processes that communicate via unbounded lossy FIFO channels. This class is able to model e.g. link protocols such as the Alternating Bit Protocol and HDLC. In an earlier paper, we showed that several interesting verification problems are decidable for this class of systems, namely (1) the reachability problem: is a set of states reachable from some other state of the system, (2) safety property over traces formulated as regular sets of allowed finite traces, and (3) eventuality properties: do all computations of a system eventually reach a given set of states. In this paper, we show that the following problems are undecidable, namely

  • The model checking problem in propositional temporal logics such as Propositional Linear Time Logic (PTL) and Computation Tree Logic (CTL).

  • The problem of deciding eventuality properties with fair channels: do all computations eventually reach a given set of states if the unreliable channels are fair in the sense that they deliver infinitely many messages if infinitely many messages are transmitted. This problem can model the question of whether a link protocol, such as HDLC, will eventually reliably transfer messages across a medium that is not permanently broken.

The results are obtained through a reduction from a variant of Post's Correspondence Problem.

Place, publisher, year, edition, pages
1996. Vol. 130, no 1, 71-90 p.
Series
Lecture Notes in Computer Science, ISSN 03 ; 820
Keyword [en]
CONTEXT-FREE PROCESSES; FINITE STATE MACHINES; AUTOMATIC VERIFICATION; SYSTEMS
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:uu:diva-27215DOI: 10.1007/3-540-58201-0_78ISBN: 978-3-540-58201-4 (print)ISBN: 978-3-540-48566-7 (print)OAI: oai:DiVA.org:uu-27215DiVA: diva2:55109
Conference
21st International Colloquium, ICALP 94 Jerusalem, Israel, July 11–14, 1994
Available from: 2008-10-17 Created: 2008-10-17 Last updated: 2013-10-03Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text

Authority records BETA

Abdulla, Parosh AzizJonsson, Bengt

Search in DiVA

By author/editor
Abdulla, Parosh AzizJonsson, Bengt
By organisation
Department of Computer Systems
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 417 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf