Title :
Reduction Criteria for Probabilistic Models with Spatial Restrictions on States
Author :
Jun, Niu ; Zeng, Guosun
Author_Institution :
Dept. of Comput. Sci. & Technol., Tongji Univ., Shanghai, China
Abstract :
Partial order reduction techniques have been used to combat the state explosion problem in model checking procedures for concurrent systems with probabilistic behaviors. There are some results that give criteria on applying partial order reduction for verifying quantitative time properties and reward-based properties on actions. However, there are many situations that reward-based properties are expressed on states rather than on actions because actions are triggered in no time and the quantities can not be obtained easily. This paper presents reduction criteria for a probabilistic temporal logic that allows specification of restrictions on quantitative measures given by spatial resources function for the states of the considered system and provides the proof of the correctness.
Keywords :
formal verification; probabilistic logic; temporal logic; Markov decision process; concurrent systems; model checking; partial order reduction techniques; probabilistic behaviors; probabilistic temporal logic; quantitative time property verification; reduction criteria; reward-based property; spatial resource function; state explosion problem; Communication system security; Computer networks; Computer security; Concurrent computing; Educational technology; Embedded computing; Explosions; Information security; Probabilistic logic; Wireless communication; Markov Decision Process; model checking; partial order reduction; spatial restrictions; temporal logic;
Conference_Titel :
Networks Security Wireless Communications and Trusted Computing (NSWCTC), 2010 Second International Conference on
Conference_Location :
Wuhan, Hubei
Print_ISBN :
978-0-7695-4011-5
Electronic_ISBN :
978-1-4244-6598-9
DOI :
10.1109/NSWCTC.2010.232
