No description available.

A disjunction is an expression using ‘or’, such as ‘Anne has a Ford or a Tesla’. From such a statement, we cannot usually infer either disjunct, for example, that ‘Anne has a Ford’. However, in choice situations like ‘You may have coffee or tea’ we can infer either option. The problem of free choice disjunction is to determine why these choice inferences are legitimate (von Wright 1968, Kamp 1973, Meyer 2016). Central to this discussion is the observation that a modal possibility operator ranging over a disjunction sometimes implies a conjunction of possibilities. In the case of permission, we express this as the choice principle ‘May (P or Q)’ entails ‘May P and May Q’ (Zimmerman 2000). Unfortunately, this inference cannot hold in a logical language without significant modification of the systems involved. I explore the history of proposed solutions to this problem, including semantic solutions that assign a distinctive meaning to free choice disjunctions and pragmatic solutions that use features of their utterance to solve the problem. I draw connections between semantics and pragmatics and, using the tools of dynamic logic (Baltag et al. 1998, van Benthem 2010), I present a formal account of one major (Gricean) approach to the problem (Kratzer & Shimoyama 2002). Ultimately, I explore the role of logic in this debate and argue that we should formally represent the meaning of these expressions directly as conjunctions of possibilities. Thus, rather than trying to account for the choice principle within a logical system, we must instead account for the fact that, in choice situations, the meaning of ‘May (P or Q)’ translates into logical formalism as (May P & May Q). / Thesis / Doctor of Philosophy (PhD) / A disjunction is a statement using ‘or’, like ‘Anne has a Ford or a Tesla’. From such a statement, we cannot infer either disjunct—e.g. ‘Anne has a Ford’. In choice situations like ‘You may have coffee or tea’ we can infer either option. Why this choice inference is legitimate is the problem of free choice disjunction. I explore the history of solutions to the problem, including semantic solutions that propose a special meaning to choice disjunctions and pragmatic solutions that appeal to the circumstances in which they are uttered. I draw connections between semantics and pragmatics and present a formal account of one major pragmatic approach to the problem. Where others have sought to explain how 'May(P or Q)' entails 'May P and May Q', I argue instead that the meaning of ‘May (P or Q)’ in choice scenarios translates directly into logical formalism as ‘May P & May Q’.

The everything as a service concept enables dynamic resource provisions to be seen and delivered as services. Their proliferation nowadays leads to the creation of new value-added services composed of several sub-services in a pre-specified manner, known as service workflows. The use of service workflow appears in various domains, ranging from the basic interactions found in several e-commerce and several online interactions to the complex ones such as Virtual Organizations, Grids, and Cloud Computing. However, the dynamic nature in open environments makes a workflow constantly changing, to be adaptable to the change of new circumstances. How to determine suitable services has becomes a very important challenge. Requirements from both workflow owners and service providers play a significant role in the process of service acquisition, composition, and interoperations. From the workflow owner viewpoint, requirements can specify properties of services to be acquired for tasks in a workflow. On the other hand, requirements from service providers affect trust-based decision in workflow participation. The lack of formal languages to specify these requirements poses difficulties in the success of service collaborations in a workflow. It impedes: (1) workflow scalability that tends to be limited within a certain set of trusted domains; (2) dynamicity when each service acts in an autonomous and unpredictable manner where any change might affect existing requirements; and (3) inconsistency in dealing with the disparate representations of requirements, causing high overhead for compliance checking. This thesis focuses on developing a framework to overcome, or at least alleviate, these problems. It situates in inter-disciplinary areas including logics, workflow modelling, specification languages, trust management, decision support system, and compliance checking. Two core elements are proposed: (1) a formal logic-based requirement specification language, namely Trust Specification (TS), such that the requirements can be formally and uniformly expressed; and (2) compliance checking algorithms to automatically check for the compliance of requirements in service workflows. It is worth noting that this thesis contains some proofs of logic extension, workflow modelling, specification language, and compliance checking algorithms. These might raise a concern to people focusing deep on one particular area such as logics, or workflow modelling who might overlook the essence of the work, for example (1) the application of a formal specification language to the exclusive characteristics of service workflows, and (2) bridging the gap of the high level languages such as trust management down to the lower logic-based ones. The first contribution of the framework is to allow requirements to be independently and consistently expressed by each party where the workflow participation decision and acquisition are subject to the compliance of requirements. To increase scalability in large-scale interoperations, the second contribution centres on automatic compliance checking where TS language and compliance checking algorithms are two key components. The last contribution focuses on dynamicity. The framework allows each party to modify existing requirements and the compliance checking would be automatically activated to check for further compliance. As a result, it is anticipated that the solution will encourage the proliferation of service provisions and consumption over the Internet.

