A Complete Approximation Theory for Weighted Transition Systems

  • Mikkel HansenEmail author
  • Kim Guldstrand Larsen
  • Radu Mardare
  • Mathias Ruggaard Pedersen
  • Bingtian Xue
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


We propose a way of reasoning about minimal and maximal values of the weights of transitions in a weighted transition system (WTS). This perspective induces a notion of bisimulation that is coarser than the classic bisimulation: it relates states that exhibit transitions to bisimulation classes with the weights within the same boundaries. We propose a customized modal logic that expresses these numeric boundaries for transition weights by means of particular modalities. We prove that our logic is invariant under the proposed notion of bisimulation. We show that the logic enjoys the finite model property which allows us to prove the decidability of satisfiability and provide an algorithm for satisfiability checking. Last but not least, we identify a complete axiomatization for this logic, thus solving a long-standing open problem in this field. All our results are proven for a class of WTSs without the image-finiteness restriction, a fact that makes this development general and robust.


Modal Logic Axiomatic System Finite Model Complete Axiomatization Arbitrary Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



The authors would like to thank the anonymous reviewers for their useful comments and suggestions. This research was supported by the Danish FTP project ASAP: “Approximate Stochastic Analysis of Processes”, the ERC Advanced Grant LASSO: “Learning, Analysis, Synthesis and Optimization of Cyber Physical Systems” as well as the Sino-Danish Basic Research Center IDEA4CPS.


  1. 1.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104(1), 2–34 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning. Elsevier Science, Amsterdam (2006)zbMATHGoogle Scholar
  3. 3.
    Breugel, F.: Generalizing finiteness conditions of labelled transition systems. In: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 376–387. Springer, Heidelberg (1994). doi: 10.1007/3-540-58201-0_83 CrossRefGoogle Scholar
  4. 4.
    Chakraborty, S., Katoen, J.P.: On the satisfiability of some simple probabilistic logics. In: LICS (2016 to appear)Google Scholar
  5. 5.
    Fagin, R., Halpern, J.Y.: Reasoning about knowledge and probability. J. ACM 41, 340 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Heifetz, A., Mongin, P.: Probability logic for type spaces. Games Econ. Behav. 35, 31 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Jaziri, S., Larsen, K.G., Mardare, R., Xue, B.: Adequacy and complete axiomatization for timed modal logic. Electr. Notes Theor. Comput. Sci. 308, 183–210 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS 1991) (1991)Google Scholar
  10. 10.
    Juhl, L., Larsen, K.G., Srba, J.: Modal transition systems with weight intervals. J. Log. Algebr. Program. 81, 408 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Kozen, D., Larsen, K.G., Mardare, R., Panangaden, P.: Stone duality for Markov processes. In: 2013 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS), pp. 321–330, June 2013Google Scholar
  12. 12.
    Kozen, D., Mardare, R., Panangaden, P.: Strong completeness for Markovian logics. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 655–666. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-40313-2_58 CrossRefGoogle Scholar
  13. 13.
    Larsen, K.G., Mardare, R.: Complete proof systems for weighted modal logic. Theor. Comput. Sci. 546, 164 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Larsen, K.G., Mardare, R., Xue, B.: On decidability of recursive weighted logics. Soft Comput. 20, 1–18 (2016)CrossRefGoogle Scholar
  15. 15.
    Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: approximate reasoning for Markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681–692. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32589-2_59 CrossRefGoogle Scholar
  16. 16.
    Mardare, R., Cardelli, L., Larsen, K.G.: Continuous Markovian logics-axiomatization and quantified metatheory. Log. Meth. Comput. Sci. 8(4) (2012)Google Scholar
  17. 17.
    Zhou, C.: A complete deductive system for probability logic. J. Log. Comput. 19, 1427 (2009)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Mikkel Hansen
    • 1
    Email author
  • Kim Guldstrand Larsen
    • 1
  • Radu Mardare
    • 1
  • Mathias Ruggaard Pedersen
    • 1
  • Bingtian Xue
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityAalborgDenmark

Personalised recommendations