Skip to Main content Skip to Navigation
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.
Complete list of metadatas

https://hal.inria.fr/hal-01087829
Contributor : Michaël Rusinowitch <>
Submitted on : Wednesday, November 26, 2014 - 5:27:13 PM
Last modification on : Wednesday, January 8, 2020 - 2:17:08 PM

Identifiers

  • HAL Id : hal-01087829, version 1

Citation

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⟩

Share

Metrics

Record views

386