Undecidable verification problems for programs with unreliable channels

DOI10.1007/3-540-58201-0_78MaRDI QIDQ4632436zbMATH OpenOpenAlexFDO

Authors Parosh A. Abdulla, Bengt Jonsson

Publication date 29 April 2019

Published in Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58201-0_78

zbMATH Keywords

computation-tree logiceventuality propertylabeled transition systemmodel checkingsafety property

Mathematics Subject Classification ID

Temporal logic (03B44) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Undecidable verification problems for programs with unreliable channels
• Verifying programs with unreliable channels
• Unreliable channels are easier to verify than perfect channels
• Undecidable problems in unreliable computations.
• scientific article; zbMATH DE number 1759620

Cites work

• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Boundedness, empty channel detection, and synchronization for communicating finite automata
• Deciding bisimulation equivalences for a class of non-finite-state programs
• scientific article; zbMATH DE number 4043216 (Why is no real title available?)
• scientific article; zbMATH DE number 176728 (Why is no real title available?)
• scientific article; zbMATH DE number 176736 (Why is no real title available?)
• On Communicating Finite-State Machines
• On some variants of Post's correspondence problem
• Parallel program schemata
• Reasoning about systems with many processes
• Symbolic model checking: \(10^{20}\) states and beyond
• Undecidable verification problems for programs with unreliable channels
• Verifying programs with unreliable channels

Cited in

(23)

• Undecidable problems in unreliable computations.
• Communication errors in the \(\pi\)-calculus are undecidable
• Using forward reachability analysis for verification of lossy channel systems
• Unreliable channels are easier to verify than perfect channels
• Verifying programs with unreliable channels
• On termination and invariance for faulty channel machines
• Non-deterministic transducer models of retransmission protocols over noisy channels
• Unidirectional channel systems can be tested
• scientific article; zbMATH DE number 2086244 (Why is no real title available?)
• Mixing Lossy and Perfect Fifo Channels
• Undecidability of accordance for open systems with unbounded message queues
• scientific article; zbMATH DE number 1512704 (Why is no real title available?)
• scientific article; zbMATH DE number 1564050 (Why is no real title available?)
• Data communicating processes with unreliable channels
• scientific article; zbMATH DE number 1863156 (Why is no real title available?)
• scientific article; zbMATH DE number 7440191 (Why is no real title available?)
• Forward analysis for WSTS. III: Karp-Miller trees
• Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
• Well-structured transition systems everywhere!
• Undecidable verification problems for programs with unreliable channels
• TSO games -- on the decidability of safety games under the total store order semantics
• Reachability and safety games under TSO semantics
• TSO games -- on the decidability of safety games under the total store order semantics

This page was built for publication: Undecidable verification problems for programs with unreliable channels

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4632436)