Please use this identifier to cite or link to this item:
https://scholarbank.nus.edu.sg/handle/10635/48654
DC Field | Value | |
---|---|---|
dc.title | Model Checking Stochastic Systems in PAT | |
dc.contributor.author | SONG SONGZHENG | |
dc.date.accessioned | 2013-12-31T18:27:27Z | |
dc.date.available | 2013-12-31T18:27:27Z | |
dc.date.issued | 2013-08-12 | |
dc.identifier.citation | SONG SONGZHENG (2013-08-12). Model Checking Stochastic Systems in PAT. ScholarBank@NUS Repository. | |
dc.identifier.uri | http://scholarbank.nus.edu.sg/handle/10635/48654 | |
dc.description.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. | |
dc.language.iso | en | |
dc.subject | Formal Verification, Probabilistic Model Checking, Stochastic Systems, Real-time Systems, Multi-agent Systems, PAT | |
dc.type | Thesis | |
dc.contributor.department | NUS GRAD SCH FOR INTEGRATIVE SCI & ENGG | |
dc.contributor.supervisor | DONG JIN SONG | |
dc.description.degree | Ph.D | |
dc.description.degreeconferred | DOCTOR OF PHILOSOPHY | |
dc.identifier.isiut | NOT_IN_WOS | |
Appears in Collections: | Ph.D Theses (Open) |
Show simple item record
Files in This Item:
File | Description | Size | Format | Access Settings | Version | |
---|---|---|---|---|---|---|
SongSZ.pdf | 1.49 MB | Adobe PDF | OPEN | None | View/Download |
Google ScholarTM
Check
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.