Complexity Bounds for the Verification of Real-Time Software

被引：0
作者：
Chadha, Rohit [1 ]
Legay, Axel [2 ]
Prabhakar, Pavithra [3 ]
Viswanathan, Mahesh [3 ]
机构：
[1] ENS Cachan, LSV, CNRS, INRIA, Cachan, France
[2] Univ Illinois, Dept Comp Sci, Champaign, IL 61820 USA
[3] IRISA, F-35042 Rennes, France
来源：
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS | 2010年 / 5944卷
基金：
美国国家科学基金会;
关键词：
SUCCINCT REPRESENTATIONS; MODEL-CHECKING; DECIDABILITY; AUTOMATA; SYSTEMS;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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.
引用
收藏
页码：95 / +
页数：3
相关论文
共 27 条
[1]  
Abdulla PA, 2005, LECT NOTES COMPUT SC, V3580, P1089
[2]  
ACETO L, 1999, LNCS, V1672, P125, DOI DOI 10.1007/3-540-48340-3
[3]  
Alur R., 2004, P 36 ANN ACM S THEOR, P202, DOI [DOI 10.1145/1007352.1007390, 10.1145/1007352.1007390]
[4]  
ALUR R, 1994, THEORETICAL COMPUTER, V126, P235
[5]  
BALCAZAR JL, 1992, COMPUTER SCIENCE, P351
[6]  
BOUAJJANI A, 1994, INT C HYBR SYST COMP, P64
[7]  
CERANS K, 1993, LNCS, V697, P302
[8]  
Chadha R, 2007, LECT NOTES COMPUT SC, V4703, P136
[9]  
CHADHA R, 2009, COMPLEXITY BOUNDS VE
[10]  
Clarke E. M., 2000, P 12 INT C COMP AID, V1855, P154
123