Fairness for Infinite-State Systems

Heidy Khlaaf

5th March 2015 (Thursday), 10:00 in ADR LG26

Slides: click here


In model checking, fairness allows us to bridge between linear-time (trace-based) and branching-time (state-based) reasoning. When proving state-based CTL properties, we must often use fairness to model trace-based assumptions about the environment both in a sequential setting, and when reasoning about concurrent environments, where fairness is used to abstract away the scheduler. In this talk, I will introduce the first-known fair-CTL model checking technique for integer programs. Our solution reduces fair-CTL to fairness-free CTL using prophecy variables to encode a partition of fair from unfair paths.

Share this page:

Contact Us

Admissions Enquiries:
BSc: +44 (0) 116 252 5280
MSc: +44 (0) 116 252 2265
E: BSc  seadmissions@le.ac.uk
E: MSc  pgadmissions@le.ac.uk

Departmental Enquiries:
T: +44 (0) 116 252 2129/3887
F: +44 (0) 116 252 3604
E: csadmin@mcs.le.ac.uk

Dept of Informatics
University of Leicester
Leicester, LE1 7RH
United Kingdom


DisabledGo logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has a detailed accessibility guide for the Informatics Building.