Propositional Dynamic Logic for Structured Data: A Graph Calculus Approach

old_uid11805
titlePropositional Dynamic Logic for Structured Data: A Graph Calculus Approach
start_date2012/11/12
schedule17h30-19h30
onlineno
location_infoGrande Salle
summaryAn extension of Propositional Dynamic Logic (PDL) is proposed for coping with mutable data structures, updates and parallelism. These situations appear often in computing, when one deals with the dynamic changes occurring during the execution of a program. Propositional Dynamic Logic (PDL)is a modal logic for representing properties of sequential programs and reasoning about them. The set of programs has an algebraic structure, so that one can express composition, non-deterministic choice and iteration of programs. PDL, though adequate for sequential programs, is not quite so adequate for other features such as parallelism and concurrency.    In this talk, we will explore the use of algebraic features, such as fork algebra, to enhance the expressive power of PDL. We also present a graph calculus approach to PDL which further enriches its expressive power.     ACKNOWLEDGEMENTS. This research is partly sponsored by the Brazilian agencies CNPq and FAPERJ. This is a joint work with Mario R. F. Benevides and Paulo A. S. Veloso.
responsiblesPataut, Dubucs, Panza