(x, u) ? F alors 1 r ? x ? C 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 ,
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 ? ,
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 ,
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 ,
é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 ,
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 ,
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 ,
La relation est définie par : La relation f est définie par : F f , C f f F, C ssi F 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 ,
(u, x) ? F alors x ? 1 r ? C ,
x ? F alors ?y ? L r , xy ? D r (C) et T? : y ? F et F? : xy ? F ,
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
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
Combinators for Trust Domains in Security Modelling, Workshop on Logics for Resources, Processes, and Programs, p.2013 ,
Epistemic Conditions for Nash Equilibrium, Econometrica, vol.63, issue.5, pp.1161-1180, 1995. ,
DOI : 10.2307/2171725
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
Decidability of Iteration-free PDL with Parallel Composition, Int Workshop on Automated Deduction : Decidability, Complexity, Tractability, ADDCT'14, 2014. ,
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
Tableaux for Public Announcement Logic, Journal of Logic and Computation, vol.20, issue.1, pp.55-76, 2010. ,
DOI : 10.1093/logcom/exn060
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
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
Epistemic Actions as Resources, Journal of Logic and Computation, vol.17, issue.3, pp.555-585, 2006. ,
DOI : 10.1093/logcom/exm015
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
A term calculus for Intuitionistic Linear Logic, Int. Conference on Typed Lambda Calculi and Applications, pp.75-90, 1993. ,
DOI : 10.1007/BFb0037099
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
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
Modal logic, 2001. ,
DOI : 10.1017/CBO9781107050884
URL : https://hal.archives-ouvertes.fr/inria-00100502
Anytime, anywhere -modal logics for mobile ambients, 27th ACM Symposium on Principles of Programming Languages, pp.1-13, 2000. ,
Model Checking, 1999. ,
A substructural logic for layered graphs, Journal of Logic and Computation, vol.24, issue.4, pp.953-988, 2014. ,
DOI : 10.1093/logcom/exu002
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
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
Erratum : Errata for Formal Aspects of Computing and their consequences, Formal Aspects of Computing, vol.18, issue.19, pp.495-517551, 2006. ,
Security properties : two agents are sufficient, Science of Computer Programming, vol.50, pp.1-351, 2004. ,
URL : https://hal.archives-ouvertes.fr/inria-00099981
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
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
Timestamps in key distribution protocols, Communications of the ACM, vol.24, issue.8, pp.533-536, 1981. ,
DOI : 10.1145/358722.358740
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
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
Petri Nets as Models of Linear Logic, CAAP 90, pp.144-161, 1990. ,
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. ,
First-order Logic and Automated Theorem Proving, 1996. ,
DOI : 10.1007/978-1-4684-0357-2
Resource models and proof-search in Intuitionistic Linear Logic, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00099314
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
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
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
BILL : A theorem prover for propositional BI logic ,
Bisimulations on Planet Kripke, 1999. ,
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
Logics of Time and Computation. Logics of Time and Computation, 1987. ,
Dynamic Logic, 2000. ,
Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol.32, issue.1, pp.137-161, 1985. ,
DOI : 10.1145/2455.2460
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
Epistemic Actions and Ontic Actions: A Unified Logical Framework, Advances in Artificial Intelligence, pp.409-418, 2006. ,
DOI : 10.1007/11874850_45
An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969. ,
DOI : 10.1145/363235.363259
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
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
BI as an Assertion Language for Mutable Data Structures, 28th ACM Symposium on Principles of Programming Languages, pp.14-26, 2001. ,
Epistemic Logic for AI and Computer Science. Tracts in Theoretical Computer Science 41, 1995. ,
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
Aglets: Programming mobile agents in Java, Worldwide Computing and Its Applications, pp.253-266, 1997. ,
DOI : 10.1007/3-540-63343-X_52
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
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
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
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
Recent work in epistemic logic, Acta Philosophia Fennica, vol.30, pp.1-219, 1978. ,
A feature-complete Petri net semantics for WS-BPEL 2.0 and its compiler BPEL2oWFN, 2007. ,
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. ,
Reasoning about Knowledge in Linear Logic : Modalities and Complexity, Logic, Epistemology, and the Unity of Science, pp.327-350, 2003. ,
A study of the recoverability of computing systems, 1974. ,
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
The Space and Motion of Communicating Agents, 2009. ,
DOI : 10.1017/CBO9780511626661
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
Local Reasoning about Programs that Alter Data Structures, Computer Science Logic, pp.1-19, 2001. ,
Petri net semantics of bunched implications, 1999. ,
Abstract, Bulletin of Symbolic Logic, vol.two, issue.02, pp.215-244, 1999. ,
DOI : 10.1016/0304-3975(93)90181-R
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. ,
The Semantics and Proof Theory of the Logic of Bunched Implications, volume 26 of Applied Logic Series, 2002. ,
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
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
Reasoning About Knowledge, 1995. ,
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
Substructural Logics, 1993. ,
The Proof Theory and Semantics of Intuitionistic Modal Logic, 1994. ,
A Petri Net Semantics for BPEL, Informatik-Berichte, vol.188, 2005. ,
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
Dynamic logic of preference upgrade, Journal of Applied Non-Classical Logics, vol.6, issue.3, pp.157-182, 2007. ,
DOI : 10.1007/BF00248150
Logics of communication and change. Information and Computation, pp.1620-1662, 2006. ,
The Logic of Pit, Synthese, vol.11, issue.1, pp.343-374, 2006. ,
DOI : 10.1007/s11229-005-4331-5
Dynamic Epistemic Logic, 2007. ,
DOI : 10.1007/978-1-4020-5839-4
URL : https://hal.archives-ouvertes.fr/hal-00868361
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
Introduction to Multiagent Systems, 2001. ,
Quantales and (noncommutative) linear logic, The Journal of Symbolic Logic, vol.II, issue.01, pp.41-64, 1990. ,
DOI : 10.1017/S0305004100065403
Les preuves se réalisent en montrant l'inclusion dans les deux sens, cela en faisant une étude par cas ,
Pour tout a ? ? Act et toute substitution ?, ?(a) = a ,
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 ,
Toute propriété de consistance -close peut être étendue en une propriété de consistance alternative -close ,
Soit P une propriété de consistance -close. Soit P + défini par ,
(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 ,