Verifying lossy channel systems has nonprimitive recursive complexity.
From MaRDI portal
Recommendations
Cites work
- Algorithmic analysis of programs with well quasi-ordered domains.
- Boundedness of reset P/T nets
- scientific article; zbMATH DE number 2242597 (Why is no real title available?)
- Nonprimitive recursive complexity and undecidability for Petri net equivalences
- On Communicating Finite-State Machines
- Ordering by Divisibility in Abstract Algebras
- Reasoning about probabilistic lossy channel systems
- Reset nets between decidability and undecidability
- The Complexity of the Finite Containment Problem for Petri Nets
- The equality problem for vector addition systems is undecidable
- Undecidable problems in unreliable computations
- Undecidable verification problems for programs with unreliable channels
- Unreliable channels are easier to verify than perfect channels
- Verifying programs with unreliable channels
- Well-structured transition systems everywhere!
Cited in
(47)- On termination and invariance for faulty channel machines
- On pebble automata for data languages with decidable emptiness problem
- Reactive synthesis from interval temporal logic specifications
- Some complexity results for stateful network verification
- Looking at mean-payoff and total-payoff through windows
- 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
- Verification of probabilistic systems with faulty communication
- Verification of programs with half-duplex communication
- Multiparty half-duplex systems and synchronous communications
- Weak and nested class memory automata
- Complexity hierarchies beyond elementary
- Automated termination in model-checking modulo theories
- Monotonic extensions of Petri nets: forward and backward search revisited
- Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\)
- Future-Looking Logics on Data Words and Trees
- On Pebble Automata for Data Languages with Decidable Emptiness Problem
- Leftist Grammars Are Non-primitive Recursive
- 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
- Symbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and Fairness
- Linear-time temporal logics with Presburger constraints: an overview
- scientific article; zbMATH DE number 1956509 (Why is no real title available?)
- Effective lossy queue languages
- scientific article; zbMATH DE number 1929967 (Why is no real title available?)
- Model-checking timed temporal logics
- The Parametric Complexity of Lossy Counter Machines
- On functions weakly computable by pushdown Petri nets and related systems
- Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties
- Validation of Stochastic Systems
- Stochastic Games with Lossy Channels
- The ω-Regular Post Embedding Problem
- Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems
- On the verification of membrane systems with dynamic structure
- Parameterized broadcast networks with registers: from NP to the frontiers of decidability
- Towards generalised half-duplex systems
- Concurrent stochastic lossy channel games
- 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
- Contextual equivalence for state and control via nested data
- Unreliability in practical subclasses of communicating systems
- Reachability problems on reliable and lossy queue automata
This page was built for publication: Verifying lossy channel systems has nonprimitive recursive complexity.
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853078)
