Complexity bounds for the verification of real-time software
Author(s)
Chadha, Rohit
Legay, Axel
Prabhakar, Pavithra
Viswanathan, Mahesh
Issue Date
2009
Keyword(s)
Complexity
Verification
Real-time software
Succint Representations
Boolean Automata
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.