Abstract Unification problems can be formulated and investigated in an algebraic setting, by identifying substitutions to modal algebra homomorphisms. This opens the door to applications of the notorious duality between Heyting or modal algebras and descriptive frames. Through substantial use of this correspondence, we give a necessary and sufficient condition for formulas to be projective. A close inspection of this characterization will motivate a generalization of standard unification, which we dub relative unification. Applying this result to a number of different logics, we then obtain new proofs of their projective—or non-projective—character. Aside from reproving known results, we show that the projective extensions of $\textbf{K5}$ are exactly the extensions of $\textbf{K45}$. This resolves the open question of whether $\textbf{K5}$ is projective.

We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it directly.

Abstract We investigate intuitionistic modal logics with locally interpreted $$\square $$ □ and $$\lozenge $$ ◊ . The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. Additionally, we present bi-nested calculi for LIK and these extensions, providing both a decision procedure and a procedure of finite countermodel extraction.

We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the logic contains dynamic modalities for making announcements and for receiving them. What an agent believes is a function of her initial uncertainty and of the announcements she has received. Beliefs need not be truthful, because announcements already made may not yet have been received. As announcements are true when sent, certain message sequences can be ruled out, just like inconsistent cuts in distributed computing. We provide a complete axiomatization for this asynchronous announcement logic ( AA ). It is a reduction system that also demonstrates that any formula in AA is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in AA closes our investigation.

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Gödel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.

International audience

In the days of its foundation, the field of science covered by UNIF – a series of annual international workshops on unification – was still in its infancy. With the advent of automated reasoning, term rewriting, logic programming, natural language processing, and program analysis, the areas of computer science concerned by unification were seething with excitement. With the coming out of researches in constraint solving and admissibility of inference rules and with the breaking out of applications, such as type checking, query answering, and cryptographic protocol analysis, the development of unification was not long in going at full speed.

We consider intuitionistic variants of linear temporal logic with “next,” “until,” and “release” based on expanding posets : partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic that we denote ITL e , and by imposing additional constraints, we obtain the logics ITL p of persistent posets and ITL ht of here-and-there temporal logic, both of which have been considered in the literature. We prove that ITL e has the effective finite model property and hence is decidable, while ITL p does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the “until” and “release” operators are not definable in terms of each other, even over the class of persistent posets.

Evidence logics model agents' belief revision process as they incorporate and aggregate information obtained from multiple sources. This information is captured using neighbourhood structures, where individual neighbourhoods represent pieces of evidence. In this paper we propose an extended framework which allows one to explicitly quantify either the number of evidence sets, or effort, needed to justify a given proposition, provide a complete deductive calculus and a proof of decidability, and show how existing frameworks can be embedded into ours.

We devote this article to the axiomatization/completeness of PRSPDL0 —a variant of iteration-free PDL with parallel composition. Our results are based on the following: although the program operation of parallel composition is not modally definable in the ordinary language of PDL , it becomes definable in a modal language strengthened by the introduction of propositional quantifiers. Instead of using axioms to define the program operation of parallel composition in the language of PDL enlarged with propositional quantifiers, we add an unorthodox rule of proof that makes the canonical model standard for the program operation of parallel composition and we use large programs for the proof of the Truth Lemma.

The core of this article is the modal correspondence theory in the class of all Euclidean frames. It shows that with respect to the class of all Euclidean frames, every modal formula is first-order definable and the problem of deciding the modal definability of sentences is undecidable.

The core of our article is the computability of the problem of deciding the modal definability of first-order sentences with respect to classes of frames. It gives a new proof of Chagrova's Theorem telling that, with respect to the class of all frames, the problem of deciding the modal definability of first-order sentences is undecidable. It also gives the proofs of new variants of Chagrova's Theorem.

This paper studies the concepts of definability and canonicity in Boolean logic with a binary relation. Firstly, it provides formulas defining first-order or second-order conditions on frames. Secondly, it proves that all formulas corresponding to compatible first-order conditions on frames are canonical.

We study a version of Propositional Dynamic Logic (PDL) that we call Dynamic Logic of Propositional Assignments (DL-PA). The atomic programs of DL-PA are assignments of propositional variables to true or to false. We show that DL-PA behaves better than PDL, having e.g. compactness and eliminability of the Kleene star. We establish tight complexity results: both satisfiability and model checking are EXPTIME-complete.

In a distributed environment, and more specially in service oriented architectures, the entities interacting one with another rely on credentials to decide whether an action they are told to perform is permitted. These credentials are exchanged within trust negotiation sessions during which the participating entities build up trust by communicating certificates to trusted peers. Dolev and Yao have introduced a notion of symbolic intruder to represent the capacities of a malicious agent trying to attack a cryptographically secured communication protocol. We present in this paper an adaptation of that intruder that retains the same deductive capabilities but is specialized for the analysis of the exchanges during a trust negotiation session. In particular this permits us to analyze the security of a distributed access control policy w.r.t. a malicious insider.

This paper proceeds to develop a model for representing and reasoning about time from the perspective of non-standard analysis.

This article considers the temporal logic defined over the class of all lexicographic products of dense linear orders without endpoints and gives its complete axiomatization for it.

