zbMATH — the first resource for mathematics

Model checking and synthesis for branching multi-weighted logics. (English) Zbl 1423.68284
Summary: We investigate the open synthesis problem in a quantitative game theoretic setting where the system model is annotated with multiple nonnegative weights representing quantitative resources such as energy, discrete time or cost. We consider system specifications expressed in the branching time logic CTL extended with bounds on resources. As our first contribution, we show that the model checking problem for the full logic is undecidable with already three weights. By restricting the bounds to constant upper or lower-bounds on the individual weights, we demonstrate that the problem becomes decidable and that the model checking problem is PSPACE-complete. As a second contribution, we show that by imposing upper-bounds on the temporal operators and assuming that the cost converges over infinite runs, the synthesis problem is also decidable. Finally, we provide an on-the-fly algorithm for the synthesis problem on an unrestricted model for a reachability fragment of the logic and we prove EXPTIME-completeness of the synthesis problem.
68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI
[1] Almagor, Shaull; Boker, Udi; Kupferman, Orna, Formally reasoning about quality, J. ACM, 63, 3, 1-56, (jun 2016)
[2] Boker, Udi; Chatterjee, Krishnendu; Henzinger, Thomas A.; Kupferman, Orna, Temporal specifications with accumulative values, ACM Trans. Comput. Log., 15, 4, Article 27, (2014) · Zbl 1354.68169
[3] Bouyer, Patricia; Fahrenberg, Ulrich; Guldstrand Larsen, Kim; Markey, Nicolas; Srba, Jirí, Infinite runs in weighted timed automata with energy constraints, (FORMATS, (2008)), 33-47 · Zbl 1171.68524
[4] Chatterjee, Krishnendu; Randour, Mickael; Raskin, Jean-François, Strategy synthesis for multi-dimensional quantitative objectives, (Acta Informatica, (2014)), 129-163 · Zbl 1360.68208
[5] Clarke, Edmund M.; Allen Emerson, E., Design and synthesis of synchronization skeletons using branching time temporal logic, (Logics of Programs. Logics of Programs, LNCS, vol. 131, (1982), Springer), 52-71 · Zbl 0546.68014
[6] Dalsgaard, A. E.; Enevoldsen, S.; Fogh, P.; Jensen, L. S.; Jepsen, T. S.; Kaufmann, I.; Larsen, K. G.; Nielsen, S. M.; Olesen, M. C.; Pastva, S.; Srba, J., Extended dependency graphs and efficient distributed fixed-point computation, LNCS, 10258, (2017) · Zbl 1393.68098
[7] Fahrenberg, Uli; Juhl, Line; Larsen, Kim G.; Srba, Jirí, Energy games in multiweighted automata, (ICTAC, (2011)), 95-115 · Zbl 1350.68168
[8] Harel, D.; Pnueli, A., On the development of reactive systems, (Logics and Models of Concurrent Systems, (1985), Springer), 477-498 · Zbl 0581.68046
[9] Jensen, J. F.; Larsen, K. G.; Srba, J.; Oestergaard, L. K., Efficient model checking of weighted CTL with upper-bound constraints, Int. J. Softw. Tools Technol. Transf., 18, 4, 409-426, (2016)
[10] Juhl, Line; Larsen, Kim Guldstrand; Raskin, Jean-François, Optimal bounds for multiweighted and parametrised energy games, (Theories of Programming and Formal Methods, (2013)), 244-255 · Zbl 1390.68399
[11] Jurdziński, Marcin; Laroussinie, François; Sproston, Jeremy, Model Checking Probabilistic Timed Automata with One or Two Clocks, LNCS, vol. 4424, 170-184, (2007), Springer · Zbl 1186.68295
[12] Jurdziński, Marcin; Lazić, Ranko; Schmitz, Sylvain, Fixed-dimensional energy games are in pseudo-polynomial time, (ICALP 2015. ICALP 2015, LNCS, vol. 9135, (2015), Springer), 260-272 · Zbl 1440.68122
[13] Laroussinie, F.; Schnoebelen, Ph; Turuani, M., On the Expressivity and Complexity of Quantitative Branching-Time Temporal Logics, (2003), Technical report · Zbl 1019.03012
[14] Larsen, Kim G.; Mardare, Radu; Xue, Bingtian, Alternation-free weighted mu-calculus: decidability and completeness, Electron. Notes Theor. Comput. Sci., 319, 289-313, (2015) · Zbl 1351.68164
[15] Liu, Xinxin; Smolka, Scott A., Simple linear-time algorithms for minimal fixed points, (ICALP 1998. ICALP 1998, LNCS, vol. 1443, (1998), Springer), 53-66
[16] Manna, Zohar; Waldinger, Richard, A deductive approach to program synthesis, ACM Trans. Program. Lang. Syst., 2, 1, 90-121, (1980) · Zbl 0468.68009
[17] Minsky, Marvin L., Computation: Finite and Infinite Machines, (1967), Prentice-Hall, Inc. · Zbl 0195.02402
[18] Pnueli, A.; Rosner, R., On the synthesis of a reactive module, (Proceedings of the 16th ACM Symposium on Principles of Programming Languages. Proceedings of the 16th ACM Symposium on Principles of Programming Languages, POPL 1989, (1989), ACM), 179-190
[19] Queille, J. P.; Sifakis, J., Specification and verification of concurrent systems in CESAR, (International Symposium on Programming, (1982), Springer), 337-351 · Zbl 0482.68028
[20] Savitch, Walter J., Relationships between nondeterministic and deterministic tape complexities, J. Comput. Syst. Sci., 4, 2, 177-192, (1970) · Zbl 0188.33502
[21] Sipser, Michael, Introduction to the Theory of Computation. Course Technology, (2006) · Zbl 1191.68311
[22] Wolfgang, Thomas, On the synthesis of strategies in infinite games, (STACS, (1995), Springer Berlin Heidelberg), 1-13 · Zbl 1379.68233
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.