Complexity Bounds for the Verification of Real-Time Software

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.

• Type: Conference
• Year: 2010
• Where: VMCAI
• Authors: Rohit Chadha, Axel Legay, Pavithra Prabhakar, Mahesh Viswanathan
• Keywords: Additional Boolean Variables, Software Engineering, Timed Automata, Timed Software Systems, VMCAI 2010