A glass couldn't contain water unless it contained H2O-molecules. Likewise, a man couldn't be a bachelor unless he was unmarried. Now, the latter is what we would call a conceptual or analytical truth. It's also what we would call a priori. But it's hardly a conceptual or analytical truth that if a glass contains water, then it contains H2O-molecules. Neither is it a priori. The fact that water is composed of H2O-molecules was an empirical discovery made in the eighteenth century. The fact that all bachelors are unmarried was not. But neither is a logical truth, so how do we explain the difference? Two-dimensional semantics is a framework that promises to shed light on these issues. The main purpose of this thesis is to understand and evaluate this framework in relation to various alternatives, to see whether some version of it can be defended. I argue that it fares better than the alternatives. However, much criticism of two-dimensionalism has focused on its alleged inability to provide a proper semantics for certain epistemic operators, in particular the belief operator and the a priori operator. In response to this criticism, a two-dimensional semantics for belief ascriptions is developed using structured propositions. In connection with this, a number of other issues in the semantics of belief ascriptions are addressed, concerning indexicals, beliefs de se, beliefs de re, and the problem of logical omniscience.

The verification of real-time systems has gained much interest in the formal verification community during the past two decades. In this thesis, we investigate two real-time verification problems that benefit from the techniques normally used in untimed verification. The first part of this thesis is concerned with the monitoring of real-time specifications. We study the expressiveness of metric temporal logics over timed words, a problem that dates back to early 1990s. We show that the logic obtained by extending Metric Temporal Logic (MTL) with two families of new modalities is expressively complete for the Monadic First-Order Logic of Order and Metric (FO[<,+1]) in time-bounded settings. Furthermore, by allowing rational constants, expressive completeness also holds in the general (time-unbounded) setting. Finally, we incorporate several notions and techniques from LTL monitoring to obtain the first trace-length independent monitoring procedure for this logic. The second part of this thesis concerns a decision problem regarding UAVs: given a set of targets (each ascribed with a relative deadline) and flight times between each pair of targets, is there a way to coordinate a flock of k identical UAVs so that all targets are visited infinitely often and no target is ever left unvisited for a time longer than its relative deadline? We show that the problem is PSPACE-complete even in the single-UAV case, thereby corrects an erroneous claim from the literature. We then complement this result by proposing an efficient antichain-based approach where a delayed simulation is used to prune the state space. Experimental results clearly demonstrate the effectiveness of our approach.

