You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: Birkbeck College » Outputs » Detail

Output details

11 - Computer Science and Informatics

Birkbeck College

Return to search Previous output Next output

Output 14 of 62 in the submission

Article title

Counterexample Generation in Probabilistic Model Checking

Type

D - Journal article

DOI

10.1109/TSE.2009.5

Title of journal

IEEE Transactions on Software Engineering

Article number

Volume number

Issue number

First page of article

241

ISSN of journal

0098-5589

Year of publication

2009

URL

Number of additional authors

Additional information

<7> This is the first paper to investigate the generation of counterexamples in probabilistic model checking. It provides algorithms, complexity analysis, and experimental results for counterexample generation in model checking PCTL and LTL formulas against discrete-time Markov chains and Markov decision processes. This work has been used in probabilistic

abstraction-refinement and assume-guarantee verification; in particular, in the analysis tool PASS http://depend.cs.uni-sb.de/tools/pass/. The paper extends sustantially two heavily cited conference papers presented at TACAS'07 and QEST'08.

Interdisciplinary

Cross-referral requested

Research group

B - Information Management and Web Technologies

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract