Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Acta Informatica
Erschienen in: Acta Informatica 2/2018

13.10.2016 | Original Article

Parameterized linear temporal logics meet costs: still not costlier than LTL

verfasst von: Martin Zimmermann

Erschienen in: Acta Informatica | Ausgabe 2/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We continue the investigation of parameterized extensions of linear temporal logic (LTL) that retain the attractive algorithmic properties of LTL: a polynomial space model checking algorithm and a doubly-exponential time algorithm for solving games. Alur et al. and Kupferman et al. showed that this is the case for parametric LTL (PLTL) and PROMPT-LTL respectively, which have temporal operators equipped with variables that bound their scope in time. Later, this was also shown to be true for parametric LDL (PLDL), which extends PLTL to be able to express all \(\omega \)-regular properties. Here, we generalize PLTL to systems with costs, i.e., we do not bound the scope of operators in time, but bound the scope in terms of the cost accumulated during time. Again, we show that model checking and solving games for specifications in PLTL with costs is not harder than the corresponding problems for LTL. Finally, we discuss PLDL with costs and extensions to multiple cost functions.
Vorheriger Artikel Average-energy games
Nächster Artikel Reachability analysis of reversal-bounded automata on series–parallel graphs

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
1
Note that the bound in the parity condition with costs may depend on the trace while one typically uses global bounds for \(\text {cPLTL}\) (see, e.g., Sects. 4 and 5). However, for games in finite arenas (and thus also for model checking) these two variants coincide [22].
 
2
Note that our definition is more involved than the one of Kupferman et al., since we require a cycle with non-zero cost instead of any circle.
 
3
Here, we use our assumption on \(\kappa \) indicating the sign of the costs.
 
4
The same disclaimer as for the parity condition with costs applies here. See Footnote 1.
 
Literatur
1.
Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for “model measuring”. ACM Trans. Comput. Log. 2(3), 388–407 (2001)MathSciNetCrossRefMATH
2.
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC 04, pp. 202–211. ACM (2004)
3.
Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009, vol. 5643 of LNCS, pp. 140–156. Springer (2009)
4.
Boom, M.V.: Weak cost monadic logic over infinite trees. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011, vol. 6907 of LNCS, pp. 580–591. Springer (2011)
5.
Bojańczyk, M.: A bounding quantifier. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004, vol. 3210 of LNCS, pp. 41–55. Springer (2004)
6.
7.
Bojanczyk, M.: Weak MSO + U with path quantifiers over infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014 Part II, vol. 8573 of LNCS, pp. 38–49. Springer (2014)
8.
Bojańczyk, M., Colcombet, T.: Bounds in \(\omega \)-regularity. In: LICS 2006, pp. 285–296. IEEE Computer Society (2006)
9.
Bojańczyk, M., Toruńczyk, S.: Weak MSO + U over infinite trees. In: Dürr, C., Wilke, T. (eds.) STACS 2012, vol. 14 of LIPIcs, pp. 648–660. Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2012)
10.
Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007, vol. 4703 of LNCS, pp. 476–491. Springer (2007)
11.
Bozzelli, L., Sánchez, C.: Visibly linear temporal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, vol. 8562 of LNCS, pp. 418–483. Springer (2014)
12.
13.
Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Madhusudan, P., Seshia, Sanjit A. (eds.) CAV 2012, vol. 7358 of LNCS, pp. 23–38. Springer (2012)
14.
C̆erný, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, vol. 6806 of LNCS, pp. 243–259. Springer (2011)
15.
Chatterjee, K., Doyen, L.: Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der H., Friedhelm, S., Paul G. (eds.) ICALP 2010 Part II, vol. 6199 of LNCS, pp. 599–610. Springer (2010)
16.
Chatterjee, K., Henzinger, T.A., Horn, F.: Finitary winning in omega-regular games. ACM Trans. Comput. Log., 11(1) (2009)
17.
Chatterjee, K., Henzinger, T.A., Jurdziński, M.: Mean-payoff parity games. In: LICS 2005, pp. 178–187. IEEE Computer Society (2005)
18.
Colcombet, T.: The theory of stabilisation monoids and regular cost functions. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S.E., Thomas, W. (eds.) ICALP 2009 Part II, vol. 5556 of LNCS, pp. 139–150. Springer (2009)
19.
De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (eds.) IJCAI. IJCAI/AAAI (2013)
20.
Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. In: Peron, A., Piazza, C. (eds.) GandALF 2014, vol. 161 of EPTCS, pp. 60–73 (2014)
21.
Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic (full version). arXiv:​1504.​03880 (2015). Accepted for publication in information and computation
22.
Fijalkow, N., Zimmermann, M.: Parity and Streett games with costs. LMCS, 10(2) (2014)
23.
Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los Angeles, USA (1968)
24.
Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Form. Methods Syst. Des. 34(2), 83–103 (2009)CrossRefMATH
25.
Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C., Liu, Z., Woodcock, J. (eds.) ICTAC 2007, vol. 4711 of LNCS, pp. 291–305. Springer (2007)
26.
Mogavero, F., Murano, A., Sorrentino, L.: On promptness in parity games. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013, vol. 8312 of LNCS, pp. 601–618. Springer (2013)
27.
Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE (1977)
28.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190 (1989)
29.
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Ronchi Della Rocca, S. (eds.) ICALP 1989, vol. 372 of LNCS, pp. 652–671. Springer (1989)
30.
Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007, vol. 4855 of LNCS, pp. 449–460. Springer (2007)
31.
32.
Tentrup, L., Weinert, A., Zimmermann, M.: Approximating optimal bounds in Prompt-LTL realizability in doubly-exponential time (2015). arXiv:​1511.​09450
33.
Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) POPL 88, pp. 250–259. ACM Press (1988)
34.
Vardi, M.Y.: The rise and fall of LTL. In: D’Agostino, G., Torre, S.L. (eds.) GandALF 2011, vol. 54 of EPTCS (2011)
35.
36.
37.
38.
39.
Zimmermann, M.: Parameterized linear temporal logics meet costs: still not costlier than LTL. In: Esparza, J., Tronci, E. (eds.) GandALF 2015, vol. 193 of EPTCS, pp. 144–157 (2015)
Metadaten
Titel
Parameterized linear temporal logics meet costs: still not costlier than LTL
verfasst von
Martin Zimmermann
Publikationsdatum
13.10.2016
Verlag
Springer Berlin Heidelberg
Erschienen in
Acta Informatica / Ausgabe 2/2018
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-016-0279-9