T. Si, (x, u) ? F alors 1 r ? x ? C r

. Soient-r,-r-?-r-tels-que-r-r, Par définition, comme (r, s) ? p, il y a deux cas : -Cas où il existe r ? R tel que r r et Tp : (r , s) ? F : Comme r r et r r alors r r , par transitivité. Donc, comme il existe r ? R tel que r r et Tp : (r , s) ? F, alors nous avons bien (r , s) ? p. -Cas r = ? : Dans ce cas ? r . Comme nous l'avons déjà vu, dans ce cas r = ?. Donc (r , s) ? p. -Inconsistance (BC) : Soit r ? R tel que ? r, Soit p ? Prop et soit s ? S, nous avons par définition de ?, (?, s) ? P . Par (K), que nous venons de démontrer, nous avons alors (r, s) ? P . En conclusion, la propriété (BC) est vérifiée

F. , C. Soit, ?. (. , ·. , R. @bullet et al., C s un Hintikka CSS tel que 1 r ? D r (C r ) et 1 r est un label consistant Les propriétés suivantes sont vérifiées pour toute formule ? : (a) ?, s K ? (b) Si F? : (r, s) ? F et r est consistant alors r, s K ? (c) Si T? : (r, s) ? F et r est consistant alors r, s K ?

·. Preuver and K. Est-un-modèle-dynamique, donc la propriété (a) est vérifiée par le Lemme 3.1.6. Nous démontrons les deux autres propriétés par induction simultanée sur la structure de la formule ?. Nous faisons remarquer que si S? : (r, s) ? F alors, par la propriété (P css ) de la Définition 3.3.12, r ? r ? C r . De plus, comme r est consistant alors r ? r ? C r? , d'où r ? D r (C r? ) Donc r = ?, par définition de ?. -Cas de base -Cas Fp : (r, s) ? F et r est consistant, avec p ? Prop : Supposons que r, s K p. Donc (r, s) ? p. Par la Définition 3.5.2, il existe r ? R tel que r r et Tp : (r , s) ? F. Comme r r et r = ? alors r ? r ? C r? . Comme C r? ? C r alors r ? r ? C r . Donc Tp : (r , s) ? F, Fp : (r, s) ? F

-. Tpr and . Prop, Donc r, s K p. -Cas F : (r, s) ? F et r est consistant : Dans ce cas, F, C r , C s n'est pas un Hintikka CSS par la condition (3) de la Définition 3.5.1. Ceci est absurde, donc ce cas ne peut pas se produire. -Cas T : (r, s) ? F et r est consistant : Par la définition de la relation de forcing, nous avons r, s K . -Cas F? : (r, s) ? F et r est consistant : Supposons que r, s K ?. Par définition, ? r. Comme r = ? alors par définition de ?, ? ? r ? C r? . Or ceci est absurde car ? ? D r (C r? ) Donc r, s K ?. -Cas T? : (r, s) ? F et r est consistant : Dans ce cas, r est inconsistant, or ceci est absurde. Donc ce cas ne peut pas se produire. -Cas FI : (r, s) ? F et r est consistant : Par le condition (2) de la Définition 3.5.1, 1 r ? r ? C r . Comme C r? ? C r alors 1 r ? r ? C r?, nous avons proposé une méthode des tableaux, montré sa correction et sa complétude et nous avons aussi proposé une méthode d'extraction de contre-modèles

D. Concernant, étude d'extensions, en particulier en introduisant la notion de place [17, 22] permettant de localiser les ressources, et à la proposition d'un outil permettant la modélisation et la vérification de propriétés dans des domaines tels que les protocoles, les webservices, systèmes multi-agents... En effet, de tels systèmes sont composés d'agents ou processus échangeant de l'information, pouvant être vue comme une ressource

. Dans-le-chapitre-suivant, nous nous intéressons à la recherche d'une abstraction des modèles de DMBI afin de proposer un noyau logique pour la modélisation et l'expression de propriétés sur des ressources dynamiques. De plus, nous nous intéressons à l'étude de nouvelles modalités multiplicatives, c'est-à-dire en lien avec la séparation

{. , F. ×. , and ×. S?, Un CSS (constrained set of statements) est une paire F, C, où F est un ensemble de formules signées et C est un ensemble de contraintes, vérifiant la propriété (P css ) suivante : si S? : (u, x) ? F alors

C. F. Un, C. Est-fini-ssi, F. , C. Sont-finis, F. et al., La relation est définie par : La relation f est définie par : F f , C f f F, C ssi F f

S. La-liste, T. , ?. , C. ]-?-t-n-est-un-lsm-tableau-pour, and F. , C 0 et 1. T? : (u, x) ? F ou F? : (u, y) ? F ou x ? y ? C 2, FI : (u, x) ? F ou x ? 1 r ? C 3. F : (u, x) ? F 4. T? : (u, x) ? F

T. Si, (u, x) ? F alors x ? 1 r ? C

S. F? and ?. , x ? F alors ?y ? L r , xy ? D r (C) et T? : y ? F et F? : xy ? F

P. A. Abdulla and A. Nylén, Timed Petri Nets and BQOs, Lecture Notes in Computer Science, vol.2075, pp.53-70, 2001.
DOI : 10.1007/3-540-45740-2_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.464.7492

G. Anderson, M. Collinson, and D. Pym, Trust Domains: An Algebraic, Logical, and Utility-Theoretic Approach, 6th International Conference on Trust & Trustworthy Computing, 2013.
DOI : 10.1007/978-3-642-38908-5_18

G. Anderson and D. Pym, Combinators for Trust Domains in Security Modelling, Workshop on Logics for Resources, Processes, and Programs, p.2013

R. Aumman and A. Brandenburger, Epistemic Conditions for Nash Equilibrium, Econometrica, vol.63, issue.5, pp.1161-1180, 1995.
DOI : 10.2307/2171725

A. Avron, Gentzen-type systems, resolution and tableaux, Journal of Automated Reasoning, vol.92, issue.2, pp.265-281, 1993.
DOI : 10.1007/BF00881838

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.20.9771

P. Balbiani and J. Boudou, Decidability of Iteration-free PDL with Parallel Composition, Int Workshop on Automated Deduction : Decidability, Complexity, Tractability, ADDCT'14, 2014.

P. Balbiani, O. Gasquet, and F. Schwarzentruber, Agents that look at one another, Logic Journal of IGPL, vol.21, issue.3, pp.438-467, 2013.
DOI : 10.1093/jigpal/jzs052

URL : https://hal.archives-ouvertes.fr/hal-01138505

P. Balbiani, H. Van-ditmarsch, A. Herzig, and T. Lima, Tableaux for Public Announcement Logic, Journal of Logic and Computation, vol.20, issue.1, pp.55-76, 2010.
DOI : 10.1093/logcom/exn060

A. Baltag, A Logic for Suspicious Players: Epistemic Actions and Belief-Updates in Games, Bulletin of Economic Research, vol.54, issue.1, pp.1-45, 2002.
DOI : 10.1111/1467-8586.00138

A. Baltag, B. Coecke, and M. Sadrzadeh, Algebra and Sequent Calculus for Epistemic Actions, Electronic Notes in Theoretical Computer Science, vol.126, pp.27-52, 2005.
DOI : 10.1016/j.entcs.2004.11.012

A. Baltag, B. Coecke, and M. Sadrzadeh, Epistemic Actions as Resources, Journal of Logic and Computation, vol.17, issue.3, pp.555-585, 2006.
DOI : 10.1093/logcom/exm015

M. R. Benevides, R. P. De-freitas, and J. P. Viana, Propositional Dynamic Logic with Storing, Recovering and Parallel Composition, Electronic Notes in Theoretical Computer Science, vol.269, issue.0, pp.95-107, 2011.
DOI : 10.1016/j.entcs.2011.03.008

URL : http://doi.org/10.1016/j.entcs.2011.03.008

N. Benton, G. Bierman, V. De-paiva, and M. Hyland, A term calculus for Intuitionistic Linear Logic, Int. Conference on Typed Lambda Calculi and Applications, pp.75-90, 1993.
DOI : 10.1007/BFb0037099

B. Berthomieu and M. Diaz, Modeling and verification of time dependent systems using time Petri nets, IEEE Transactions on Software Engineering, vol.17, issue.3, pp.259-273, 1991.
DOI : 10.1109/32.75415

N. Biri and D. Galmiche, A Separation Logic for Resource Distribution, 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS'03, pp.23-37, 2003.
DOI : 10.1007/978-3-540-24597-1_3

URL : https://hal.archives-ouvertes.fr/inria-00099555

P. Blackburn, M. De-rijke, and Y. Venema, Modal logic, 2001.
DOI : 10.1017/CBO9781107050884

URL : https://hal.archives-ouvertes.fr/inria-00100502

L. Cardelli and A. D. Gordon, Anytime, anywhere -modal logics for mobile ambients, 27th ACM Symposium on Principles of Programming Languages, pp.1-13, 2000.

E. Clarke, O. Grumberg, and D. Peled, Model Checking, 1999.

M. Collinson, K. Mcdonald, and D. Pym, A substructural logic for layered graphs, Journal of Logic and Computation, vol.24, issue.4, pp.953-988, 2014.
DOI : 10.1093/logcom/exu002

M. Collinson, B. Monahan, and D. Pym, A Logical and Computational Theory of Located Resource, Journal of Logic and Computation, vol.19, issue.6, pp.1207-1244, 2009.
DOI : 10.1093/logcom/exp021

M. Collinson and D. Pym, Algebra and logic for resource-based systems modelling, Mathematical Structures in Computer Science, vol.10, issue.05, pp.959-1027, 2009.
DOI : 10.1002/malq.19630090502

M. Collinson, D. Pym, and C. Tofts, Erratum : Errata for Formal Aspects of Computing and their consequences, Formal Aspects of Computing, vol.18, issue.19, pp.495-517551, 2006.

H. Comon-lundh and V. Cortier, Security properties : two agents are sufficient, Science of Computer Programming, vol.50, pp.1-351, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00099981

J. R. Courtault and D. Galmiche, A modal extension of Boolean BI for resource transformations, Int. Workshop on Logics for Resources, Processes, and Programs, LRPP'13, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01259775

J. R. Courtault and D. Galmiche, A Modal BI Logic for Dynamic Resource Properties, Logical Foundations of Computer Science, LFCS 2013, pp.134-148, 2013.
DOI : 10.1007/978-3-642-35722-0_10

URL : https://hal.archives-ouvertes.fr/hal-01259770

D. E. Denning and G. M. Sacco, Timestamps in key distribution protocols, Communications of the ACM, vol.24, issue.8, pp.533-536, 1981.
DOI : 10.1145/358722.358740

R. Devillers, H. Klaudel, and M. Koutny, Petri Net Semantics of the Finite ??-Calculus, Formal Techniques for Networked and Distributed Systems, pp.309-325, 2004.
DOI : 10.1007/978-3-540-30232-2_20

URL : https://hal.archives-ouvertes.fr/hal-00340125

E. A. Emerson and E. M. Clarke, Using branching time temporal logic to synthesize synchronization skeletons, Science of Computer Programming, vol.2, issue.3, pp.241-266, 1982.
DOI : 10.1016/0167-6423(83)90017-5

U. Engberg and G. Winskel, Petri Nets as Models of Linear Logic, CAAP 90, pp.144-161, 1990.

U. Engberg, G. J. Winskel-]-m, R. E. Fischer, and . Ladner, Completeness results for Linear Logic on Petri nets Annals of Pure and Applied Logic Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.8633, issue.182, pp.101-135194, 1979.

