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, 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.
Type de document :
Communication dans un congrès
Advances in Modal Logic, Aug 2014, Groningen, Netherlands. 10, pp.34-53, 2014, Advances in Modal Logic
Liste complète des métadonnées

https://hal.inria.fr/hal-01087829
Contributeur : Michaël Rusinowitch <>
Soumis le : mercredi 26 novembre 2014 - 17:27:13
Dernière modification le : jeudi 15 février 2018 - 08:48:14

Identifiants

  • 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. 10, pp.34-53, 2014, Advances in Modal Logic. 〈hal-01087829〉

Partager

Métriques

Consultations de la notice

248