Unreliable channels are easier to verify than perfect channels

DOI10.1006/INCO.1996.0003zbMath0844.68035OpenAlexW1985925577MaRDI QIDQ1908353

Alain Finkel, S. Purushothaman Iyer, Gérard Cécé

Publication date: 27 March 1996

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/ca36046e1bfcedc91db31991e877875e4f48e668

zbMATH Keywords

reachabilityunboundednessdeadlockmodel-checking against CTL\(^*\)

Mathematics Subject Classification ID

Related Items (30)

Zeno, Hercules, and the Hydra ⋮ Unnamed Item ⋮ The inclusion structure of partially lossy queue monoids and their trace submonoids ⋮ Rational, recognizable, and aperiodic partially lossy queue languages ⋮ The transformation monoid of a partially lossy queue ⋮ Unnamed Item ⋮ Handling infinitely branching well-structured transition systems ⋮ Multiparty half-duplex systems and synchronous communications ⋮ Undecidable problems in unreliable computations. ⋮ On termination and invariance for faulty channel machines ⋮ Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations ⋮ Mixing Lossy and Perfect Fifo Channels ⋮ A Sound Algorithm for Asynchronous Session Subtyping ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Ordinal recursive complexity of unordered data nets ⋮ A classification of the expressive power of well-structured transition systems ⋮ Well-structured transition systems everywhere! ⋮ Quantitative analysis of probabilistic lossy channel systems ⋮ Unnamed Item ⋮ On the termination and structural termination problems for counter machines with incrementing errors ⋮ A Language-Based Comparison of Extensions of Petri Nets with and without Whole-Place Operations ⋮ Towards generalised half-duplex systems ⋮ Verifying identical communicating processes is undecidable ⋮ Complexity Hierarchies beyond Elementary ⋮ Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations ⋮ Verification of probabilistic systems with faulty communication ⋮ Verification of programs with half-duplex communication ⋮ Verifying lossy channel systems has nonprimitive recursive complexity. ⋮ Automated formal analysis and verification: an overview ⋮ Generalized Post embedding problems

This page was built for publication: Unreliable channels are easier to verify than perfect channels