\input zb-basic
\input zb-ioport
\iteman{io-port 06069570}
\itemau{Delzanno, Giorgio; Sangnier, Arnaud; Zavattaro, Gianluigi}
\itemti{Verification of ad hoc networks with node and communication failures.}
\itemso{Giese, Holger (ed.) et al., Formal techniques for distributed systems. Joint 14th IFIP WG 6.1 international conference, FMOODS 2012 and 32nd IFIP WG 6.1 international conference, FORTE 2012, Stockholm, Sweden, June 13--16, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-30792-8/pbk). Lecture Notes in Computer Science 7273, 235-250 (2012).}
\itemab
Summary: We investigate the impact of node and communication failures on the decidability and complexity of parametric verification of a formal model of ad hoc networks. We start by considering three possible types of node failures: intermittence, restart, and crash. Then we move to three cases of communication failures: nondeterministic message loss, message loss due to conflicting emissions, and detectable conflicts. Interestingly, we prove that the considered decision problem (reachability of a control state) is decidable for node intermittence and message loss (either nondeterministic or due to conflicts) while it turns out to be undecidable for node restart/crash, and conflict detection.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-30793-5\_15}
\end