Les comportement épistémiques, mobiles et spatiaux sont omniprésent dans les systèmes distribués aujourd’hui. La nature intrinsèque épistémique de ces types de systèmes provient des interactions des éleménts qui en font parties. La plupart des gens sont familiarisés avec des systèmes numériques où les utilisateurs peuvent partager ses croyances, opinions et même des mensonges intentionnels (des canulars). Aussi, les modèles de ces systèmes doivent tenir compte des interactions avec d’autres de même que leur nature distribués. Ces comportements spatiaux et mobiles font part d’applications où les données se déplacent dans des espaces (peut-être imbriqués) qui sont définis par, par exemple, cercles d’amis, des groupes, ou des dossiers partagés. Nous pensons donc qu’une solide compréhension des notion d’espaces, de mobilité spatial ainsi que le flux d’information épistémique est cruciale dans la plupart des modèles de systèmes distribués de nos jours.Les systèmes de contrainte (sc) fournissent les domaines et les opérations de base pour les fondements sémantiques de la famille de modèles déclaratifs formels de la théorie de la concurrence connu sous le nom de programmation concurrent par contraintes (pcc). Les systèmes des contraintes spatiales (scs) représentent des structures algébriques qui étendent sc pour raisonner sur les comportement spatiaux et épistémiques de base tel que croyance et l’extrusion. Les assertions spatiales et épistémiques peuvent être vues comme des modalités spécifiques. D’autres modalités peuvent être utilisées pour les assertions concernant le temps, les connaissances et même pour l’analyse des groupes entre autres concepts utilisés dans la spécification et la vérification des systèmes concurrents.Dans cette thèse nous étudions l’expressivité des systèmes de contraintes spatiales dans la perspective générale du comportement modal et épistémique. Nous montrerons que les systèmes de contraintes spatiales sont assez robustes pour capturer des modalités inverses et pour obtenir de nouveaux résultats pour les logiques modales. Également, nous montrerons que nous pouvons utiliser les scs pour exprimer un comportement épistémique fondamental comme connaissance. Finalement, nous donnerons une caractérisation algébrique de la notion de l’information distribuée au moyen de constructions sur scs. / Epistemic, mobile and spatial behaviour are common place in today’s distributed systems. The intrinsic epistemic nature of these systems arises from the interactions of the elements taking part of them. Most people are familiar with digital systems where users share their beliefs, opinions and even intentional lies (hoaxes). Models of those systems must take into account the interactions with others as well as the distributed quality these systems present. Spatial and mobile behaviour are exhibited by applications and data moving across (possibly nested) spaces defined by, for example, friend circles, groups, and shared folders. We therefore believe that a solid understanding of the notion of space and spatial mobility as well as the flow of epistemic information is relevant in many models of today’s distributed systems.Constraint systems (cs’s) provide the basic domains and opera- tions for the semantic foundations of the family of formal declarative models from concurrency theory known as concurrent constraint programming (ccp). Spatial constraint systems (scs’s) are algebraic structures that extend cs’s for reasoning about basic spatial and epistemic behaviour such as belief and extrusion. Both spatial and epistemic assertions can be viewed as specific modalities. Other modalities can be used for assertions about time, knowledge and even the analysis of groups among other concepts used in the specification and verification of concurrent systems.In this thesis we study the expressiveness of spatial constraint systems in the broader perspective of modal and epistemic behaviour. We shall show that spatial constraint systems are sufficiently robust to capture inverse modalities and to derive new results for modal logics. We shall show that we can use scs’s to express a fundamental epistemic behaviour such as knowledge. Finally we shall give an algebraic characterization of the notion of distributed information by means of constructors over scs’s.

