Please use this identifier to cite or link to this item: http://scholarbank.nus.edu.sg/handle/10635/48654
Title: Model Checking Stochastic Systems in PAT
Authors: SONG SONGZHENG
Keywords: Formal Verification, Probabilistic Model Checking, Stochastic Systems, Real-time Systems, Multi-agent Systems, PAT
Issue Date: 12-Aug-2013
Source: SONG SONGZHENG (2013-08-12). Model Checking Stochastic Systems in PAT. ScholarBank@NUS Repository.
Abstract: Stochastic systems are useful in modelling real-world complicated systems. Automatic verification of stochastic systems is important but challenging. Previous work on specifying and verifying stochastic systems relies on simple modeling languages like PRISM. Reasoning complicated stochastic systems however requires not only efficient verification algorithms but also expressive modeling languages. In this thesis, we first propose a formal modeling language called PCSP for discrete probabilistic systems. Hierarchical structure, shared variables, concurrency and probability are all supported in PCSP, which allow us to model a variety of systems. Under the PAT framework, we have developed a verification system for PCSP and it can efficiently support reachability checking, LTL checking, reward checking and trace refinement checking. Second, we extend PCSP to support Probabilistic Real-Time Systems and build the PRTS verification module in PAT. In addition, we develop a novel divide-conquer approach to speed up the reachability analysis. Besides standard application domains of stochastic system, we apply our technique and tool in a novel domain: multi-agent systems. The experimental results have demonstrated the effectiveness of our approaches proposed by comparing with the existing State-of-the art tools.
URI: http://scholarbank.nus.edu.sg/handle/10635/48654
Appears in Collections:Ph.D Theses (Open)

Show full item record
Files in This Item:
File Description SizeFormatAccess SettingsVersion 
SongSZ.pdf1.49 MBAdobe PDF

OPEN

NoneView/Download

Page view(s)

117
checked on Dec 11, 2017

Download(s)

161
checked on Dec 11, 2017

Google ScholarTM

Check


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.