Fairness and priority in progress property analysis
File(s)DTR99-3.pdf (216.32 KB)
Technical report
Author(s)
Giannakopoulou, Dimitra
Magee, Jeffrey
Kramer, Jeff
Type
Report
Abstract
The liveness characteristics of a system are intimately related to the notion of fairness. However, the task of modelling explicitly fairness constraints is complicated in practice. To address this issue, we propose to check LTS (Labelled Transition System) models under a strong fairness assumption, which can be relaxed with the use of action priority. The combination of the two provides a novel and practical way of dealing with fairness. The approach is presented in the context of a class of liveness properties termed progress, for which it yields an efficient model-checking algorithm. Progress properties cover a wide range of interesting properties of systems, while presenting a clear intuitive meaning to users. An extensive comparison is provided of the approach proposed with classical LTL model-checking.
Date Issued
1999-01-01
Citation
Departmental Technical Report: 99/2, 1999, pp.1-29
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
29
Journal / Book Title
Departmental Technical Report: 99/2
Copyright Statement
© 1999 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published