M. Fitting, First-order Logic and Automated Theorem Proving, 1996.
DOI : 10.1007/978-1-4684-0357-2

D. Galmiche and D. Larchey-wendling, Resource models and proof-search in Intuitionistic Linear Logic, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00099314

D. Galmiche and D. Méry, Semantic Labelled Tableaux for Propositional BI??, Journal of Logic and Computation, vol.13, issue.5, pp.707-753, 2003.
DOI : 10.1093/logcom/13.5.707

URL : https://hal.archives-ouvertes.fr/inria-00099556

D. Galmiche and D. Mery, Characterizing Provability in BI???s Pointer Logic Through Resource Graphs, Int. Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2005, pp.459-473, 2005.
DOI : 10.1007/11591191_32

D. Galmiche, D. Méry, and D. Pym, The semantics of BI and resource tableaux, Mathematical Structures in Computer Science, vol.15, issue.06, pp.1033-1088, 2005.
DOI : 10.1017/S0960129505004858

URL : https://hal.archives-ouvertes.fr/hal-00076735

D. Galmiche and D. Méry, BILL : A theorem prover for propositional BI logic

J. D. Gerbrandy, Bisimulations on Planet Kripke, 1999.

J. Y. Girard, Linear logic, Theoretical Computer Science, vol.50, issue.1, pp.1-102, 1987.
DOI : 10.1016/0304-3975(87)90045-4

