An Efficient Method of Probabilistic Model Checking

Author

Song, Songzheng

Author_Institution

NUS Grad. Sch. for Integrative Sci. & Eng., Nat. Univ. of Singapore, Singapore, Singapore

fYear

2010

fDate

9-11 June 2010

Firstpage

24

Lastpage

25

Abstract

A probabilistic system is useful in modeling randomized algorithms (e.g., consensus algorithms), unreliable or unpredictable behaviors (e.g., human behaviors in decision making process), etc. Markov Decision Process (MDP) is used to construct this kind of system, because it has both nondeterministic and probabilistic choices. In this work, we study probabilistic models and analyze some issues such as reachability and LTL model checking with some new methods in calculating the probability.

Keywords

Markov processes; behavioural sciences; decision making; probability; program verification; randomised algorithms; temporal logic; LTL model checking; Markov decision process; linear temporal logic model checking; probabilistic model checking; randomized algorithm; unpredictable behavior; Automata; Automatic logic units; Decision making; Humans; Probability; Reliability engineering; Safety; Software algorithms; Specification languages; System recovery; LTL; MDP; Model Checking; Probabilistic;

fLanguage

English

Publisher

ieee

Conference_Titel

Secure Software Integration and Reliability Improvement Companion (SSIRI-C), 2010 Fourth International Conference on

Conference_Location

Singapore

Print_ISBN

978-1-4244-7644-2

Type

conf

DOI

10.1109/SSIRI-C.2010.14

Filename

5521552