Complexity bounds for the verification of real-time software

Rohit Chadha; Axel Legay; Pavithra Prabhakar; Mahesh Viswanathan

doi:10.1007/978-3-642-11319-2_10

Complexity bounds for the verification of real-time software

Rohit Chadha, Axel Legay, Pavithra Prabhakar, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables.

Original language	English (US)
Title of host publication	Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings
Pages	95-111
Number of pages	17
DOIs	https://doi.org/10.1007/978-3-642-11319-2_10
State	Published - 2010
Externally published	Yes
Event	11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010 - Madrid, Spain Duration: Jan 17 2010 → Jan 19 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5944 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010
Country/Territory	Spain
City	Madrid
Period	1/17/10 → 1/19/10

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-642-11319-2_10

Library availability

Discover UIUC Full Text

Cite this

Chadha, R., Legay, A., Prabhakar, P., & Viswanathan, M. (2010). Complexity bounds for the verification of real-time software. In Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings (pp. 95-111). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5944 LNCS). https://doi.org/10.1007/978-3-642-11319-2_10

Complexity bounds for the verification of real-time software. / Chadha, Rohit; Legay, Axel; Prabhakar, Pavithra et al.
Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. 2010. p. 95-111 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5944 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Chadha, R, Legay, A, Prabhakar, P & Viswanathan, M 2010, Complexity bounds for the verification of real-time software. in Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5944 LNCS, pp. 95-111, 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010, Madrid, Spain, 1/17/10. https://doi.org/10.1007/978-3-642-11319-2_10

Chadha R, Legay A, Prabhakar P, Viswanathan M. Complexity bounds for the verification of real-time software. In Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. 2010. p. 95-111. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-11319-2_10

Chadha, Rohit ; Legay, Axel ; Prabhakar, Pavithra et al. / Complexity bounds for the verification of real-time software. Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings. 2010. pp. 95-111 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{89d92ec4c1d14612ab43e5432a766b23,

title = "Complexity bounds for the verification of real-time software",

abstract = "We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables.",

author = "Rohit Chadha and Axel Legay and Pavithra Prabhakar and Mahesh Viswanathan",

year = "2010",

doi = "10.1007/978-3-642-11319-2_10",

language = "English (US)",

isbn = "3642113184",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "95--111",

booktitle = "Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings",

note = "11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010 ; Conference date: 17-01-2010 Through 19-01-2010",

}

TY - GEN

T1 - Complexity bounds for the verification of real-time software

AU - Chadha, Rohit

AU - Legay, Axel

AU - Prabhakar, Pavithra

AU - Viswanathan, Mahesh

PY - 2010

Y1 - 2010

N2 - We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables.

AB - We present uniform approaches to establish complexity bounds for decision problems such as reachability and simulation, that arise naturally in the verification of timed software systems. We model timed software systems as timed automata augmented with a data store (like a pushdown stack) and show that there is at least an exponential blowup in complexity of verification when compared with untimed systems. Our proof techniques also establish complexity results for boolean programs, which are automata with stores that have additional boolean variables.

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

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

U2 - 10.1007/978-3-642-11319-2_10

DO - 10.1007/978-3-642-11319-2_10

M3 - Conference contribution

AN - SCOPUS:77949442191

SN - 3642113184

SN - 9783642113185

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 95

EP - 111

BT - Verification, Model Checking, and Abstract Interpretation - 11th International Conference, VMCAI 2010, Proceedings

T2 - 11th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2010

Y2 - 17 January 2010 through 19 January 2010

ER -

Complexity bounds for the verification of real-time software

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this