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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1089–1101. Springer, Heidelberg (2005)
Aceto, L., Laroussinie, F.: Is your model checker on time? In: Kutyłowski, M., Wierzbicki, T., Pacholski, L. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 125–136. Springer, Heidelberg (1999)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Madhusudan, P.: Visibly Pushdown Automata. In: ACM Symposium on Theory of Computation, pp. 202–211 (2004)
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202–211. ACM, New York (2004)
Balcázar, J.L., Lozano, A., Torán, J.: The complexity of algorithmic problems on succinct instances. Computer Science, 351–377 (1992)
Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: International Conference on Hybrid Systems: Computation and Control, pp. 64–85 (1994)
Cerans, K.: Decidability of bisimulation equivalence for parallel timer processes. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 302–315. Springer, Heidelberg (1993)
Chadha, R., Legay, A., Prabhakar, P., Viswanathan, M.: Complexity bounds for the verification of real-time software. Technical report, University of Illinois at Urbana-Champaign (2009), http://hdl.handle.net/2142/14134
Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 136–150. Springer, Heidelberg (2007)
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided Abstraction-refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Dang, Z.: Pushdown timed automata: A binary reachability characterization and safety verification. Theoretical Computer Science 302, 93–121 (2003)
Emmi, M., Majumdar, R.: Decision Problems for the Verification of Real-time Software. In: International Conference on Hybrid Systems: Computation and Control, pp. 200–211 (2006)
Galperin, H., Wigderson, A.: Succinct representations of graphs. Information and Computation 56, 183–198 (1983)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Hague, M., Ong, C.-H.L.: Symbolic backwards-reachability analysis for higher-order pushdown systems. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 213–227. Springer, Heidelberg (2007)
Harel, D., Kupferman, O., Vardi, M.Y.: On the complexity of verifying concurrent transition systems. In: International Conference on Concurrency Theory, pp. 258–272 (1997)
Kucera, A.: On simulation-checking with sequential systems. In: He, J., Sato, M. (eds.) ASIAN 2000. LNCS, vol. 1961, pp. 133–148. Springer, Heidelberg (2000)
Laroussinie, F., Schnoebelen, P.: The State Explosion Problem from Trace to Bisimulation Equivalence. In: Tiuryn, J. (ed.) FOSSACS 2000. LNCS, vol. 1784, pp. 192–207. Springer, Heidelberg (2000)
Mayr, R.: On the complexity of bisimulation problems for pushdown automata. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 474–488. Springer, Heidelberg (2000)
Luke Ong, C.-H.: On model checking trees generated by higher order recursion schemes. In: IEEE Symposium on Logic in Computer Science, pp. 81–90 (2006)
Ouaknine, J., Worrell, J.: On the language inclusion problem for timed automata: Closing a decidability gap. In: IEEE Symposium on Logic in Computer Science, pp. 54–63 (2004)
Papadimitriou, C., Yannakakis, M.: A note on succinct representation of graphs. Information and Computation 71, 181–185 (1986)
Rabinovich, A.: Complexity of equivalence problems for concurrent finite agents. Information and Computation 139(2), 111–129 (1997)
Rabinovich, A.: Symbolic model checking for μ-calculus requires exponential time. Theoretical Computer Science 243(2), 467–475 (2000)
Sawa, Z., Jancar, P.: P-Hardness of Equivalence Testing on Finite-State Processes. In: Pacholski, L., Ružička, P. (eds.) SOFSEM 2001. LNCS, vol. 2234, pp. 326–335. Springer, Heidelberg (2001)
Srba, J.: Visibly pushdown automata: From language equivalence to simulation and bisimulation. In: International Workshop on Computer Science Logic, pp. 89–103 (2006)
Veith, H.: Succinct representation, leaf languages, and projection reductions. In: IEEE Conference on Computational Complexity, pp. 118–126 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chadha, R., Legay, A., Prabhakar, P., Viswanathan, M. (2010). Complexity Bounds for the Verification of Real-Time Software. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-11319-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11318-5
Online ISBN: 978-3-642-11319-2
eBook Packages: Computer ScienceComputer Science (R0)