Abstract
We introduce a weighted linear temporal logic over infinite words with weights and discounting parameters over ℝ max . We translate the formulas of a syntactically defined fragment of our logic to weighted Büchi automata with discounting. We prove that every ω-recognizable series with discounting is the image of a series definable by a formula of this syntactic fragment through a strict alphabetic epimorphism.
This research has been co-financed by the European Union (European Social Fund - ESF) and Greek national funds through the Operational Program ”Education and Lifelong Learning” of the National Strategic Reference Framework (NSRF) - Research Funding Program: Heracleitus II.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
De Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the Future in Systems Theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)
Dermi, S., Gastin, P.: Specification and verification using temporal logics. In: D’Souza, D., Shankar, P. (eds.) Modern Applications of Automata Theory, IISc, Research monographs, vol. 2. World Scientific (2011)
Droste, M., Kuske, D.: Skew and infinitary formal power series. Theoret. Comput. Sci. 366, 189–227 (2006)
Droste, M., Vogler, H.: Weighted automata and multi-valued logics over arbitrary bounded lattices. Theoret. Comput. Sci. 418, 14–36 (2012)
Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electron. Notes Theor. Comput. Sci. 220, 61–77 (2008)
Kupferman, O., Lustig, Y.: Lattice Automata. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 199–213. Springer, Heidelberg (2007)
Mandrali, E., Rahonis, G.: Weighted first order logic with discounting (in preparation)
Pnueli, A.: The temporal logics of programs. In: 18th IEEE Symposium on Foundations of Computer Science (FOCS), pp. 46–67 (1977)
Vardi, M., Wopler, P.: Reasoning about infinite computations. Inform. and Comput. 115, 1–37 (1994)
Wolper, P.: Constructing Automata from Temporal Logic Formulas: A Tutorial. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) FMPA 2000. LNCS, vol. 2090, pp. 261–277. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mandrali, E. (2012). Weighted LTL with Discounting. In: Moreira, N., Reis, R. (eds) Implementation and Application of Automata. CIAA 2012. Lecture Notes in Computer Science, vol 7381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31606-7_32
Download citation
DOI: https://doi.org/10.1007/978-3-642-31606-7_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31605-0
Online ISBN: 978-3-642-31606-7
eBook Packages: Computer ScienceComputer Science (R0)