URL : https://hal.archives-ouvertes.fr/inria-00075966

R. Goldblatt, Logics of Time and Computation. Logics of Time and Computation, 1987.

D. Harel, J. Tiuryn, and D. Kozen, Dynamic Logic, 2000.

M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol.32, issue.1, pp.137-161, 1985.
DOI : 10.1145/2455.2460

A. Herzig, A Simple Separation Logic, Workshop on Logic, Language, Information and Computation, pp.168-178, 2013.
DOI : 10.1007/978-3-642-39992-3_16

URL : https://hal.archives-ouvertes.fr/hal-01147307

A. Herzig and T. Lima, Epistemic Actions and Ontic Actions: A Unified Logical Framework, Advances in Artificial Intelligence, pp.409-418, 2006.
DOI : 10.1007/11874850_45

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

Z. Hóu, A. Tiu, and R. Goré, A labelled sequent calculus for BBI: proof theory and proof search, Automated Reasoning with Analytic Tableaux and Related Methods, pp.172-187, 2013.
DOI : 10.1093/logcom/exv033

K. Ishihara and K. Hiraishi, The completeness of linear logic for Petri net models, Logic Journal of IGPL, vol.9, issue.4, pp.549-567, 2001.
DOI : 10.1093/jigpal/9.4.549

