NDLI: Verification of linear duration properties over continuous-time markov chains

Content Provider	ACM Digital Library
Author	Kwiatkowska, Marta Chen, Taolue Diciolla, Marco Mereacre, Alexandru
Copyright Year	2013
Abstract	Stochastic modelling and algorithmic verification techniques have been proved useful in analysing and detecting unusual trends in performance and energy usage of systems such as power management controllers and wireless sensor devices. Many important properties are dependent on the cumulated time that the device spends in certain states, possibly intermittently. We study the problem of verifying continuous-time Markov Chains (CTMCs) against Linear Duration Properties (LDP), that is, properties stated as conjunctions of linear constraints over the total duration of time spent in states that satisfy a given property. We identify two classes of LDP properties, Eventuality Duration Properties (EDP) and Invariance Duration Properties (IDP), respectively referring to the reachability of a set of goal states, within a time bound; and the continuous satisfaction of a duration property over an execution path. The central question that we address is how to compute the probability of the set of infinite timed paths of the CTMC that satisfy a given LDP. We present algorithms to approximate these probabilities up to a given precision, stating their complexity and error bounds. The algorithms mainly employ an adaptation of uniformisation and the computation of volumes of multidimensional integrals under systems of linear constraints, together with different mechanisms to bound the errors.
Starting Page	1
Ending Page	35
Page Count	35
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/2528935
Volume Number	14
Issue Number	4
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-11-28
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Markovian reward models Model checking Continuous-time Markov chains Linear duration properties
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

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

Model-checking continuous-time Markov chains

Verification of linear duration properties over continuous-time markov chains

Verification of linear duration properties over continuous-time markov chains

Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains

Model-Checking Linear-Time Properties of Quantum Systems

Model Checking of Recursive Probabilistic Systems

Datalog LITE: a deductive query language with linear time model checking

Verification of linear duration properties over conitnuous time Markov chains (2012)

Quantitative languages

Verification of linear duration properties over continuous-time markov chains

Similar Documents

Model-checking continuous-time Markov chains

Verification of linear duration properties over continuous-time markov chains

Verification of linear duration properties over continuous-time markov chains

Decidability of Approximate Skolem Problem and Applications to Logical Verification of Dynamical Properties of Markov Chains

Model-Checking Linear-Time Properties of Quantum Systems

Model Checking of Recursive Probabilistic Systems

Datalog LITE: a deductive query language with linear time model checking

Verification of linear duration properties over conitnuous time Markov chains (2012)

Quantitative languages

Verification of linear duration properties over continuous-time markov chains