On termination and invariance for faulty channel machines

DOI10.1007/S00165-012-0234-7MaRDI QIDQ1941874zbMATH OpenOpenAlexFDO

Authors Patricia Bouyer, Nicolas Markey, Philippe Schnoebelen, James Worrell, Joël Ouaknine

Publication date 22 March 2013

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-012-0234-7

zbMATH Keywords

computational complexitymetric temporal logicprimitive recursivewell-structured systemschannel machines

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• On termination for faulty channel machines
• On the termination problem for counter machines with incrementing errors
• On the termination and structural termination problems for counter machines with incrementing errors
• Undecidable verification problems for programs with unreliable channels
• Undecidable verification problems for programs with unreliable channels
• On the upper bound for unreliability of non-branching programs under constant faults of the same type on the outputs of computational operators
• Stochastic invariants for probabilistic termination
• Abstractions of Finite-State Machines Optimal with Respect to Single Undetectable Output Faults
• Abstractions of finite-state machines and immediately-detectable output faults
• Fault-tolerance and complexity (extended abstract)

Cites work

• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• Algorithmic analysis of programs with well quasi-ordered domains.
• Foundations of Software Science and Computation Structures
• Foundations of Software Science and Computational Structures
• Mixing Lossy and Perfect Fifo Channels
• Multiply-recursive upper bounds with Higman's lemma
• Nets with tokens which carry data
• On Communicating Finite-State Machines
• On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems
• On termination for faulty channel machines
• Ordering by Divisibility in Abstract Algebras
• Safety alternating automata on data words
• The covering and boundedness problems for vector addition systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Undecidable problems in unreliable computations.
• Undecidable verification problems for programs with unreliable channels
• Unreliable channels are easier to verify than perfect channels
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Well-structured transition systems everywhere!

Cited in

(8)

• Interval temporal logics over strongly discrete linear orders: expressiveness and complexity
• Zeno, Hercules, and the Hydra: safety metric temporal logic is Ackermann-complete
• On termination for faulty channel machines
• On the termination and structural termination problems for counter machines with incrementing errors
• Computable fixpoints in well-structured symbolic model checking
• Handling infinitely branching well-structured transition systems
• On the termination problem for counter machines with incrementing errors
• Complexity hierarchies beyond elementary

This page was built for publication: On termination and invariance for faulty channel machines

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