S. Ishtiaq and P. O. Hearn, BI as an Assertion Language for Mutable Data Structures, 28th ACM Symposium on Principles of Programming Languages, pp.14-26, 2001.

J. Meyer, W. Van-der, and . Hoek, Epistemic Logic for AI and Computer Science. Tracts in Theoretical Computer Science 41, 1995.

B. Kooi, Expressivity and completeness for public update logics via reduction axioms, Journal of Applied Non-Classical Logics, vol.1, issue.2, pp.231-253, 2007.
DOI : 10.1017/CBO9780511569852

D. Lange, M. Oshima, G. Karjoth, and K. Kosaka, Aglets: Programming mobile agents in Java, Worldwide Computing and Its Applications, pp.253-266, 1997.
DOI : 10.1007/3-540-63343-X_52

D. Larchey-wendling, The formal strong completeness of partial monoidal Boolean BI, To appear in Journal of Logic and Computation, 2014.
DOI : 10.1093/logcom/exu031

URL : https://hal.archives-ouvertes.fr/hal-01256932

D. Larchey-wendling and D. Galmiche, Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding, Mathematical Structures in Computer Science, vol.5213, issue.03, pp.1-66, 2009.
DOI : 10.1016/j.entcs.2007.02.020

URL : https://hal.archives-ouvertes.fr/hal-00577929

D. Larchey-wendling and D. Galmiche, The Undecidability of Boolean BI through Phase Semantics, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.140-149, 2010.
DOI : 10.1109/LICS.2010.18

URL : https://hal.archives-ouvertes.fr/hal-00577919

D. Larchey-wendling and D. Galmiche, Nondeterministic Phase Semantics and the Undecidability of Boolean BI, ACM Transactions on Computational Logic, vol.14, issue.1, pp.1-41, 2013.
DOI : 10.1145/2422085.2422091

URL : https://hal.archives-ouvertes.fr/hal-01256956

W. Lenzen, Recent work in epistemic logic, Acta Philosophia Fennica, vol.30, pp.1-219, 1978.

N. Lohmann, A feature-complete Petri net semantics for WS-BPEL 2.0 and its compiler BPEL2oWFN, 2007.

G. Lowe, Breaking and fixing the needham-schroeder public-key protocol using fdr In Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS '96, pp.147-166, 1996.

M. Mathieu and S. Mehrnoosh, Reasoning about Knowledge in Linear Logic : Modalities and Complexity, Logic, Epistemology, and the Unity of Science, pp.327-350, 2003.

P. M. Merlin, A study of the recoverability of computing systems, 1974.

R. Milner, Bigraphs and Their Algebra, Proceedings of the {LIX} Colloquium on Emerging Trends in Concurrency Theory, pp.5-19, 2006.
DOI : 10.1016/j.entcs.2008.04.002

URL : http://doi.org/10.1016/j.entcs.2008.04.002

R. Milner, The Space and Motion of Communicating Agents, 2009.
DOI : 10.1017/CBO9780511626661

R. M. Needham and M. D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.
DOI : 10.1145/359657.359659

