SMT-based Searching for κ-quasi-optimal Runs in Weighted Timed Automata

• Autorzy: Woźna-Szcześniak B. , Zbrzezny A. M. , Zbrzezny A.

Identyfikatory

DOI

10.3233/FI-2017-1527

• Języki publikacji: EN

Abstrakty

EN

We investigate a quasi-optimal cost reachability problem for weighted timed automata. We use a translation to the satisfiability modulo theories (SMT) problem to solve the problem. In particular, we show how to find a run of length κ ∊ N that starts at the initial state and terminates at a state containing the target location, its total cost belongs to the interval [c; c + 1), for some natural number c ∊ IN, and the cost of each other run of length κ, which also leads from the initial state to a state containing the target location, is greater or equal to c. This kind of run is called κ-quasi-optimal. We exemplify the use of our solution to the investigated problem by means of the weighted timed generic pipeline protocol and the weighted job shop scheduling problem, and we provide some preliminary experimental results.

Słowa kluczowe

EN

satisfiability; quasi-markets; job shop; workshop; flow shop

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 152, nr 4
• Strony: 411--433
• Opis fizyczny: Bibliogr. 27 poz., tab., wykr.

Twórcy

autor

Woźna-Szcześniak B.

• IMCS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A. M.

• IMCS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

autor

Zbrzezny A.

• IMCS, Jan Długosz University in Częstochowa, Al. Armii Krajowej 13/15, 42-200 Częstochowa, Poland

Bibliografia