In this thesis we extend BDI logics, which are normal multimodal logics with an arbitrary set of normal modal operators, from three different perspectives. Firstly, based on some recent developments in modal logic, we examine BDI logics from a combining logic perspective and apply combination techniques like fibring/dovetailing for explaining them. The second perspective is to extend the underlying logics so as to include action constructs in an explicit way based on some recent action-related theories. The third perspective is to adopt a non-monotonic logic like defeasible logic to reason about intentions in BDI. As such, the research captured in this thesis is theoretical in nature and situated at the crossroads of various disciplines relevant to Artificial Intelligence (AI). More specifically this thesis makes the following contributions: 1. Combining BDI Logics through fibring/dovetailing: BDI systems modeling rational agents have a combined system of logics of belief, time and intention which in turn are basically combinations of well understood modal logics. The idea behind combining logics is to develop general techniques that allow to produce combinations of existing and well understood logics. To this end we adopt Gabbay's fibring/dovetailing technique to provide a general framework for the combinations of BDI logics. We show that the existing BDI framework is a dovetailed system. Further we give conditions on the fibring function to accommodate interaction axioms of the type G [superscript k,l,m,n] ([diamond][superscript k] [superscript l] [phi] [implies] [superscript m] [diamond][superscript n] [phi]) based on Catach's multimodal semantics. This is a major result when compared with other combining techniques like fusion which fails to accommodate axioms of the above type. 2. Extending the BDI framework to accommodate Composite Actions: Taking motivation from a recent work on BDI theory, we incorporate the notion of composite actions, [pi]-1; [pi]-2 (interpreted as [pi]-1 followed by [pi]-2), to the existing BDI framework. To this end we introduce two new constructs Result and Opportunity which helps in reasoning about the actual execution of such actions. We give a set of axioms that can accommodate the new constructs and analyse the set of commitment axioms as given in the original work in the background of the new framework. 3. Intention reasoning as Defeasible reasoning: We argue for a non-monotonic logic of intention in BDI as opposed to the usual normal modal logic one. Our argument is based on Bratman's policy-based intention. We show that policy-based intention has a defeasible/non-monotonic nature and hence the traditional normal modal logic approach to reason about such intentions fails. We give a formalisation of policy-based intention in the background of defeasible logic. The problem of logical omniscience which usually accompanies normal modal logics is avoided to a great extend through such an approach.

Le concept de confiance est un concept sociocognitif qui adresse la question de l'interaction dans les systèmes concurrents. Quand la complexité d'un système informatique prohibe l'utilisation de solutions traditionnelles de sécurité informatique en amont du processus de développement (solutions dites de type dur), la confiance est un concept candidat, pour le développement de systèmes d'aide à l'interaction. Dans cette thèse, notre but majeur est de présenter une vue d'ensemble de la discipline de la modélisation de la confiance dans les systèmes informatiques, et de proposer quelques modèles logiques pour le développement de module de confiance. Nous adoptons comme contexte applicatif majeur, les applications basées sur les architectures orientées services, qui sont utilisées pour modéliser des systèmes ouverts telle que les applications web. Nous utiliserons pour cela une abstraction qui modélisera ce genre de systèmes comme des systèmes multi-agents. Notre travail est divisé en trois parties, la première propose une étude de la discipline, nous y présentons les pratiques utilisées par les chercheurs et les praticiens de la confiance pour modéliser et utiliser ce concept dans différents systèmes, cette analyse nous permet de définir un certain nombre de points critiques, que la discipline doit aborder pour se développer. La deuxième partie de notre travail présente notre premier modèle de confiance. Cette première solution basée sur un formalisme logique (logique dynamique épistémique), démarre d'une interprétation de la confiance comme une croyance sociocognitive, ce modèle présentera une première modélisation de la confiance. Apres avoir prouvé la décidabilité de notre formalisme. Nous proposons une méthodologie pour inférer la confiance en des actions complexes : à partir de notre confiance dans des actions atomiques, nous illustrons ensuite comment notre solution peut être mise en pratique dans un cas d'utilisation basée sur la combinaison de service dans les architectures orientées services. La dernière partie de notre travail consiste en un modèle de confiance, où cette notion sera perçue comme une spécialisation du raisonnement causal tel qu'implémenté dans le formalisme des règles de production. Après avoir adapté ce formalisme au cas épistémique, nous décrivons trois modèles basés sur l'idée d'associer la confiance au raisonnement non monotone. Ces trois modèles permettent respectivement d'étudier comment la confiance est générée, comment elle-même génère les croyances d'un agent et finalement, sa relation avec son contexte d'utilisation. / The concept of trust is a socio-cognitive concept that plays an important role in representing interactions within concurrent systems. When the complexity of a computational system and its unpredictability makes standard security solutions (commonly called hard security solutions) inapplicable, computational trust is one of the most useful concepts to design protocols of interaction. In this work, our main objective is to present a prospective survey of the field of study of computational trust. We will also present two trust models, based on logical formalisms, and show how they can be studied and used. While trying to stay general in our study, we use service-oriented architecture paradigm as a context of study when examples are needed. Our work is subdivided into three chapters. The first chapter presents a general view of the computational trust studies. Our approach is to present trust studies in three main steps. Introducing trust theories as first attempts to grasp notions linked to the concept of trust, fields of application, that explicit the uses that are traditionally associated to computational trust, and finally trust models, as an instantiation of a trust theory, w.r.t. some formal framework. Our survey ends with a set of issues that we deem important to deal with in priority in order to help the advancement of the field. The next two chapters present two models of trust. Our first model is an instantiation of Castelfranchi & Falcone's socio-cognitive trust theory. Our model is implemented using a Dynamic Epistemic Logic that we propose. The main originality of our solution is the fact that our trust definition extends the original model to complex action (programs, composed services, etc.) and the use of authored assignment as a special kind of atomic actions. The use of our model is then illustrated in a case study related to service-oriented architecture. Our second model extends our socio-cognitive definition to an abductive framework that allows us to associate trust to explanations. Our framework is an adaptation of Bochman's production relations to the epistemic case. Since Bochman approach was initially proposed to study causality, our definition of trust in this second model presents trust as a special case of causal reasoning, applied to a social context. We end our manuscript with a conclusion that presents how we would like to extend our work.

