Abstract
We study the model-checking problem for WMTL, a cost-extension of the linear-time timed temporal logic MTL, that is interpreted over weighted timed automata. We draw a complete picture of the decidability for that problem: it is decidable only for the class of one-clock weighted timed automata with a restricted stopwatch cost, and any slight extension of this model leads to undecidability. We finally give some consequences on the undecidability of linear hybrid automata.
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
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. Journal of the ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. In: Proc. 5th Annual Symposium on Logic in Computer Science (LICS 1990), pp. 390–401. IEEE Computer Society Press, Los Alamitos (1990)
Alur, R., Torre, S.L., 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)
Abdulla, P.A., Nylén, A.: Better is better than well: On efficient verification of infinite-state systems. In: Proc. 15th Annual Symposium on Logic in Computer Science (LICS 2000), pp. 132–140. IEEE Computer Society press, Los Alamitos (2000)
Bouyer, P., Brihaye, T., Bruyère, V., Raskin, J.-F.: On the optimal reachability problem. Formal Methods in System Design (to appear, 2007)
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., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. Information Processing Letters 98(5), 188–194 (2006)
Brihaye, T., Bruyère, V., Raskin, J.-F.: Model-checking for weighted timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 277–292. Springer, Heidelberg (2004)
Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 49–64. Springer, Heidelberg (2005)
Brihaye, T., Bruyère, V., Raskin, J.-F.: On model-checking timed automata with stopwatch observers. Information and Computation 204(3), 447–478 (2006)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)
Bouyer, P., Larsen, K.G., Markey, N.: Model-checking one-clock priced timed automata. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 108–122. Springer, Heidelberg (2007)
Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one-clock priced timed automata. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 345–356. Springer, Heidelberg (2006)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proc. 21st Annual Symposium on Logic in Computer Science (LICS’07). IEEE Computer Society Press (to appear, 2007)
Fleury, E.: Automates temporisés avec mises à jour. PhD thesis, École Normale Supérieure de Cachan, Cachan, France (2002)
Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? Journal of Computer and System Sciences 57(1), 94–124 (1998)
Koymans, R.: Specifying real-time properties with Metric Temporal Logic. Real-Time Systems 2(4), 255–299 (1990)
Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 387–401. Springer, Heidelberg (2004)
Larsen, K.G., Rasmussen, J.I.: Optimal conditional scheduling for multi-priced timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 234–249. Springer, Heidelberg (2005)
Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 250–265. Springer, Heidelberg (2005)
Lasota, S., Walukiewicz, I.: Alternating timed automata. ACM Transactions on Computational Logic (to appear, 2007)
Ouaknine, J., Worrell, J.: On the decidability of Metric Temporal Logic. In: Proc. 19th Annual Symposium on Logic in Computer Science (LICS 2005), pp. 188–197. IEEE Computer Society Press, Los Alamitos (2005)
Ouaknine, J., Worrell, J.: On Metric Temporal Logic and faulty Turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)
Ouaknine, J., Worrell, J.: On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Computer Science 3(1:8), 1–27 (2007)
Raskin, J.-F.: Logics, Automata and Classical Theories for Deciding Real-Time. PhD thesis, University of Namur, Namur, Belgium (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouyer, P., Markey, N. (2007). Costs Are Expensive!. In: Raskin, JF., Thiagarajan, P.S. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2007. Lecture Notes in Computer Science, vol 4763. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75454-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-75454-1_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75453-4
Online ISBN: 978-3-540-75454-1
eBook Packages: Computer ScienceComputer Science (R0)