@inbook {IOPORT.05795636,
    author       = {Long, Teng and Zhang, Wenhui},
    title        = {Auxiliary constructs for proving liveness in compassion discrete systems.},
    year         = {2010},
    booktitle    = {Automated technology for verification and analysis. 8th international symposium, ATVA 2010, Singapore, September 21-24, 2010. Proceedings},
    isbn         = {978-3-642-15642-7},
    pages        = {276-290},
    publisher    = {Berlin: Springer},
    doi          = {10.1007/978-3-642-15643-4_21},
    abstract     = {Summary: For proving response properties in systems with compassion requirements, a deductive rule is introduced in [1]. In order to use the rule, auxiliary constructs are needed. They include helpful assertions and ranking functions defined on a well-founded domain. The work in [2] computes ranking functions for response properties in systems with justice requirements. This paper presents an approach which extends the work in [2] with compassion requirements. The approach is illustrated on two examples of sequential and concurrent programs.},
    identifier   = {05795636},
}