• DocumentCode
    2334092
  • Title

    Counterexample for Timed Probabilistic Reachability in Uniform CTMDP

  • Author

    Zhang, Junhua ; Huang, Zhiqiu ; Cao, Zining ; Xiao, Fangxiong

  • Author_Institution
    Coll. of Inf. Sci. & Technol., Najing Univ. of Aeronaut. & Astronaut., Nanjing
  • fYear
    2008
  • fDate
    20-20 Nov. 2008
  • Firstpage
    612
  • Lastpage
    615
  • Abstract
    A uniform continuous-time Markov decision process (CTMDP) is a CTMDP where the exit rate from every state is the same for all states. This paper solves the problem of generating counterexamples for timed probabilistic reachability in uniform CTMDP. The key contribution is an efficient algorithm for computing a minimal part of a uniform CTMDP that indicates the violation of time-bounded reachability probabilities.
  • Keywords
    Markov processes; continuous time systems; probability; reachability analysis; time-bounded reachability probability; timed probabilistic reachability; uniform CTMDP; uniform continuous-time Markov decision process; Educational institutions; Engineering management; Information management; Information science; Information technology; Processor scheduling; Seminars; Space technology; Technology management;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Future Information Technology and Management Engineering, 2008. FITME '08. International Seminar on
  • Conference_Location
    Leicestershire, United Kingdom
  • Print_ISBN
    978-0-7695-3480-0
  • Type

    conf

  • DOI
    10.1109/FITME.2008.26
  • Filename
    4746569