In this document we extend Proposal A' for augmenting the formal semantics of PSL with local variables to all of PSL (issue 67). Proposal A' provides semantics for PSL without truncated words, abort and clock operators. In this proposal we augment the entire formal semantics of PSL (including the above constructs) with local variables. In addition, we add semantics for procedural blocks (issue 66), for built-in functions that refer to the past (issue 117) and for clock alignment operators (issue 137).
This document presents the semantics gradually. First it presents the semantics of the base logic, which is the set of FL formulas that (i) do not use the clock operator (ii) do not refer to the past (i.e., do not use past built-in functions) and (iii) do not use local variables or procedural blocks. Then it presents the semantics of the base logic extended with either the clock operator or references to the past or local variables and procedural blocks. Last it presents the overall semantics of linear formulas with no restrictions.
By: Cindy Eisner; Dana Fisman
Published in: H-0256 in 2008
LIMITED DISTRIBUTION NOTICE:
This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.
Questions about this service can be mailed to reports@us.ibm.com .