Verifying lossy channel systems has nonprimitive recursive complexity |
| |
Authors: | Ph Schnoebelen |
| |
Affiliation: | Lab. Spécification et Vérification, ENS de Cachan & CNRS UMR 8643, 61, av. Pdt. Wilson, 94235 Cachan Cedex, France |
| |
Abstract: | Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. It is known that reachability, termination and a few other verification problems are decidable for these systems. In this article we show that these problems cannot be solved in primitive recursive time. |
| |
Keywords: | Verification of infinite-state systems Communication protocols Program correctness Formal methods |
本文献已被 ScienceDirect 等数据库收录! |