Deontic logic as founded on nonmonotonic logic

Ever since its inception in the work of von Wright, deontic logic has been developed primarily as a species of modal logic. I argue in this paper, however, that the techniques of nonmonotonic logic may provide a better theoretical framework — at least for the formalization of commensense normative reasoning — than the usual modal treatment. After reviewing some standard approaches to deontic logic, I focus on two areas in which nonmonotonic techniques promise improved understanding: reasoning in the presence of conflicting obligations, and reasoning with conditional obligations.     

A Logical Analysis of the Relationship between Commitment and Obligation

In this paper, we analyze the relationship between commitment and obligation from a logical viewpoint. The principle of commitment implying obligation is proven in a specific logic of action preference which is a generalization of Meyer's dynamic deontic logic. In the proposed formalism, an agent's commitment to goals is considered as a special kind of action which can change one's deontic preference andone's obligation to take some action is based on the preference and the effects of the action. In this logic, it is shown that an agent has the obligation to take any action which is necessary for achieving as many committed goals as possible. The semantics of our logic is based on the possible world models for the dynamic logic of actions. A binary preference relation between possible worlds is associated with the model. Then the preference between actions are determined by comparing that of their consequences. According to the semantics, while the preference will influence the agent's choice of action, commitment is a kind of action that will change the agent's preference. Thus we can show how obligations arise from commitments via updating of deontic preference. The integrated semantics make it possible to express and reason about the mutual relationship among these mental attitudes in a common logic. This revised version was published online in August 2006 with corrections to the Cover Date.     

Top-down development of layered fault tolerant systems and its problems — a deontic perspective

Although the top-down development paradigm has successfully been applied to master the complexity of large systems, it has not yet been accepted as a useful paradigm for fault tolerant system design. This is mainly due to a problem that is sometimes referred to as the lazy programmers paradox. The lazy programmer paradox was already present and solved in top-down development methods for non-critical systems. However, the problem has re-appeared in an even more serious variant for critical systems. A few toy examples concerning exception handling in an Ada-like language are used to explain and illustrate the paradox. One possible solution to the problem is to use a specification language in which one can express that certain behaviours of a system are preferred over others. This paper proposes deontic logic as such a specification language. Therefore, a short and rather informal introduction to deontic logic is included. A non-trivial example is included to illustrate how deontic logic can be used to solve the lazy programmer paradox.Supported by NWO/SION Project 612-316-022: Fault Tolerance: Paradigms, Models, Logics, Construction.     

Constraint rule-based programming of norms for electronic institutions

Norms constitute a powerful coordination mechanism among heterogeneous agents. In this paper, we propose a rule language to specify and explicitly manage the normative positions of agents (permissions, prohibitions and obligations), with which distinct deontic notions and their relationships can be captured. Our rule-based formalism includes constraints for more expressiveness and precision and allows to supplement (and implement) electronic institutions with norms. We also show how some normative aspects are given computational interpretation.     

Contrary‐to‐duty reasoning with preference‐based dyadic obligations

In this paper we introduce Prohairetic Deontic Logic (PDL), a preference‐based dyadic deontic logic. In our preference‐based interpretation of obligations “α should be (done) if β is (done)” is true if (1) no ¬α ∧ β state is as preferable as an α ∧ β state and (2) the preferred β states are α states. We show that this representation solves different problems of deontic logic. The first part of the definition is used to formalize contrary‐to‐duty reasoning, which, for example, occurs in Chisholm’s and Forrester’s notorious deontic paradoxes. The second part is used to make deontic dilemmas inconsistent.     

Formal Verification of Websites

In this paper, a model for websites is presented. The model is well-suited for the formal verification of dynamic as well as static properties of the system. A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using a model-checking tool on the system. In this setting, we discuss some interesting properties which often need to be checked when designing websites. We have encoded the model using the specification language Maude which allows us to use the Maude model-checking tool.     

A Role Based Model for the Normative Specification of Organized Collective Agency and Agents Interaction

In this article we propose a role based model for the specification of organized collective agency, based on the legal concept of artificial person and on the normative perspective of organizational systems. We focus on the analysis of groups of agents (humans or not) that want to act collectively in a (more or less) permanent basis, and in a stable and organized way, as it is the typical case of organizations. We argue that in those cases such groups of agents should give rise to a new agent, that we call of institutionalized agent, with its own identity, whose structure is essentially defined through the characterization of a set of roles and whose behavior is determined by the acts of the agents that play such roles. We also present a deontic and action modal logic that captures the concept of acting in a role and relates it with the deontic notions of obligation, permission and prohibition. This logic is used in the formal specification of institutionalized agents and of societies of agents and in the rigorous analysis of them. We pay particular attention to the interaction between agents through contracts or other normative relations. A high level specification language is also suggested.     

Reasoning about action and change

Reasoning about change is a central issue in research on human and robot planning. We study an approach to reasoning about action and change in a dynamic logic setting and provide a solution to problems which are related to the Frame problem. Unlike most work on the frame problem the logic described in this paper is monotonic. It (implicitly) allows for the occurrence of actions of multiple agents by introducing non-stationary notions of waiting and test. The need to state a large number of frame axioms is alleviated by introducing a concept of chronological preservation to dynamic logic. As a side effect, this concept permits the encoding of temporal properties in a natural way. We compare the relative merits of our approach and non-monotonic approaches as regards different aspects of the frame problem. Technically, we show that the resulting extended systems of propositional dynamic logic preserve (weak) completeness, finite model property and decidability.     

A logical model of transfer of obligations in trade contracts

