CONCUR 2004 – Concurrency Theory- P19: The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency and promote its applications. Interest in this topic is continually growing, as a consequence of the importance and ubiquity of concurrent systems and their applications, and of the scientific relevance of their foundations. | 526 M. Viswanathan and R. Viswanathan decode Prop0 Prop Prop Prop0 Prop Prop Iinit Prop flc-sem Prop Prop flc-diag Prop with the HFL formula flc-diag expressing a property of the form prescribed by Theorem 2. The properties of the terms decode and init defined in Table 4 are given by the following theorem Theorem 3. Let p be a closed well-named FLCformula over the action set A. 1. Consider any subformula ip e SF ip and FLC environment rjt V 2S- 2S . For any function Fr e F lfProp0 Prop Prop such that Fv FPlf x rfx for every x free in ip 7 decode F7 T 2. T init M The heart of the construction is decode that shows how to decode in HFL the transition system representing an FLC formula. Its definition given in Table 4 is easiest understood on the basis of its property given in Theorem 3 with the A-bound variable e read as standing for the function F representing an environment 7 and the A-bound variable x in each of the cases read as standing for the singleton set ip . On an argument ip the formula is decoded in cases according to its outermost form which in turn is inferred based on which of the propositional constants pi pv . holds in x standing for 0 . For all constructs other than variables and fixed points their corresponding cases can be understood by close analogy with the HFL-translation of these constructs given in Table 3 together with the understanding that lc x and rc x yield singleton sets including the corresponding subformulas of ip and that for constant literals term ev x yields the set of states in which the literal ip holds. If ip is a variable we evaluate the environment on the set FP ip as given by the property of F which is yielded by the term ev x. If ip is a fixed point formula we correspondingly bind using p or v a new variable f and decode the subformula of ip given by lc x but in an environment that is obtained by modifying the current environment e to map ip given by x to f the case-term used for the environment argument to d in the fixed .