• [1] Abdeddaïm Y, Asarin E, and Maler O. Scheduling with timed automata. Theoretical Computer Science, 2006;354(2):272–300. doi:10.1016/j.tcs.2005.11.018.
• [2] Abdeddaïm Y, and Maler O. Job-shop scheduling using timed automata. In Proceedings of the 13th International Conference on Computer Aided Verification (CAV’01), volume 2102 of LNCS, pp. 478–492. Springer-Verlag, 2001.
• [3] Alur R, Courcoubetis C, and Henzinger T. Computing accumulated delays in real-time systems. Formal Methods in System Design, 1997;11(2):137–155.
• [4] Alur R, La Torre S, and Pappas GJ. Optimal paths in weighted timed automata. Theoretical Computer Science, 2004;318(3):297–322. URL http://dx.doi.org/10.1016/j.tcs.2003.10.038.
• [5] Asarin E, and Maler O. As soon as possible: Time optimal control for timed automata. In Proceedings of the 2nd International Workshop on Hybrid Systems: Computation and Control, volume 1569 of LNCS, pp. 19–30. Springer-Verlag, 1999. doi:10.1007/3-540-48983-5_6.
• [6] Clark Barrett, Roberto Sebastiani, Sanjit Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 26, pages 825–885. IOS Press, 2009. doi:10.3233/978-1-58603-929-5-825.
• [7] Behrmann G, Fehnker A, Hune T, Larsen K, Pettersson P, Romijn J, and Vaandrager F. Minimum-cost reachability for priced timed automata. In Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC’2001), volume 2034 of LNCS, pp. 147–161. Springer-Verlag, 2001. doi:10.1007/3-540-45351-2_15.
• [8] Behrmann G, Larsen KG, and Rasmussen JI. Priced timed automata: Algorithms and applications. In Formal Methods for Components and Objects, Third International Symposium, FMCO 2004, volume 3657 of LNCS, pp. 162–182. Springer, 2005. doi:10.1007/11561163_8.
• [9] Bouyer P, Brihaye T, Bruyère V, and Raskin J. On the optimal reachability problem of weighted timed automata. Formal Methods in System Design, 2007;31(2):135–175. doi:10.1007/s10703-007-0035-4.
• [10] Bouyer P, Brinksma E, and Larsen KG. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design, 2008;32(1):3–23. doi:10.1007/s10703-007-0043-4.
• [11] Clarke EM, Grumberg O, and Peled DA. Model Checking. The MIT Press, 1999. ISBN:0-262-03270-8.
• [12] Courcoubetis C and Yannakakis M. Minimum and maximum delay problems in real-time systems. Formal Methods in System Design, 1992;1(4):385–415. doi:10.1007/BF00709157.
• [13] D’Argenio PR, Jeannet B, Jensen HE, and Larsen KG. Reachability analysis of probabilistic systems by successive refinements. In Proceedings of the Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification, volume 2165 of LNCS, pp. 39–56. Springer-Verlag, 2001. ISBN:3-540-42556-X.
• [14] Fehnker A. Bounding and heuristics in forward reachability algorithms. Technical Report CSI-R0002, Computing Science Institute Nijmegen, 2000. URL http://hdl.handle.net/2066/18840.
• [15] Kesten Y, Pnueli A, Sifakis J, and Yovine S. Decidable integration graphs. Information and Computation, 1999;150(2):209–243. URL http://dx.doi.org/10.1006/inco.1998.2774.
• [16] Koymans R. Specifying Message Passing and Time-Critical Systems with Temporal Logic, volume 651 of LNCS, chapter Time-critical systems, pp. 99–142. Springer Berlin Heidelberg, 1992. ISBN-13:978-3540562832, 10:3540562834.
• [17] Larsen KG, and Rasmussen JI. Optimal reachability for multi-priced timed automata. Theoretical Computer Science, 2008;390(2-3):197–213. URL http://dx.doi.org/10.1016/j.tcs.2007.09.021.
• [18] Malinowski J, and Niebert P. Sat based bounded model checking with partial order semantics for timed automata. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), volume 6015 of LNCS, pp. 405–419. Springer-Verlag, 2010. doi:10.1007/978-3-642-12002-2_34.
• [19] De Moura L, and Bjørner N. Z3: an efficient SMT solver. In Proceedings of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2008), volume 4963 of LNCS, pp. 337–340. Springer-Verlag, 2008. URL http://dl.acm.org/citation.cfm?id=1792734.1792766.
• [20] Niebert P, Mahfoudh M, Asarin E, Bozga M, Maler O, and Jain N. Verification of Timed Automata via satisfiability checking. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT’02), volume 2469 of LNCS, pp. 226–243. Springer-Verlag, 2002. doi:10.1007/3-540-45739-9_15.
• [21] Niebert P, Tripakis S, and Yovine S. Minimum-time reachability for Timed Automata. In Proceedings of the 8th IEEE Mediterranean Conference on Control and Automation (MED’2000), Patros, Greece, July 2000. IEEE Computer Society.
• [22] Peled D. All from one, one for all: On model checking using representatives. In Proceedings of the 5th International Conference on Computer Aided Verification (CAV’93), volume 697 of LNCS, pp. 409–423. Springer-Verlag, 1993. ISBN:1-55860-299-2.
• [23] Roscoe AW. Understanding Concurrent Systems. Springer-Verlag, 2010.
• [24] E. Taillard. Benchmarks for basic scheduling problems. European Journal of Operational Research, 1993;64(2):278–285. URL http://dx.doi.org/10.1016/0377-2217(93)90182-M.
• [25] Woźna B, Zbrzezny A, and Penczek W. Checking reachability properties for Timed Automata via SAT. Fundamenta Informaticae, 2003;55(2):223–241. URL http://dl.acm.org/citation.cfm?id=2370935.2370944.
• [26] Woźna-Szcześniak B, and Zbrzezny A. SAT-based searching for k-quasi-optimal runs in weighted timed automata. Scientific Issues of Jan Długosz University in Częstochowa: Mathematica, XV:149–162, 2010.
• [27] Zbrzezny A. On boolean encodings of transition relation for parallel compositions of transition systems. In Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013), volume 1032 of CEUR Workshop Proceedings, pp. 478–489, 2013. URL http://ceur-ws.org/Vol-1032/paper-42.pdf.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).