tailieunhanh - CONCUR 2004 – Concurrency Theory- P12

CONCUR 2004 – Concurrency Theory- P12: 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. | 316 . Groote and T. Willemse A self evident way of solving a single equation is by applying the standard rules of predicate calculus. In order to use these we first define logical implication for our setting. Definition 6. Letp tp be arbitrary predicate formulae. We write p representing logical implication which is defined as implies p Tiefor all data environments and predicate environments We write as a shorthand for p- p and p -Hp. Note that in this definition we used a data environment which is only important if free data variables occur in formulae. In line with the rest of this paper we omit the data environment elsewhere. Lemma 4. Let p and ÿ be predicate formulae such thatp ÿ. Then aX d D p aX rfi. A straightforward but often laborious method for solving an equation aX d D p in X is by means of an iterative approximation of the fixpoint solution of X which is possible as we are dealing with a monotonic operators over a poset. One starts with an initial solution Sq for X being either Xd . for a p or for a v . Then the approximate solutions of the form Xd i p Sn X are calculated repeatedly. A stable approximant is an approximant that is logically equivalent to its next approximation. A stable approximant is in fact the fixpoint solution to the equation. Definition 7. Let p be predicate formulae and X a predicate variable. We inductively define f p X k where k is of sort N. 1. p X and 2. p X k f p X k X . Thus ip p X k represents the result of recursively substituting for X in Note that for any fc N and all predicate formulae ip p the expression ip p X k is a predicate formula. Below we state that p X k and p T X k are approximations of the solution of an equation and that a stable approximant is the solution to an equation. Lemma 5. Let p be a predicate formula and k N be an arbitrary natural number. Then 1. pX X jjX d D V . 2. uX d D p 3- uX d D p T X k . 3. Ifp X k p X k then pX d D X fe pX d D y . 4. If p T X k - p T X k 1 then .