Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 2/2018

13-10-2016 | Original Article

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

Author: Martin Zimmermann

Published in: Acta Informatica | Issue 2/2018

Log in

Activate our intelligent search to find suitable subject content or patents.

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.
previous article Average-energy games
next article Reachability analysis of reversal-bounded automata on series–parallel graphs

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Footnotes
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.
 
Literature
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)
Metadata
Title
Parameterized linear temporal logics meet costs: still not costlier than LTL
Author
Martin Zimmermann
Publication date
13-10-2016
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 2/2018
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-016-0279-9

Premium Partner

    Image Credits