Statistical guarantees of performance for MIMO designs

Jayanand Asok Kumar, Shobha Vasudevan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.

Original languageEnglish (US)
Title of host publicationProceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
Pages467-476
Number of pages10
DOIs
StatePublished - Sep 20 2010
Event2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010 - Chicago, IL, United States
Duration: Jun 28 2010Jul 1 2010

Publication series

NameProceedings of the International Conference on Dependable Systems and Networks

Other

Other2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010
CountryUnited States
CityChicago, IL
Period6/28/107/1/10

Fingerprint

Model checking
Temporal logic
Explosions
Scalability
Systems analysis
Acoustic waves
Statistical Models

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Computer Networks and Communications

Cite this

Kumar, J. A., & Vasudevan, S. (2010). Statistical guarantees of performance for MIMO designs. In Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010 (pp. 467-476). [5544281] (Proceedings of the International Conference on Dependable Systems and Networks). https://doi.org/10.1109/DSN.2010.5544281

Statistical guarantees of performance for MIMO designs. / Kumar, Jayanand Asok; Vasudevan, Shobha.

Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010. 2010. p. 467-476 5544281 (Proceedings of the International Conference on Dependable Systems and Networks).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kumar, JA & Vasudevan, S 2010, Statistical guarantees of performance for MIMO designs. in Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010., 5544281, Proceedings of the International Conference on Dependable Systems and Networks, pp. 467-476, 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010, Chicago, IL, United States, 6/28/10. https://doi.org/10.1109/DSN.2010.5544281
Kumar JA, Vasudevan S. Statistical guarantees of performance for MIMO designs. In Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010. 2010. p. 467-476. 5544281. (Proceedings of the International Conference on Dependable Systems and Networks). https://doi.org/10.1109/DSN.2010.5544281
Kumar, Jayanand Asok ; Vasudevan, Shobha. / Statistical guarantees of performance for MIMO designs. Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010. 2010. pp. 467-476 (Proceedings of the International Conference on Dependable Systems and Networks).
@inproceedings{c084265356c5484f8250bdddc8b6a213,
title = "Statistical guarantees of performance for MIMO designs",
abstract = "Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.",
author = "Kumar, {Jayanand Asok} and Shobha Vasudevan",
year = "2010",
month = "9",
day = "20",
doi = "10.1109/DSN.2010.5544281",
language = "English (US)",
isbn = "9781424475018",
series = "Proceedings of the International Conference on Dependable Systems and Networks",
pages = "467--476",
booktitle = "Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010",

}

TY - GEN

T1 - Statistical guarantees of performance for MIMO designs

AU - Kumar, Jayanand Asok

AU - Vasudevan, Shobha

PY - 2010/9/20

Y1 - 2010/9/20

N2 - Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.

AB - Sources of noise such as quantization, introduce randomness into Register Transfer Level (RTL) designs of Multiple Input Multiple Output (MIMO) systems. Performance of these MIMO RTL designs is typically quantified by metrics averaged over simulations. In this paper, we introduce a formal approach to compute these metrics with high confidence. We define best, bounded and average case performance metrics as properties in a probabilistic temporal logic. We then use probabilistic model checking to verify these properties for MIMO RTL and thereby guarantee the statistical performance. If a property fails, we show a characterization of error. However, probabilistic model checking is known to encounter the problem of state space explosion. With respect to the properties of interest, we show sound and efficient reductions that significantly improve the scalability of our approach. We illustrate our approach on different non-trivial components of MIMO system designs.

UR - http://www.scopus.com/inward/record.url?scp=77956572729&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=77956572729&partnerID=8YFLogxK

U2 - 10.1109/DSN.2010.5544281

DO - 10.1109/DSN.2010.5544281

M3 - Conference contribution

SN - 9781424475018

T3 - Proceedings of the International Conference on Dependable Systems and Networks

SP - 467

EP - 476

BT - Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2010

ER -