Skip to Main content Skip to Navigation
New interface
Conference papers

A Parametrized Propositional Dynamic Logic with Application to Service Synthesis

Walid Belkhir 1 Gisela Rossi 1 Michael Rusinowitch 1 
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We extend propositional dynamic logic (PDL) with variables ranging over an innitedomain. This extension, called parametrized PDL or PPDL for short, is interpretedover parametrized transitions systems whose edges are labeled with letters or variablesand whose states are labeled with non-parametrized propositions. We show that thesatisability problem for PPDL is decidable.We apply these results to the composition problem of web services in presence of con-straints on the global ordering of the message-exchange events between the agents.We express the client specication and the available services as parametrized tran-sitions systems and we express the behavioral constraints as a PPDL formula thatthe generated orchestrator must fulll. It turns out that the model of such a formularepresents the desired orchestrator.
Document type :
Conference papers
Complete list of metadata
Contributor : Michaël Rusinowitch Connect in order to contact the contributor
Submitted on : Wednesday, November 26, 2014 - 5:27:13 PM
Last modification on : Friday, January 21, 2022 - 3:09:05 AM


  • HAL Id : hal-01087829, version 1


Walid Belkhir, Gisela Rossi, Michael Rusinowitch. A Parametrized Propositional Dynamic Logic with Application to Service Synthesis. Advances in Modal Logic, Aug 2014, Groningen, Netherlands. pp.34-53. ⟨hal-01087829⟩



Record views