Multiple-input multiple-output (MIMO) communication systems employ multiple antennas at the transmitter and the receiver. Multiple antennas provide capacity gain and/or robust performance over single antenna communications. Traditional automatic-repeat-request (ARQ) techniques developed for single-input single-output (SISO) communication systems have to be modified in order to be employed in MIMO communication systems. In this dissertation, we propose and analysis some ARQ techniques for MIMO communication systems. The basic retransmission protocols of ARQ, stop-and-wait (SW-ARQ), go-back-$N$ (GBN-ARQ), and selective repeat (SR-ARQ), designed for SISO communication systems are generalized for parallel multichannel communication systems. The generalized ARQ protocols seek to improve the channel utilization of multiple parallel channels with different transmission rates and different packet error rates. The generalized ARQ protocols are shown to improve the transmission delay as well. A type-I hybrid-ARQ error control is used to illustrate the throughput gain of employing ARQ error control into MIMO communication systems. With the channel information known at both the transmitter and the receiver, the MIMO channel is converted into a set of parallel independent subchannels. The performance of the type-I hybrid-ARQ error control is presented. Simulation results show the throughput gain of using an ARQ scheme in MIMO communication systems. When the channel state information is unknown to the transmitter, error control codes that span both space and time, so-called space-time coding, are explored in order to obtained spatial diversity. As a consequence, the coding scheme used for ARQ error control has to be designed in order to consider coding across both space and time. In this dissertation, we design a set of retransmission codes for a type-II hybrid-ARQ scheme employing the multidimensional space-time trellis code as the forward error control code. A concept of sup-optimal partitioning of the (super-)constellation is proposed. The hybrid-ARQ error control scheme, consisting of the optimal code for each transmission, outperforms the hybrid-ARQ error control scheme, consisting of the same code for all transmissions.

Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this work, we consider noisy channels which can corrupt messages. We present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We call these protocols retransmission protocols as they achieve reliable communication through repeated retransmissions of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively. We propose models of these protocols as regular transducers operating on bit strings. Deterministic streaming string transducers provide a natural way of modeling these protocols and formalizing correctness requirements. The verification problem is posed as functional equivalence between the protocol transducer and the specification transducer. Functional equivalence checking is decidable for this class of transducers and this makes the transducer models amenable to algorithmic verification. In our transducer models, message lengths and retransmission rounds are unbounded. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol. We further extend our protocol models to capture the effects of a noisy channel with non-determinism. We present two non-deterministic yet decidable extensions of transducer models of retransmission protocols. For one of our models, we achieve decidable verification by bounding the retransmission rounds, whereas for the other, even retransmission rounds are unbounded.