## Abstract

UNITY is a model for concurrent specifications with a complete logic

for proving progress properties of the form ``$P$ leads to $Q$''.

UNITY is generalized to U-specifications by giving more freedom to

specify the steps that are to be taken infinitely often. In

particular, these steps can correspond to non-total relations. The

generalization keeps the logic sound and complete. The paper

exploits the generalization in two ways. Firstly, the logic remains

sound when the specification is extended with hypotheses of the form

``$F$ leads to $G$''. As the paper shows, this can make the logic

incomplete. The generalization is used to show that the logic

remains complete, if the added hypotheses ``$F$ leads to $G$''

satisfy ``$F$ unless $G$''.

The main result extends the applicability and completeness of

UNITY logic to proofs that a given concurrent program satisfies

any given formula of LTL, linear temporal logic, without the

next-operator which is omitted because it is sensitive to

stuttering. For this purpose, the program, written as a UNITY

program, is extended with a number of boolean variables. The proof

method relies on implementing the LTL formula, i.e., restricting the

specification in such a way that only those runs remain that satisfy

the formula. This result is a variation of the classical

construction of a B\"uchi automaton for a given LTL formula that

accepts precisely those runs that satisfy the formula.

for proving progress properties of the form ``$P$ leads to $Q$''.

UNITY is generalized to U-specifications by giving more freedom to

specify the steps that are to be taken infinitely often. In

particular, these steps can correspond to non-total relations. The

generalization keeps the logic sound and complete. The paper

exploits the generalization in two ways. Firstly, the logic remains

sound when the specification is extended with hypotheses of the form

``$F$ leads to $G$''. As the paper shows, this can make the logic

incomplete. The generalization is used to show that the logic

remains complete, if the added hypotheses ``$F$ leads to $G$''

satisfy ``$F$ unless $G$''.

The main result extends the applicability and completeness of

UNITY logic to proofs that a given concurrent program satisfies

any given formula of LTL, linear temporal logic, without the

next-operator which is omitted because it is sensitive to

stuttering. For this purpose, the program, written as a UNITY

program, is extended with a number of boolean variables. The proof

method relies on implementing the LTL formula, i.e., restricting the

specification in such a way that only those runs remain that satisfy

the formula. This result is a variation of the classical

construction of a B\"uchi automaton for a given LTL formula that

accepts precisely those runs that satisfy the formula.

Original language | English |
---|---|

Pages (from-to) | 185–205 |

Number of pages | 21 |

Journal | Formal Aspects of Computing |

Volume | 33 |

DOIs | |

Publication status | Published - Mar-2021 |

## Keywords

- concurrency, progress, UNITY, LTL, B\"uchi automaton