Abstract
This paper is concerned with the derivation of infinite schedules for timed automata that are in some sense optimal. To cover a wide class of optimality criteria we start out by introducing an extension of the (priced) timed automata model that includes both costs and rewards as separate modelling features. A precise definition is then given of what constitutes optimal infinite behaviours for this class of models. We subsequently show that the derivation of optimal non-terminating schedules for such double-priced timed automata is computable. This is done by a reduction of the problem to the determination of optimal mean-cycles in finite graphs with weighted edges. This reduction is obtained by introducing the so-called corner-point abstraction, a powerful abstraction technique of which we show that it preserves optimal schedules.
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
Applegate, D., Cook, W.: A Computational Study of the Job-Shop Scheduling Problem. OSRA Journal on Computing 3, 149–156 (1991)
Alur, R., Dill, D.: Automata for Modeling Real-Time Systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990)
Alur, R., Dill, D.: A Theory of Timed Automata. Theoretical Computer Science (TCS) 126(2), 183–235 (1994)
Alur, R., La Torre, S., Pappas, G.J.: Optimal Paths inWeighted Timed Automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001)
Asarin, E., Maler, O.: As soon as possible: Time optimal control for timed automata. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 19–30. Springer, Heidelberg (1999)
Abdeddaim, Y., Maler, O.: Job-Shop Scheduling using Timed Automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 478–492. Springer, Heidelberg (2001)
Abdeddaïm, Y., Maler, O.: Preemptive Job-Shop Scheduling using Stopwatch Automata. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 113–126. Springer, Heidelberg (2002)
Bouyer, P., Brinksma, E., Larsen, K.G.: Staying Alive as Cheaply as Possible. Research Report LSV–04–2, LSV, ENS de Cachan, France (2004)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Efficient Guiding Towards Cost-Optimality in Uppaal. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 174–188. Springer, Heidelberg (2001)
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)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., Weise, C.: New Generation of UPPAAL. In: Proc. Int. Work. Software Tools for Technology Transfer (STTT 1998). BRICS Notes Series, pp. 43–52 (1998)
Brinksma, E., Mader, A., Fehnker, A.: Verification and Optimization of a PLC Control Schedule. Journal of Software Tools for Technology Transfer (STTT) 4(1), 21–33 (2002)
Dasdan, A., Gupta, R.K.: Faster Maximum and Minimum Mean Cycle Algorithms for System Performance Analysis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 17(10), 889–899 (1998)
Dasdan, A., Irani, S., Gupta, R.K.: Efficient Algorithms for Optimum Cycle Mean and Optimum Cost to Time Ratio Problems. In: Proc. 36th ACM/IEEE Design Automation Conf (DAC 1999), pp. 42–47. ACM, New York (1999)
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)
D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and Refinement Strategies for Probabilistic Analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol. 2399, pp. 57–76. Springer, Heidelberg (2002)
Fehnker, A.: Scheduling a Steel Plant with Timed Automata. In: Proc. 6th Int. Conf. Real-Time Computing Systems and Applications (RTCSA 1999), pp. 280–286. IEEE Computer Society Press, Los Alamitos (1999)
Hune, T., Larsen, K.G., Pettersson, P.: Guided Synthesis of Control Programs Using UPPAAL. In: Proc. IEEE ICDS Int. Work. Distributed Systems Verification and Validation, pp. 15–22. IEEE Computer Society Press, Los Alamitos (2000)
Karp, R.M.: A Characterization of the Minimum Mean-Cycle in a Digraph. Discrete Mathematics 23(3), 309–311 (1978)
Larsen, K.G., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 493–505. Springer, Heidelberg (2001)
Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a Nutshell. Journal of Software Tools for Technology Transfer (STTT) 1(1-2), 134–152 (1997)
La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-Reachability and Control for Acyclic Weighted Timed Automata. In: Proc. 2nd IFIP Int. Conf. Theoretical Computer Science (TCS 2002). IFIP Conf. Proc., vol. 223, pp. 485–497. Kluwer, Dordrecht (2002)
Mader, A.: Deriving Schedules for a Smart Card Personalisation System (2003) (submitted)
Niebert, P., Yovine, S.: Computing Efficient Operations Schemes for Chemical Plants in Multi-batch Mode. European Journal of Control 7(4), 440–453 (2001)
Zwick, U., Paterson, M.: The Complexity of Mean Payoff Games on Graphs. Theoretical Computer Science (TCS) 158(1-2), 343–359 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouyer, P., Brinksma, E., Larsen, K.G. (2004). Staying Alive as Cheaply as Possible. In: Alur, R., Pappas, G.J. (eds) Hybrid Systems: Computation and Control. HSCC 2004. Lecture Notes in Computer Science, vol 2993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24743-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-24743-2_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21259-1
Online ISBN: 978-3-540-24743-2
eBook Packages: Springer Book Archive