Abstract
We consider the model of priced timed automata, an extension of timed automata and study the model checking problem of logic WCTL with multi constrained modalities. For simple modalities, it is known that this is decidable [10] for one clock priced timed automata, and is not [14] when the number of clocks is more than one. For the model of priced timed automata with 2 stopwatch costs having no discrete costs, we give an algorithm for model checking the existential fragment of WCTL with multi constrained modalities. The algorithm runs in time that is doubly exponential in the size of the input(automaton, formula).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Chiplunkar, A., Krishna, S., Jain, C.: Model Checking logic WCTL with multiconstrained modalities on One Clock Priced Timed Automata, TR-09-30, Technical Report, IIT Bombay (2009), http://www.cse.iitb.ac.in/~krishnas/TR-09-30.pdf
Strzebonski, A.: Solving Systems of Strict Polynomial Inequalities. Journal of Symbolic Computation 29, 471–480 (2000)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theoretical Computer Science 126(2), 183–235 (1994)
Abdeddaim, Y., Asarin, E., Mailer, O.: Scheduling with timed automata. Theoretical Computer Science 354(2), 272–300 (2006)
Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: DÃaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122–133. Springer, Heidelberg (2004)
Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, p. 147. Springer, Heidelberg (2001)
Bouyer, P., Brinksma, E., Larsen, K.G.: Staying alive as cheaply as possible. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 203–218. Springer, Heidelberg (2004)
Bouyer, P., Brinksma, E., Larsen, K.G.: Optimal infinite scheduling for multi priced timed automata. Formal Methods in System Design 31(2), 135–175 (2007)
Bouyer, P., Larsen, K.G.: Nicolas Markey. Model-Checking One Clock Priced Timed Automata. Logical Methods in Computer Science 4(2:9), 1–28 (2008)
Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49–64. Springer, Heidelberg (2005)
Brihaye, T., Bruyère, V., Raskin, J.-F.: On model-checking timed automata with stopwatch observers. Info. and Computation 204(3), 408–433 (2006)
Larsen, K.G., Rasmussen, J.I.: Optimal conditional reachability for multi-priced timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 234–249. Springer, Heidelberg (2005)
Manasa, L., Krishna, S.N., Jain, C.: Model-Checking Weighted Integer Reset Timed Automata, http://www.cse.iitb.ac.in/~krishnas/jlc.pdf
Rasmussen, J.I., Larsen, K.G., Subramani, K.: Resource-optimal scheduling using priced timed automata. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 220–235. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chiplunkar, A., Krishna, S.N., Jain, C. (2009). Model Checking Logic WCTL with Multi Constrained Modalities on One Clock Priced Timed Automata. In: Ouaknine, J., Vaandrager, F.W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2009. Lecture Notes in Computer Science, vol 5813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04368-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-04368-0_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04367-3
Online ISBN: 978-3-642-04368-0
eBook Packages: Computer ScienceComputer Science (R0)