Please use this identifier to cite or link to this item:
Title: Probabilistic CTL*: The Deductive Way
Authors: Dimitrova, Rayna
Fioriti, Luis María Ferrer
Hermanns, Holger
Majumdar, Rupak
First Published: 9-Apr-2016
Presented at: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS), Eindhoven, NETHERLANDS
Start Date: 2-Apr-2016
End Date: 8-Apr-2016
Publisher: Springer-Verlag Berlin
Citation: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2016. Lecture Notes in Computer Science, 2016, 9636
Abstract: Complex probabilistic temporal behaviours need to be guaranteed in robotics and various other control domains, as well as in the context of families of randomized protocols. At its core, this entails checking infinite-state probabilistic systems with respect to quantitative properties specified in probabilistic temporal logics. Model checking methods are not directly applicable to infinite-state systems, and techniques for infinite-state probabilistic systems are limited in terms of the specifications they can handle. This paper presents a deductive approach to the verification of countable-state systems against properties specified in probabilistic CTL ∗, on models featuring both nondeterministic and probabilistic choices. The deductive proof system we propose lifts the classical proof system by Kesten and Pnueli to the probabilistic setting. However, the soundness arguments are completely distinct and go via the theory of martingales. Completeness results for the finite-state case and an infinite-state example illustrate the effectiveness of our approach.
Series/Report no.: Lecture Notes in Computer Science book series (LNCS);9636
DOI Link: 10.1007/978-3-662-49674-9_16
ISSN: 0302-9743
ISBN: 978-3-662-49673-2
eISSN: 1611-3349
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Copyright © 2016, Springer-Verlag Berlin. Deposited with reference to the publisher’s open access archiving policy. (
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
tacas16.pdfPost-review (final submitted author manuscript)405.65 kBAdobe PDFView/Open

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