Abstract
While a mature theory around logics such as MSO, LTL, and CTL has been developed in the pure boolean setting of finite automata, weighted automata lack such a natural connection with (temporal) logic and related verification algorithms. In this paper, we will identify weighted versions of MSO and CTL that generalize the classical logics and even other quantitative extensions such as probabilistic CTL. We establish expressiveness results on our logics giving translations from weighted and probabilistic CTL into weighted MSO.
Partially supported by projects ARCUS Île de France-Inde and ANR-06-SETIN-003 DOTS.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004)
Baier, C., Bertrand, N., Größer, M.: On decision problems for probabilistic Büchi automata. In: Amadio, R. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 287–301. Springer, Heidelberg (2008)
Baier, C., Größer, M.: Recognizing ω-regular languages with probabilistic automata. In: Proceedings of LICS 2005, pp. 137–146. IEEE Computer Society Press, Los Alamitos (2005)
Bollig, B., Leucker, M.: Verifying qualitative properties of probabilistic programs. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 124–146. Springer, Heidelberg (2004)
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008)
Buchholz, P., Kemper, P.: Model checking for a class of weighted automata. Discrete Event Dynamic Systems (to appear, 2009)
Büchi, J.R.: Weak second-order arithmetic and finite automata. Z. Math. Logik Grundlagen Math. 6, 66–92 (1960)
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. of the International Congress on Logic, Methodology and Philosophy, pp. 1–11. Standford University Press (1962)
Ciesinski, F., Größer, M.: On probabilistic computation tree logic. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 147–188. Springer, Heidelberg (2004)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)
Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857–907 (1995)
Culik, K., Kari, J.: Image compression using weighted finite automata. Computer and Graphics 17(3), 305–313 (1993)
de Alfaro, L.: Formal verification of probabilistic systems. Technical report, Stanford University, PhD thesis (1998)
Droste, M., Gastin, P.: Weighted automata and weighted logics. Theoretical Computer Science 380(1-2), 69–86 (2007); Special issue of ICALP 2005
Droste, M., Gastin, P.: Weighted automata and weighted logics. In: Kuich, W., Vogler, H., Droste, M. (eds.) Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (to appear, 2009)
Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. In: Holub, J., Žďárek, J. (eds.) CIAA 2007. LNCS, vol. 4783, pp. 73–84. Springer, Heidelberg (2007)
Droste, M., Vogler, H.: Weighted tree automata and weighted logics. Theoretical Computer Science 366(3), 228–247 (2006)
Eisner, J.: Expectation semirings: Flexible EM for learning finite-state transducers. In: Proceedings of the ESSLLI workshop on finite-state methods in NLP (2001)
Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc. 98, 21–52 (1961)
Fischer, D., Grädel, E., Kaiser, L.: Model checking games for the quantitative μ-calculus. Theory of Computing Systems (2009); Special Issue of STACS 2008
Größer, M., Norman, G., Baier, C., Ciesinski, F., Kwiatkowska, M., Parker, D.: On reduction criteria for probabilistic reward models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 309–320. Springer, Heidelberg (2006)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Knopp, K.: Theory and Application of Infinite Series. Dover Publications, New York (1990); Republication of the second English edn. (1951)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Kuich, W., Salomaa, A.: Semirings, Automata and Languages. Springer, Heidelberg (1985)
Kuich, W., Vogler, H., Droste, M. (eds.): Handbook of Weighted Automata. EATCS Monographs in Theoretical Computer Science. Springer, Heidelberg (2009)
Meinecke, I.: A weighted μ-calculus on words. In: Diekert, V., Nowotka, D. (eds.) DLT 2009. LNCS, vol. 5583. Springer, Heidelberg (2009)
Mohri, M.: Finite-state transducers in language and speech processing. Computational Linguistics 23(2), 269–311 (1997)
Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Puterman, M.L.: Markov Decision Processes. John Wiley & Sons, Inc., New York (1994)
Rabin, M.O.: Probabilistic automata. Information and Control 6, 230–245 (1963)
Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006)
Thomas, W.: Languages, automata and logic. In: Salomaa, A., Rozenberg, G. (eds.) Handbook of Formal Languages. Beyond Words, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
van Glabbeek, R.J., Smolka, S.A., Steffen, B.: Reactive, generative and stratified models of probabilistic processes. Information and Computation 121(1), 59–80 (1995)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of FOCS 1985, pp. 327–338. IEEE, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bollig, B., Gastin, P. (2009). Weighted versus Probabilistic Logics. In: Diekert, V., Nowotka, D. (eds) Developments in Language Theory. DLT 2009. Lecture Notes in Computer Science, vol 5583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02737-6_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-02737-6_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02736-9
Online ISBN: 978-3-642-02737-6
eBook Packages: Computer ScienceComputer Science (R0)