Verifying lossy channel systems has nonprimitive recursive complexity.

From MaRDI portal
Publication:1853078

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




Related Items

Reachability problems on reliable and lossy queue automataAdding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\)Unnamed ItemFuture-Looking Logics on Data Words and TreesOn Pebble Automata for Data Languages with Decidable Emptiness ProblemOn the verification of membrane systems with dynamic structureMultiparty half-duplex systems and synchronous communicationsOn termination and invariance for faulty channel machinesLeftist Grammars Are Non-primitive RecursiveOn pebble automata for data languages with decidable emptiness problemTree Pattern Rewriting SystemsOn the Reachability Analysis of Acyclic Networks of Pushdown SystemsSome Recent Results in Metric Temporal LogicA Biologically Inspired Model with Fusion and Clonation of MembranesUnnamed ItemQuantitative analysis of probabilistic lossy channel systemsA Kleene theorem and model checking algorithms for existentially bounded communicating automataA general approach to comparing infinite-state systems with their finite-state specificationsNon-primitive recursive decidability of products of modal logics with expanding domainsWeak and Nested Class Memory AutomataSymbolic Verification of Communicating Systems with Probabilistic Message Losses: Liveness and FairnessStochastic Games with Lossy ChannelsThe ω-Regular Post Embedding ProblemPost Embedding Problem Is Not Primitive Recursive, with Applications to Channel SystemsReactive synthesis from interval temporal logic specificationsThe Parametric Complexity of Lossy Counter MachinesComplexity Hierarchies beyond ElementaryModel-checking Timed Temporal LogicsLinear-time temporal logics with Presburger constraints: an overview ★AUTOMATED TERMINATION IN MODEL-CHECKING MODULO THEORIESSome complexity results for stateful network verificationVerification of probabilistic systems with faulty communicationVerification of programs with half-duplex communicationLooking at mean-payoff and total-payoff through windowsRational subsets and submonoids of wreath products.



Cites Work