Public announcement logic extends multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. In this article, we propose a labelled tableau calculus for this logic, and show that it decides satisfiability of formulas in deterministic polynomial space. Since this problem is known to be PSPACE-complete, it follows that our proof method is optimal.

We propose in this paper a framework in which the security policies of services in a distributed environment can be expressed. Services interact by exchanging credentials. Each service is made up of an access control policy protecting the access to the service, and of a trust negotiation policy controlling the accessibility of the credentials for other services. We add a workflow layer for each service to model its dynamic evolution with respect to the performed accesses. Unlike most of the access control policies which are uniquely based on roles, we choose an attribute based framework leading to more flexibility in the characterization of users. The strengths of this framework are its ability to control and check the access control aspect of the services and its dynamic evolution based on an exchange of credentials. We provide a unified framework for reasoning on access control policies, trust negotiation policies and workflows.

The development of deontic logic has opened new possibilities for the mathematical analysis of norms. This article tackles the description of large families of deontic systems that attempt to formalize such-and-such idea of juridical notions like obligation. It also introduces a modal logic based on actions for studying deontic reasoning within the context of a dynamic logic. © 2008 Wiley Periodicals, Inc.

Public announcement logic is an extension of multi-agent epistemic logic with dynamic operators to model the informational consequences of announcements to the entire group of agents. We propose an extension of public announcement logic with a dynamic modal operator that expresses what is true after any announcement: □φ expresses that φ is true after an arbitrary announcement ψ. As this includes the trivial announcement ⊤, one might as well say that □φ expresses what remains true after any announcement: it therefore corresponds to truth persistence after (definable) relativisation. The dual operation ⋄φ expresses that there is an announcement after which φ. This gives a perspective on Fitch's knowability issues: for which formulas φ does it hold that φ → ⋄Kφ? We give various semantic results, and we show completeness for a Hilbert-style axiomatisation of this logic.

International audience

International audience

Summary form only given. This paper describes a model for access control based on roles and permissions. Then it considers computational problems related to the verification of properties in protection systems defined from our model.

We present a variant of the access control matrix model obtained by incorporating uncertain surveillance saying that "if subject s performs illegally action a on object o then the degree of likelihood that remains unpunished is equal to x". We then turn to the question whether the expressive power of the matrix model grows when enriching access control with uncertain surveillance. In connection with this enriched model, we also discuss the solvable and unsolvable cases of the major theme of computer security, namely the safety problem for access control matrices.

In this paper, we further investigate the consistency problem for the qualitative temporal calculus INDU introduced by A. K. Pujari et al. (1999). We prove the intractability of the consistency problem for the subset of preconvex relations. On the other hand, we show the tractability of strongly preconvex relations. Furthermore, we also define another interesting set of relations for which the consistency problem can be decided by a method similar to the usual path-consistency method.

In this paper we define the notion of a block algebra, which is based upon a spatial application of Allen's interval algebra. In the p‐dimensional Euclidean space, where p ≥ 1, we consider only blocks whose sides are parallel to the axes of some orthogonal basis. The block algebra consists of a set of relations (the block relations) together with the fundamental operations of composition, converse and intersection. The 13p basic relations of this algebra constitute the exhaustive list of the relations possibly holding between two blocks. We are interested in the problem of testing the consistency of a set of spatial constraints between blocks, i.e. a block network. The consistency question for block networks is NP‐complete. We first extend the notions of convexity and preconvexity to the block algebra. Similarly to the interval algebra case, convexity leads to a tractable set whereas, contrary to the interval algebra case, preconvexity leads to an intractable set. Nevertheless we characterize a tractable subset of the preconvex relations: the strongly preconvex relations. Moreover we show that strong preconvexity and ORD‐Horn representability are the same.

Incidence geometry is based on two-sorted structures consisting of ‘points’ and ‘lines’ together with an intersort binary relation called incidence. We introduce an equivalent one-sorted geometrical structure, called incidence frame, which is suitable for modal considerations. Incidence frames constitute the semantical basis of MIG, the modal logic of incidence geometry. A completeness theorem for MIG is proved: a modal formula is a theorem of MIG if and only if it is valid in all incidence frames. Extensions to projective and affine geometries are also considered.

The purpose of a logic programming language is to handle symbols, clauses, goals and programs, and to say whether there are proofs of these goals or not in these programs. It differs from other programming languages in the sense that it is ‘logic in action’. Nevertheless, negation in logic programming—namely: the negation as failure rule and SLDNF-resolution—is very different from the logical classical negation. The negation as failure rule gives a false value to a predicate if the logic program considered cannot give a proof of that predicate. This practical view leads to the fact that negation in logic programming is an operator which tests the provability of the predicate under its scope. Thus negation as failure looks very much like a modal operator which would characterize some idea of provability. The purpose of this report is to define a declarative semantics for every logic program using the negation as failure rule. It shows that SLDNF-provability is a modal notion. It gives modal formulae which are proved to be sound and complete for this non-monotonic procedure and which explicitly express the implicit meaning of the negation and derivation symbols in logic programming.