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

?. Soient-r,-r-?-?-r-tels-que-r, ?. , ?. Tel-que-r-??-?-r, and . Tp, Par définition, comme (r, s) ? p, il y a deux cas : -Cas où il existe r (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? . Par définition de ? et comme r = ? alors e ? r. Donc r, s K I. 4.7. Complétude de la méthode des tableaux pour DMBI Conclusion Dans ce chapitre, nous avons présenté une extension de DBI, nommée DMBI, 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

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

. ]. De, et (5.) nous pouvons déduire que s 1
URL : https://hal.archives-ouvertes.fr/jpa-00241696

. Si, TI : 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

S. Fk-u-?-x-?-f-alors-?y-?-l-r,-x-?-u-y and ?. C. F?, Si T K u ? : x ? F alors ?y ? L r , x ? u y ? C et T? : y ? F 6.3. Une méthode des tableaux pour ESL 21

. Preuve, La preuve est similaire à celle de la Proposition 4

. Preuve, Pour cela, il convient de démontrer dans un premier temps que ?(F, C) est un modèle au sens de la Définition 6.1.2. Puis, dans un second temps, nous démontrons que si F? : x ? F alors [x] M ? et si T? : x ? F alors

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://www.it.uu.se/research/docs/fm/apv/tools/tpns/files/bqo.pdf

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://www.math.tau.ac.il/~aa/articles/gentzen_jar.ps.gz

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.3, issue.3, pp.438-467, 2013.
DOI : 10.1002/(SICI)1098-111X(200002)15:2<129::AID-INT3>3.0.CO;2-T

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.204, issue.1, pp.55-76, 2010.
DOI : 10.1016/j.ic.2006.04.006

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

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-00100503

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.36, issue.13, pp.953-988, 2014.
DOI : 10.1016/j.eswa.2008.07.090

M. Collinson, B. Monahan, and D. Pym, A Logical and Computational Theory of Located Resource, Journal of Logic and Computation, vol.6, 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

J. R. Courtault, D. Galmiche, and D. Pym, A logic of separating modalities, Theoretical Computer Science, vol.637, 2015.
DOI : 10.1016/j.tcs.2016.04.040

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/BFb0029994

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

J. and M. Dunn, Relevance Logic and Entailment, Handbook of Philosophical Logic, pp.117-224, 1986.
DOI : 10.1007/978-94-009-5203-4_3

E. A. Emerson and E. M. Clarke, Using branching time temporal logic to synthesize synchronization skeletons, CAAP 90, pp.241-266, 1982.
DOI : 10.1016/0167-6423(83)90017-5

U. Engberg and G. Winskel, Completeness results for linear logic on Petri nets, Annals of Pure and Applied Logic, vol.86, issue.2, pp.101-135, 1997.
DOI : 10.1016/S0168-0072(96)00024-3

M. J. Fischer and R. E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.2, pp.194-211, 1979.
DOI : 10.1016/0022-0000(79)90046-1

M. Fitting, First-order Logic and Automated Theorem Proving, 1996.

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

URL : http://www.utdallas.edu/~kxh060100/cs6371fa07/hoare.pdf

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.2307/421090

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.1007/s11229-005-3384-9

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.1017/S0960129509007567

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

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 Unpublished draft. [72] P.W. O'Hearn and D. Pym. The Logic of Bunched Implications, Bulletin of Symbolic Logic, vol.5, issue.2, pp.215-244, 1999.

J. A. Plaza, Logics of public communications, Proc. of the 4th ISMIS, pp.201-216, 1989.
DOI : 10.1007/s11229-007-9168-7

A. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

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/978-1-4757-3550-5

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.

S. Read, Relevant Logic : A Philosophical Examination of, Inference. B. Blackwell, 1988.

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.1017/CBO9780511569852

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

T. Supposons-que, Supposons maintenant que F, C ? {1 r ? x} ? P (il existe un µ-tableau clos pour ce CSS) Par la règle TI, [F, C ? {1 r ? x}] est un µ-tableau pour F, C. Donc F, C a un µ-tableau clos

?. Supposons-que-t?, C. ?. ?}, C. P. Par-la-règle, T. ?. , and C. , Supposons maintenant que F ?{F?, Alors F, C a un µ-tableau clos, ce qui est contradictoire. En conséquence F ? {F? : (x, u)}, C ? P ou F ? {T?

C. P. Supposons-que-f?-?-?-u-)-}, F. ?. Par-la-règle, and C. {t?}, F? : (x, u)}, C] est un µ-tableau pour F, C. Donc F, C a un µ-tableau clos, ce qui est contradictoire, En conséquence F ? {T? : (x, u)

*. Supposons-que-t?, C. ?}, ?. ?-{c-i-c-j, ?. P. Par-la-règle, and T. *. , Choisissons c i = c j ? ? r \A r (C) (ces constantes existent car ? r est infini et A r (C) est fini parce que C est fini) Supposons maintenant que F ?{T? : (c i , u) T? : (c j , u)}, C ? {c i c j ? x}] est un µ-tableau pour F, C. Donc F, C a un µ-tableau clos, ce qui est contradictoire, T? : (c j , u)}, C ?{c i c j ? x} ? P

T. Supposons-que, Comme P est une propriété de consistance alors ?(F), ?(C) ? {1 r ? ?(x)} ? P. Comme ?(1 r ) = 1 r alors ?(F), ?(C) ? {?(1 r ) ? ?(x)} ? P, Par la Proposition B, vol.9

?. Supposons-que-t? and C. , Comme P est une propriété de consistance alors ?(F)?{F? : (?(x), ?(u))

?. Supposons-que-f? and C. , Comme P est une propriété de consistance alors ?(F) ? {T? : (?(x), ?(u)), F? : (?(x), ?(u))}, ?(C) ? P, F? : (x, u)}), ?(C) ? P. Donc F ? {T? : (x, u)

*. Supposons-que-t?, Alors T? * ? : (?(x), ?(u)) ? ?(F) Soit c i , c j ? ? r \A r (C), tels que c i = c j