Defining Fairness in Reactive and Concurrent Systems

Abstract

We define when a linear-time temporal property is a fairness property with respect to a given system. This captures the essence shared by most fairness assumptions that are used in the specification and verification of reactive and concurrent systems, such as weak fairness, strong fairness, k-fairness, and many others. We provide three characterizations of fairness: a language-theoretic, a game-theoretic, and a topological characterization. It turns out that the fairness properties are the sets that are “large” from a topological point of view, that is, they are the co-meager sets in the natural topology of runs of a given system.

This insight provides a link to probability theory where a set is “large” when it has measure 1. While these two notions of largeness are similar, they do not coincide in general. However, we show that they coincide for ω-regular properties and bounded Borel measures. That is, an ω-regular temporal property of a finite-state system has measure 1 under a bounded Borel measure if and only if it is a fairness property with respect to that system.

The definition of fairness leads to a generic relaxation of correctness of a system in linear-time semantics. We define a system to be fairly correct if there exists a fairness assumption under which it satisfies its specification. Equivalently, a system is fairly correct if the set of runs satisfying the specification is topologically large. We motivate this notion of correctness and show how it can be verified in a system.

References

1. Abadi, M. and, Lamport, L. 1991. The existence of refinement mappings. Theoret. Comput. Sci. 82, 253--284.
2. Abadi, M., Lamport, L., and Wolper, P. 1989. Realizable and unrealizable specifications of reactive systems. In Proceedings of the 16th International Colloquium on Automata, Languages and Programming. Springer-Verlag, 1--17.
3. Alpern, B. and Schneider, F. B. 1985. Defining liveness. Inf. Proc. Lett. 21, 181--185.
4. Alur, R. and Henzinger, T. A. 1994. Finitary fairness. In Proceedings of 9th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 52--61.
5. Alur, R. and Henzinger, T. A. 1995. Local liveness for compositional modeling of fair reactive systems. In Proceedings of 7th International Conference on Computer Aided Verification. Lecture Notes in Computer Science Series, vol. 939, Springer, 166--179.
6. Apt, K. R., Francez, N., and Katz, S. 1988. Appraising fairness in languages for distributed programming. Dist. Comput. 2, 226--241.
7. Asarin, E., Chane-Yack-Fa, R., and Varacca, D. 2010. Fair adversaries and randomization in two-player games. In Proceedings of 13th FOSSACS. Lecture Notes in Computer Science Series, vol. 6014, Springer, 64--78.
8. Attie, P. C., Francez, N., and Grumberg, O. 1993. Fairness and hyperfairness in multi-party interactions. Dist. Comput. 6, 245--254.
9. Baier, C. and Kwiatkowska, M. Z. 1998. On the verification of qualitative properties of probabilistic processes under fairness constraints. Inf. Proc. Lett. 66, 2, 71--79.
10. Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., and Größer, M. 2008. Almost-sure model checking of infinite paths in one-clock timed automata. In Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 217--226.
11. Ben-Eliyahu, R. and Magidor, M. 1996. A temporal logic for proving properties of topologically general executions. Inf. Comput. 124, 2, 127--144.
12. Berwanger, D., Grädel, E., and Kreutzer, S. 2003. Once upon a time in a west - determinacy, definability, and complexity of path games. In Proceedings of 10th LPAR. Lecture Notes in Computer Science Series, vol. 2850, Springer, 229--243.
13. Best, E. 1984. Fairness and conspiracies. Inf. Proc. Lett. 18, 215--220. (Erratum ibidem 19:162).
14. Clarke, E. M., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Prog. Lang. Sys. 8, 2, 244--263.
15. Courcoubetis, C. and Yannakakis, M. 1995. The complexity of probabilistic verification. J. ACM 42, 4, 857--907.
16. Darondeau, P., Nolte, D., Priese, L., and Yoccoz, S. 1992. Fairness, distances and degrees. Theoret. Comput. Sci. 97, 1, 131--142.
17. Dugundji, J. 1966. Topology. Allyn and Bacon.
18. Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). MIT Press and Elsevier, 995--1072.
19. Fich, F. E. and Ruppert, E. 2003. Hundreds of impossibility results for distributed computing. Dist. Comput. 16, 2-3, 121--163.
20. Francez, N. 1986. Fairness. Springer.
21. Grädel, E. 2008. Banach-Mazur games on graphs. In Proceedings of the 28th FSTTCS. LIPIcs 2 Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik.
22. Jaeger, M. 2009. On fairness and randomness. Inf. Comput. 207, 9, 909--922.
23. Joung, Y.-J. 1999. Localizability of fairness constraints and their distributed implementations. In Proceedings of 10th CONCUR. Lecture Notes in Computer Science Series, vol. 1664, Springer, 336--351.
24. Joung, Y.-J. 2001. On fairness notions in distributed systems, part I: A characterization of implementability. Inf. Comput. 166, 1--34.
25. Kupferman, O. 1999. Augmenting branching temporal logics with existential quantification over atomic propositions. J. Logic. Comput. 9, 2, 135--147.
26. Kupferman, O. and Vardi, M. Y. 2006. Memoryful branching-time logic. In Proceedings of 21st Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 265--274.
27. Kwiatkowska, M. Z. 1989. Survey of fairness notions. Inf. Softw. Tech. 31, 7, 371--386.
28. Kwiatkowska, M. Z. 1991. On topological characterization of behavioural properties. In Topology and Category Theory in Computer Science, G. Reed, A. Roscoe, and R. Wachter Eds., Oxford University Press, 153--177.
29. Lamport, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 2, 125--143.
30. Lamport, L. 2000. Fairness and hyperfairness. Dist. Comput. 13, 4, 239--245.
31. Landweber, L. H. 1969. Decision problems for omega-automata. Math. Syst. Theory 3, 4, 376--384.
32. Lehmann, D. and Shelah, S. 1982. Reasoning with time and chance. Inf. Control 53, 3, 165--198.
33. Lehmann, D. J., Pnueli, A., and Stavi, J. 1981. Impartiality, justice and fairness: The ethics of concurrent termination. In Proceedings of 8th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science Series, vol. 115, Springer, 264--277.
34. Lichtenstein, O., Pnueli, A., and Zuck, L. D. 1985. The glory of the past. In Proceedings of the Conference on Logic of Programs. Lecture Notes in Computer Science Series, vol. 193, Springer, 196--218.
35. Manna, Z. and Pnueli, A. 1990. A hierarchy of temporal properties. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing. ACM, 377--408.
36. Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems -- Specification. Springer.
37. Mauldin, R. D. 1981. The Scottish Book: Mathematics from the Scottish Cafe. Birkhäuser.
38. Murata, T. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4, 541--580.
39. Oxtoby, J. C. 1957. The Banach-Mazur game and Banach category theorem. In Contributions to the Theory of Games, Vol. III. Annals of Mathematical Studies Series, vol. 39, Princeton University Press, 159--163.
40. Oxtoby, J. C. 1971. Measure and Category. A Survey of the Analogies between Topological and Measure Spaces. Springer.
41. Pistore, M. and Vardi, M. Y. 2003. The planning spectrum - one, two, three, infinity. In Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 234--243.
42. Pnueli, A. 1983. On the extremely fair treatment of probabilistic algorithms. In Proceedings of the 15th Annual Symposium on Theory of Computing. ACM, 278--290.
43. Reisig, W. 1985. Petri Nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series Series, vol. 4, Springer.
44. Schmalz, M. 2007. Extensions of an algorithm for generalised fair model checking. M.S. thesis, Technisch-Naturwissenschaftliche Fakultät, Universität zu Lübeck, Germany.
45. Schmalz, M., Völzer, H., and Varacca, D. 2007. Model checking almost all paths can be less expensive than checking all paths. In Proceedings of 27th FSTTCS. Lecture Notes in Computer Science Series, vol. 4855, Springer, 532--543.
46. Schmalz, M., Varacca, D., and Völzer, H. 2009. Counterexamples in probabilistic LTL model checking for Markov chains. In Proceedings of 20th CONCUR. Lecture Notes in Computer Science Series, vol. 5710, Springer, 587--602.
47. Smyth, M. B. 1992. Topology. In Handbook of Logic in Computer Science, S. Abramsky, D. M. Gabbay, and T. Maibaum Eds. Vol. 1: Background: Mathematical Structures. Oxford University Press, 641--761.
48. Spitzer, F. 2001. Principles of Random Walk. Springer.
49. Telgársky, R. 1987. Topological games: On the 50th anniversary of the Banach-Mazur game. Rocky Mountain J. Math. 17, 2, 227--276.
50. Thomas, W. 1990. Automata on infinite objects. In Handbook of Theoretical Computer Science, J. van Leeuwen Ed., Vol. B: Formal Models and Semantics. Elsevier.
51. Varacca, D. and Völzer, H. 2006. Temporal logics and model checking for fairly correct systems. In Proceedings of 21st LICS. IEEE Computer Society, 389--398.
52. Vardi, M. Y. 1985. Automatic verification of probabilistic concurrent finite-state programs. In Proceedings of 26th Foundation of Computer Science. 327--338.
53. Völzer, H. 2002. Refinement-robust fairness. In Proceedings of 13th CONCUR. Lecture Notes in Computer Science Series, vol. 2421, Springer, 547--561.
54. Völzer, H. 2005. On conspiracies and hyperfairness in distributed computing. In Proceedings of 19th DISC. Lecture Notes in Computer Science Series, vol. 3724, Springer, 33--47.
55. Völzer, H., Varacca, D., and Kindler, E. 2005. Defining fairness. In Proceedings of 16th CONCUR. Lecture Notes in Computer Science Series, vol. 3653, Springer, 458--472.
56. Williams, D. 1991. Probability with Martingales. Cambridge University Press.
57. Zuck, L. D., Pnueli, A., and Kesten, Y. 2002. Automatic verification of probabilistic free choice. In Proceedings of 3rd VMCAI, Revised Papers. Lecture Notes in Computer Science Series, vol. 2294, Springer, 208--224.

Index Terms

• Theory of computation

  • Logic

  • Semantics and reasoning

    • Program reasoning