In this paper we present an outline of a formal framework for representing Deontic Deep Structure Models for business procedures and contracts. These models can be used in redesign of such procedures. In particular, to transform paper-based procedures into electronic procedures for electronic commerce. The framework is based on a combination of deontic logic and action logic. To illustrate its usefulness we illustrate how transferable obligations, i.e. obligations that can be transferred from one agent to another, can be analysed in this framework. In particular, we analyse the difference between transfer of agency and transfer of liability of an obligation.     

PMaude: Rewrite-based Specification Language for Probabilistic Object Systems

We introduce a rewrite-based specification language for modelling probabilistic concurrent and distributed systems. The language, based on PMaude, has both a rigorous formal basis and the characteristics of a high-level rule-based programming language. Furthermore, we provide tool support for performing discrete-event simulations of models written in PMaude, and for statistically analyzing various quantitative aspects of such models based on the samples that are generated through discrete-event simulation. Because distributed and concurrent communication protocols can be modelled using actors (concurrent objects with asynchronous message passing), we provide an actor PMaude module. The module aids writing specifications in a probabilistic actor formalism. This allows us to easily write specifications that are purely probabilistic – and not just non-deterministic. The absence of such (un-quantified) non-determinism in a probabilistic system is necessary for a form of statistical analysis that we also discuss. Specifically, we introduce a query language called Quantitative Temporal Expressions (or QuaTEx in short), to query various quantitative aspects of a probabilistic model. We also describe a statistical technique to evaluate QuaTEx expressions for a probabilistic model.     

Formalization of the Standard Uniform random variable

Continuous random variables are widely used to mathematically describe random phenomena in engineering and the physical sciences. In this paper, we present a higher-order logic formalization of the Standard Uniform random variable as the limit value of the sequence of its discrete approximations. We then show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover, summarizing the proof steps. The formalized Standard Uniform random variable can be transformed to formalize other continuous random variables, such as Uniform, Exponential, Normal, etc., by using various non-uniform random number generation techniques. The formalization of these continuous random variables will enable us to perform an error free probabilistic analysis of systems within the framework of a higher-order-logic (HOL) theorem prover. For illustration purposes, we present the formalization of the Continuous Uniform random variable based on the formalized Standard Uniform random variable, and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.     

Verifying conformance of multi-agent commitment-based protocols

Although several approaches have been proposed to specify multi-agent commitment-based protocols that capture flexible and rich interactions among autonomous and heterogeneous agents, very few of them synthesize their formal specification and automatic verification in an integrated framework. In this paper, we present a new logic-based language to specify commitment-based protocols, which is derived from ACTL^1c, a logic extending CTL¹ with modalities to represent and reason about social commitments and their actions. We present a reduction technique that formally transforms the problem of model checking ACTL^1c to the problem of model checking GCTL¹ (an extension of CTL¹ with action formulae). We prove that the reduction technique is sound and we fully implement it on top of the CWB-NC model checker to automatically verify the NetBill protocol, a motivated and specified example in the proposed specification language. We also apply the proposed technique to check the compliance of another protocol: the Contract Net protocol with given properties and report and discuss the obtained results. We finally develop a new symbolic algorithm to perform model checking dedicated to the proposed logic.     

Specification of contractual obligations in formal business communication

Formal business communication is a process-oriented (vs. document-oriented) environment for digital interoorganizational business transactions. They improve efficiency and effectiveness of business communications and often provide strategic advantages. Thanks to the current advances in information and telecommunications technologies, the development of formal business communication systems plays one of the key roles in the establishment of digital commerce, or virtual organizational business transaction platform. This paper proposes a logic of relativized deontic modalities as a component of digital commerce systems. The logic of relativized deontic modalities provides syntactic and semantic treatment for such notions of duty in the context of formal business communications. Also addressed are the practical issue of conflicts of duties and their resolution based on defeasibility reasoning, and the dynamic aspect of contractual obligations including delegation of duties and assignment of rights. Finally, we suggest augmentation of the CASE/Open-EDI system with the proposed logic of contractual obligations.     

A deontic approach to database integrity

The logical theory of database integrity is developed as an application of deontic logic. After a brief introduction to database theory and Kripke semantics, a deontic operator X, denoting what should hold, non-trivially, given a set of constraints, is defined and axiomatized. The theory is applied to updates, to dynamic constraints and to databases extended with nulls.     

Focusing qualitative simulation using temporal logic: theoretical foundations

We illustrate TeQsim, a qualitative simulator for continuous dynamical systems that combines the expressive power of qualitative differential equations with temporal logic to constrain and refine the resulting predicted behaviors. Temporal logic is used to specify constraints that restrict the simulation to a region of the state space and to specify trajectories for input variables. A propositional linear‐time temporal logic is adopted, which is extended to a three valued logic that allows a formula to be conditionally entailed when quantitative information specified in the formula can be applied to a behavior to refine it. We present a formalization of the logic with correctness and completeness results for the adopted model checking algorithm. We show an example of the simulation of a non‐autonomous dynamical system and illustrate possible application tasks, ranging from simulation to monitoring and control of continuous dynamical systems, where TeQsim can be applied. This revised version was published online in June 2006 with corrections to the Cover Date.     

Towards specifying norms

A normative statement (or norm) is one whichshould hold orusually holds, as opposed to ordinary statements whichactually oralways hold. The need for normative statements in computer science specifications is described, and different kinds of norms that can occur in an action-based system are classified. A language and logic for expressing such norms is described, We show that it allows the specifier to reason about the system's behaviour even when it fails to satisfy the norms. The logic used is based on Modal Action Logic [6,4,7,11], and has two additions for expressing norms. The first of these additions is the use ofdeontic axioms. The second is the use of an ordering between axioms of a specification to stipulate priorities. Such orderings of axioms are calledordered theory presentations. We show that they arise naturally fromstructured specifications.The author acknowledges support of the British Science and Engineering Research Council on theForest project.