ASSUMPTION GUARANTEE SPECIFICATIONS IN LINEAR-TIME TEMPORAL LOGIC/

An assumption/guarantee specification of a system consists of an assum ption part, which specifies the assumptions on the behavior of the env ironment, and a guarantee part, which specifies the properties guarant eed by the system if the environment obeys the assumptions. A suitable interpretation of an assumption/guarantee specification was essential ly formulated by Misra and Chandy (1981). The interpretation was later extended by others to allow liveness properties in the guarantee part . In this paper, we explore the use of linear-time temporal logic in w riting and reasoning about assumption/guarantee specifications. We cho ose this logic, specifically LTL defined in the book by Manna and Pnue li (1992), for the following reasons: (i) Linear-time temporal logics, including LTL and TLA, have proven to be a successful formalism for t he specification and verification of concurrent systems. (ii) Previous works on assumption/guarantee specifications typically reason about r elevant properties at the semantic level or define a special-purpose l ogic. We feel it is beneficial to formulate such specifications in a m ore widely used formalism. (iii) We find that, with past temporal oper ators, LTL admits a succinct syntactic formulation of assumption/guara ntee specifications. This contrasts, in particular, with the work by A badi and Lampost using TLA, where working at the syntactic level is mo re complicated. We derive inference rules for refining and composing a ssumption/guarantee specifications as the main results of this paper. The derived rules can handle internal variables. We had to overcome a number of technical problems in this pursuit, in particular, the probl em of extracting the safety closure of a temporal formula. As a by-pro duct, we identify general conditions under which the safety closure ca n be expressed in a succinct way that facilitates syntactic manipulati on.