More or Less True DCTL for Continuous-Time MDPs

  • David N. Jansen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)


Discounted Computation Tree Logic is a logic that measures utility (as a real value in the interval [0,1]) instead of discrete truth (only 0 or 1). It is able to express properties that give more weight to the near future than to the far future. This article extends earlier work on DCTL with time, to continuous-time Markov chains and continuous-time Markov decision processes. It presents model checking algorithms for the two possible semantics of DCTL.

A long version of this article containing full proofs is available as [4].


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theoretical Computer Science 345(1), 139–170 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Baier, C., Cloth, L., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performability assessment by model checking of Markov reward models. Formal Methods in System Design 36(1), 1–36 (2010)zbMATHCrossRefGoogle Scholar
  3. 3.
    Baier, C., Hermanns, H., Katoen, J.-P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345(1), 2–26 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Jansen, D.N.: More or less true: DCTL for continuous-time MDPs. Tech. Rep. ICIS–R13006, Radboud Universiteit, Nijmegen (2013),
  5. 5.
    Maplesoft: technical computing software for engineers, mathematicians, scientists, instructors and students,
  6. 6.
    Neuhäußer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 364–379. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  7. 7.
    Wolovick, N., Johr, S.: A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 352–367. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Zadeh, L.A.: Fuzzy sets, fuzzy logic, and fuzzy systems. World Scientific, Singapore (1996)zbMATHGoogle Scholar
  9. 9.
    Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Efficient CSL model checking using stratification. Logical Methods in Computer Science 8(2), paper 17 (2012)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • David N. Jansen
    • 1
  1. 1.Model-Based System DevelopmentRadboud UniversiteitNijmegenThe Netherlands

Personalised recommendations