UNITY and Büchi automata

Research output: Contribution to journalArticleAcademicpeer-review

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.
Original languageEnglish
Pages (from-to)185–205
Number of pages21
JournalFormal Aspects of Computing
Volume33
DOIs
Publication statusPublished - Mar-2021

Keywords

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

Cite this