Please use this identifier to cite or link to this item:
Title: Model Checking Stochastic Systems in PAT
Keywords: Formal Verification, Probabilistic Model Checking, Stochastic Systems, Real-time Systems, Multi-agent Systems, PAT
Issue Date: 12-Aug-2013
Citation: 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.
Appears in Collections:Ph.D Theses (Open)

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



Page view(s)

checked on Nov 24, 2020


checked on Nov 24, 2020

Google ScholarTM


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