abstract: Reasoning about actions forms the basis of many tasks such as prediction, planning, and diagnosis in a dynamic domain. Within the reasoning about actions community, a broad class of languages, called action languages, has been developed together with a methodology for their use in representing and reasoning about dynamic domains. With a few notable exceptions, the focus of these efforts has largely centered around single-agent systems. Agents rarely operate in a vacuum however, and almost in parallel, substantial work has been done within the dynamic epistemic logic community towards understanding how the actions of an agent may effect not just his own knowledge and/or beliefs, but those of his fellow agents as well. What is less understood by both communities is how to represent and reason about both the direct and indirect effects of both ontic and epistemic actions within a multi-agent setting. This dissertation presents ongoing research towards a framework for representing and reasoning about dynamic multi-agent domains involving both classes of actions. The contributions of this work are as follows: the formulation of a precise mathematical model of a dynamic multi-agent domain based on the notion of a transition diagram; the development of the multi-agent action languages mA+ and mAL based upon this model, as well as preliminary investigations of their properties and implementations via logic programming under the answer set semantics; precise formulations of the temporal projection, and planning problems within a multi-agent context; and an investigation of the application of the proposed approach to the representation of, and reasoning about, scenarios involving the modalities of knowledge and belief. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2018

Model generation and minimal model generation are useful for tasks such as model checking, query answering and for debugging of logical specifications. Due to this variety of applications, several minimality criteria and model generation methods for classical logics have been studied. Minimal model generation for modal logics how ever did not receive the same attention from the research community. This thesis aims to fill this gap by investigating minimality criteria and designing minimal model generation procedures for all the sublogics of the multi-modal logic S5(m) and their extensions with universal modalities. All the procedures are minimal model sound and complete, in the sense that they generate all and only minimal models. The starting point of the investigation is the definition of a Herbrand semantics for modal logics on which a syntactic minimality criterion is devised. The syntactic nature of the minimality criterion allows for an efficient minimal model generation procedure, but, on the other hand, the resulting minimal models can be redundant or semantically non minimal with respect to each other. To overcome the syntactic limitations of the first minimality criterion, the thesis moves from minimal modal Herbrand models to semantic minimality criteria based on subset-simulation. At first, theoretical procedures for the generation of models minimal modulo subset-simulation are presented. These procedures for the generation of models minimal modulo subset-simulation are minimal model sound and complete, but they might not terminate. The minimality criterion and the procedures are then refined in such a way that termination can be ensured while preserving minimal model soundness and completeness.