Abstract
In this paper we present an algorithm for efficiently computing optimal cost of reaching a goal state in the model of Linearly Priced Timed Automata (LPTA). The central contribution of this paper is a priced extension of so-called zones. This, together with a notion of facets of a zone, allows the entire machinery for symbolic reachability for timed automata in terms of zones to be lifted to cost-optimal reachability using priced zones. We report on experiments with a cost-optimizing extension of Uppaal on a number of examples.
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
D. Applegate and W. Cook. A Computational Study of the Job-Shop Scheduling Problem. OSRA Journal on Computing 3, pages 149–156, 1991.
P. Abdulla, K. Cerans, B. Jonsson, and T. Yih-Kuen. General decidability theorems for infinite-state systems, 1996.
R. Alur and D. Dill. Automata for Modelling Real-Time Systems. In Proc. of Int. Colloquium on Algorithms, Languages and Programming, number 443 in Lecture Notes in Computer Science, pages 322–335, July 1990.
P. Abdulla and B. Jonsson. Undecidability of verifying programs with unreliable channels. In Proc. 21st Int. Coll. Automata, Languages, and Programming (ICALP’94), volume 820 of LNCS, 1994.
R. Alun, S. La Torre, and G. J. Pappas. Optimal paths in weighted timed automata. To appear in HSCC2001.
M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. In Proc. of the 10th Int. Conf. on Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 546–550. Springer-Verlag, 1998.
G. Behrmann, A. Fehnker, T. Hune, K.G. Larsen, P. Pettersson, and J. Romijn. Efficient guiding towards cost-optimality in uppaal. To appear in Proceedings of TACAS’2001.
_G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson, J. Romijn, and F. Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. To appear in Proceedings of HSCC2001, 2001.
J.E. Beasley, M. Krishnamoorthy, and D. Abramson. Scheduling Aircraft Landings-The Static Case. Transportation Science, 34(2):180–197, 2000.
Ed Brinksma and Angelika Mader. Verification and optimization of a plc control schedule. In Proceedings of the 7th SPIN Workshop, volume 1885 of Lecture Notes in Computer Science. Springer Verlag, 2000.
K. Cerans. Deciding properties of integral relational automata. In Proceedings of ICALP 94, volume 820 of LNCS, 1994.
D. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In J. Sifakis, editor, Proc. of Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 197–212. Springer-Verlag, 1989.
Jack J. Dongarra. Performance of Various Computers Using Standard Linear Equations Software. Technical Report CS-89-85, Computer Science Department, University of Tennessee, 2001. An up-to-date version of this report can be found at http://www.netlib.org/benchmark/performance.ps.
A. Fehnker. Scheduling a steel plant with timed automata. In Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA99), pages 280–286. IEEE Computer Society, 1999.
A. Finkel and P. Schnoebelen. Fundamental structures in well-structured infinite transition systems. In Proc. 3rd Latin American Theoretical Informatics Symposium (LATIN’98), volume 1380 of LNCS, 1998.
A. Finkel and Ph. Schnoebelen. Well structured transition systems everywhere. Theoretical Computer Science, 256(1-2):64–92, 2001.
T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: AModel Checker for Hybird Systems. In Orna Grumberg, editor, Proc. of the 9th Int. Conf. on Computer Aided Verification, number 1254 in Lecture Notes in Computer Science, pages 460–463. Springer-Verlag, 1997.
G. Higman. Ordering by divisibility in abstract algebras. Proc. of the London Math. Soc., 2:326–336, 1952.
T. Hune, K.G. Larsen, and P. Pettersson. Guided Synthesis of Control Programs Using Uppaal. In Ten H. Lai, editor, Proc. of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation, pages E15–E22. IEEE Computer Society Press, April 2000.
Fredrik Larsson, Kim G. Larsen, Paul Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 14–24. IEEE Computer Society Press, December 1997.
K.G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134–152, October 1997.
R. Milner. Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989.
P. Niebert and S. Yovine. Computing optimal operation schemes for multi batch operation of chemical plants. VHS deliverable, May 1999. Draft.
T.C. Ruys and E. Brinksma. Experience with Literate Programming in the Modelling and Validation of Systems. In Bernhard Steffen, editor, Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’98), number 1384 in Lecture Notes in Computer Science (LNCS), pages 393–408, Lisbon, Portugal, April 1998. Springer-Verlag, Berlin.
T.G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Larsen, K. et al. (2001). As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_47
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_47
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive