Decidability and Expressiveness of Recursive Weighted Logic

  • Kim Guldstrand Larsen
  • Radu Mardare
  • Bingtian Xue
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8974)


Labelled weighted transition systems (LWSs) are transition systems labelled with actions and real numbers. The numbers represent the costs of the corresponding actions in terms of resources. Recursive Weighted Logic (RWL) is a multimodal logic that expresses qualitative and quantitative properties of LWSs. It is endowed with simultaneous recursive equations, which specify the weakest properties satisfied by the recursive variables. We demonstrate that RWL is sufficiently expressive to characterize weighted-bisimilarity of LWSs. In addition, we prove that the logic is decidable, i.e., the satisfiability problem for RWL can be algorithmically solved.


Labelled weighted transition system Maximal fixed point Hennessy-Milner property Satisfiability 


  1. [ACD93]
    Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  2. [AD90]
    Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 322–335. Springer, Heidelberg (1990) CrossRefGoogle Scholar
  3. [AILS07]
    Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007) CrossRefGoogle Scholar
  4. [ATP01]
    Alur, R., La Torre, S., Pappas, G.J.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 49–62. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  5. [BFH+01]
    Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J.M.T., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001) CrossRefGoogle Scholar
  6. [CKS92]
    Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: von Bochmann, G., Probst, D.K. (eds.) CAV 1992. LNCS, vol. 663, pp. 410–422. Springer, Heidelberg (1993) CrossRefGoogle Scholar
  7. [CS93]
    Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Form. Meth. Syst. Design 2(2), 121–147 (1993)CrossRefzbMATHGoogle Scholar
  8. [DKV09]
    Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009) zbMATHGoogle Scholar
  9. [HKT01]
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. The MIT Press, Cambridge (2001)CrossRefGoogle Scholar
  10. [HM80]
    Hennessy, M., Milner, R.: On observing nondeterminism and concurrency. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol. 85, pp. 299–309. Springer, Heidelberg (1980) CrossRefGoogle Scholar
  11. [HNSY92]
    Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. In: LICS, pp. 394–406 (1992)Google Scholar
  12. [Koz82]
    Kozen, D.: Results on the propositional \(\mu \)-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. Lecture Notes in Computer Science, vol. 140, pp. 348–359. Springer, Heidelberg (1982) Google Scholar
  13. [Lar90]
    Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265–288 (1990)CrossRefzbMATHGoogle Scholar
  14. [LLW95]
    Laroussinie, F., Larsen, K.G., Weise, C.: From timed automata to logic - and back. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 529–539. Springer, Heidelberg (1995) CrossRefGoogle Scholar
  15. [LM13]
    Larsen, K.G., Mardare, R.: Complete proof system for weighted modal logic. Theor. Comput. Sci. 546, 164–175 (2013)CrossRefMathSciNetGoogle Scholar
  16. [SR11]
    Sangiorgi, D., Rutten, J. (eds.): Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, Cambridge (2011) Google Scholar
  17. [Sti99]
    Stirling, C.: Bisimulation, modal logic and model checking games. Log. J. IGPL 7(1), 103–124 (1999)CrossRefzbMATHMathSciNetGoogle Scholar
  18. [Tar55]
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5(2), 285–309 (1955)CrossRefzbMATHMathSciNetGoogle Scholar
  19. [Wal00]
    Walukiewicz, I.: Completeness of kozen’s axiomatisation of the propositional \(\mu \)-calculus. Inf. Comput. 157(1–2), 142–182 (2000)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Kim Guldstrand Larsen
    • 1
  • Radu Mardare
    • 1
  • Bingtian Xue
    • 1
  1. 1.Aalborg UniversityAalborgDenmark

Personalised recommendations