P. O. 'hearn, J. Reynolds, and S. Ishtiaq, Local Reasoning about Programs that Alter Data Structures, Computer Science Logic, pp.1-19, 2001.

O. Peter, H. Hearn, and . Yang, Petri net semantics of bunched implications, 1999.

P. W. O-'hearn and D. Pym, Abstract, Bulletin of Symbolic Logic, vol.two, issue.02, pp.215-244, 1999.
DOI : 10.1016/0304-3975(93)90181-R

J. A. Plaza, Logics of public communications Oak Ridge National Laboratory [72] A. Pnueli. The temporal logic of programs, Proc. of the 4th ISMIS Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS '77, pp.201-216, 1977.

D. Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series, 2002.

D. Pym and C. Tofts, A Calculus and logic of resources and processes, Formal Aspects of Computing, vol.6, issue.5, pp.495-517, 2006.
DOI : 10.1007/s00165-006-0018-z

D. Pym and C. Tofts, Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic, Electronic Notes in Theoretical Computer Science, vol.172, pp.545-587, 2007.
DOI : 10.1016/j.entcs.2007.02.020

Y. Moses, R. Fagin, J. Halpern, and M. Vardi, Reasoning About Knowledge, 1995.

J. Reynolds, Separation logic: a logic for shared mutable data structures, Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp.55-74, 2002.
DOI : 10.1109/LICS.2002.1029817

P. Schroeder-heister and K. Dosen, Substructural Logics, 1993.

A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, 1994.

C. Stahl, A Petri Net Semantics for BPEL, Informatik-Berichte, vol.188, 2005.

V. Valero, D. Frutos-escrig, and F. R. Cuartero, On non-decidability of reachability for timed-arc Petri nets, Proceedings 8th International Workshop on Petri Nets and Performance Models (Cat. No.PR00331), pp.188-196, 1999.
DOI : 10.1109/PNPM.1999.796565

J. Van-benthem and F. Liu, Dynamic logic of preference upgrade, Journal of Applied Non-Classical Logics, vol.6, issue.3, pp.157-182, 2007.
DOI : 10.1007/BF00248150

J. Van-benthem, J. Van-eijck, and B. Kooi, Logics of communication and change. Information and Computation, pp.1620-1662, 2006.

H. Van-ditmarsch, The Logic of Pit, Synthese, vol.11, issue.1, pp.343-374, 2006.
DOI : 10.1007/s11229-005-4331-5

H. Van-ditmarsch, Dynamic Epistemic Logic, 2007.
DOI : 10.1007/978-1-4020-5839-4

URL : https://hal.archives-ouvertes.fr/hal-00868361

H. Van-ditmarsch, W. Van-der-hoek, and B. Kooi, Dynamic epistemic logic with assignment, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems , AAMAS '05, pp.141-148, 2005.
DOI : 10.1145/1082473.1082495

M. Woolridge, Introduction to Multiagent Systems, 2001.

D. N. Yetter, Quantales and (noncommutative) linear logic, The Journal of Symbolic Logic, vol.II, issue.01, pp.41-64, 1990.
DOI : 10.1017/S0305004100065403

. Preuve, Les preuves se réalisent en montrant l'inclusion dans les deux sens, cela en faisant une étude par cas

B. Proposition, Pour tout a ? ? Act et toute substitution ?, ?(a) = a

. Preuve, Cas a = 1 : Nous rappelons que, par définition, ?(1 a ) = 1 a et 1 = 1 a . Donc ?(1) = ?(1 a ) = 1 a = 1. -Cas a = 1 : Par définition, comme a ? ? Act alors ?(a) = a et comme a = 1 alors a = a

B. Proposition, Toute propriété de consistance -close peut être étendue en une propriété de consistance alternative -close

. Preuve, Soit P une propriété de consistance -close. Soit P + défini par

. Nous-montrons-que-p-+-est-clos, F. Soit, C. ?. , F. , C. F. et al., (C ) ?(F), ?(C) Comme P est -clos alors ? Nous montrons que P + est une propriété de consistance alternative Par définition, il existe une substitution ? telle que ?(F), ?(C) ? P : 1. Supposons que T? : (x, u) ? F et F? : (y, u) ? F et x ? y ? C, Par définition et par le Corollaire B.7, T? : (?(x), ?(u)) ? ?(F) et F? : (?(y), ?(u)) ? ?(F) et ?(x) ? ?(y) ? ?(C). Or, ceci est absurde parce que P est une propriété de consistance