Please use this identifier to cite or link to this item:
Title: Fairness for Infinite-State Systems
Authors: Cook, B.
Khlaaf, H.
Piterman, Nir
First Published: Apr-2015
Presented at: 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, London, UK
Start Date: 11-Apr-2015
End Date: 18-Apr-2015
Publisher: Springer
Citation: Tools and Algorithms for the Construction and Analysis of Systems Lecture Notes in Computer Science Volume 9035, 2015, pp 384-398
Abstract: In this paper we introduce the first known tool for symbolically proving fair-CTL properties of (infinite-state) integer programs. Our solution is based on a reduction to existing techniques for fairness- free CTL model checking via the use of infinite non-deterministic branching to symbolically partition fair from unfair executions. We show the viability of our approach in practice using examples drawn from device drivers and algorithms utilizing shared resources.
Series/Report no.: Lecture Notes in Computer Science;9035
DOI Link: 10.1007/978-3-662-46681-0_30
ISSN: 0302-9743
ISBN: 978-3-662-46680-3
Version: Post-print
Status: Peer-reviewed
Type: Conference Paper
Rights: Archived with reference to SHERPA/RoMEO and publisher website. The final publication is available at Springer via
Description: See also Research Note RN/14/11 UCL Department of Computer Science.
Appears in Collections:Conference Papers & Presentations, Dept. of Computer Science

Files in This Item:
File Description SizeFormat 
paper.pdfPost-review (final submitted)434.1 kBAdobe PDFView/Open

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