Verifying lossy channel systems has nonprimitive recursive complexity.

DOI10.1016/S0020-0190(01)00337-4zbMath1043.68016OpenAlexW1987814265MaRDI QIDQ1853078

Yanyan Li

Publication date: 21 January 2003

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0020-0190(01)00337-4

zbMATH Keywords

Formal methodsCommunication protocolsProgram correctnessVerification of infinite-state systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Distributed systems (68M14) Network protocols (68M12)

Related Items

Reachability problems on reliable and lossy queue automata ⋮ Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\) ⋮ Unnamed Item ⋮ Future-Looking Logics on Data Words and Trees ⋮ On Pebble Automata for Data Languages with Decidable Emptiness Problem ⋮ On the verification of membrane systems with dynamic structure ⋮ Multiparty half-duplex systems and synchronous communications ⋮ On termination and invariance for faulty channel machines ⋮ Leftist Grammars Are Non-primitive Recursive ⋮ On pebble automata for data languages with decidable emptiness problem ⋮ Tree Pattern Rewriting Systems ⋮ On the Reachability Analysis of Acyclic Networks of Pushdown Systems ⋮ Some Recent Results in Metric Temporal Logic ⋮ A Biologically Inspired Model with Fusion and Clonation of Membranes ⋮ Unnamed Item ⋮ Quantitative analysis of probabilistic lossy channel systems ⋮ A Kleene theorem and model checking algorithms for existentially bounded communicating automata ⋮ A general approach to comparing infinite-state systems with their finite-state specifications ⋮ Non-primitive recursive decidability of products of modal logics with expanding domains ⋮ Weak and Nested Class Memory Automata ⋮ Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness ⋮ Stochastic Games with Lossy Channels ⋮ The ω-Regular Post Embedding Problem ⋮ Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems ⋮ Reactive synthesis from interval temporal logic specifications ⋮ The Parametric Complexity of Lossy Counter Machines ⋮ Complexity Hierarchies beyond Elementary ⋮ Model-checking Timed Temporal Logics ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIES ⋮ Some complexity results for stateful network verification ⋮ Verification of probabilistic systems with faulty communication ⋮ Verification of programs with half-duplex communication ⋮ Looking at mean-payoff and total-payoff through windows ⋮ Rational subsets and submonoids of wreath products.

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Undecidable verification problems for programs with unreliable channels
• The equality problem for vector addition systems is undecidable
• Algorithmic analysis of programs with well quasi-ordered domains.
• Unreliable channels are easier to verify than perfect channels
• Verifying programs with unreliable channels
• On Communicating Finite-State Machines
• The Complexity of the Finite Containment Problem for Petri Nets
• Ordering by Divisibility in Abstract Algebras
• Nonprimitive recursive complexity and undecidability for Petri net equivalences
• Well-structured transition systems everywhere!