NDLI: Sound statistical model checking for MDP using partial order and confluence reduction

Content Provider	Springer Nature Link
Author	Hartmanns, Arnd Timmer, Mark
Copyright Year	2014
Abstract	Statistical model checking (SMC) is an analysis method that circumvents the state space explosion problem in model-based verification by combining probabilistic simulation with statistical methods that provide clear error bounds. As a simulation-based technique, it can in general only provide sound results if the underlying model is a stochastic process. In verification, however, models are very often variations of nondeterministic transition systems. In classical exhaustive model checking, partial order reduction and confluence reduction allow the removal of spurious nondeterministic choices. In this paper, we show that both can be adapted to detect and discard such choices on-the-fly during simulation, thus extending the applicability of SMC to a subclass of Markov decision processes. We prove their correctness in a uniform way and study their effectiveness and efficiency using an implementation in the modes simulator for the Modest modelling language. The examples we use highlight the different strengths and limitations of the two approaches. We find that runtime may be affected by unnecessary recomputations, and thus also investigate the feasibility of caching results to speed up simulation at the cost of increased memory usage.
Starting Page	429
Ending Page	456
Page Count	28
File Format	PDF
ISSN	14332779
Journal	International Journal on Software Tools for Technology Transfer
Volume Number	17
Issue Number	4
e-ISSN	14332787
Language	English
Publisher	Springer Berlin Heidelberg
Publisher Date	2014-10-01
Publisher Place	Berlin, Heidelberg
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Statistical model checking Simulation Markov decision processes Partial order reduction Confluence reduction Software Engineering Software Engineering/Programming and Operating Systems Theory of Computation
Content Type	Text
Resource Type	Article
Subject	Information Systems Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Partial-order reduction and trail improvement in directed model checking

Smart sampling for lightweight verification of Markov decision processes

Selected dynamic issues in software model checking

Solving the ignoring problem for partial order reduction

Distributed dynamic partial order reduction

Model checking software: on some new waves and some evergreens

Schedulability of Herschel revisited using statistical model checking

Statistical abstraction and model-checking of large heterogeneous systems

Statistical model checking for biological systems

Sound statistical model checking for MDP using partial order and confluence reduction

Similar Documents

Partial-order reduction and trail improvement in directed model checking

Smart sampling for lightweight verification of Markov decision processes

Selected dynamic issues in software model checking

Solving the ignoring problem for partial order reduction

Distributed dynamic partial order reduction

Model checking software: on some new waves and some evergreens

Schedulability of Herschel revisited using statistical model checking

Statistical abstraction and model-checking of large heterogeneous systems

Statistical model checking for biological systems

Sound statistical model checking for MDP using partial order and confluence reduction