Modeling control objectives for business process compliance

Business process design is primarily driven by process improvement objectives. However, the role of control objectives stemming from regulations and standards is becoming increasingly important for businesses in light of recent events that led to some of the largest scandals in corporate history. As organizations strive to meet compliance agendas, there is an evident need to provide systematic approaches that assist in the understanding of the interplay between (often conflicting) business and control objectives during business process design. In this paper, our objective is twofold. We will firstly present a research agenda in the space of business process compliance, identifying major technical and organizational challenges. We then tackle a part of the overall problem space, which deals with the effective modeling of control objectives and subsequently their propagation onto business process models. Control objective modeling is proposed through a specialized modal logic based on normative systems theory, and the visualization of control objectives on business process models is achieved procedurally. The proposed approach is demonstrated in the context of a purchase-to-pay scenario.

Modelling and verifying smell-free architectures with the Archery language

Architectural (bad) smells are design decisions found in software architectures that degrade the ability of systems to evolve. This paper presents an approach to verify that a software architecture is smellfree using the Archery architectural description language. The language provides a core for modelling software architectures and an extension for specifying constraints. The approach consists in precisely specifying architectural smells as constraints, and then verifying that software architectures do not satisfy any of them. The constraint language is based on a propositional modal logic with recursion that includes: a converse operator for relations among architectural concepts, graded modalities for describing the cardinality in such relations, and nominals referencing architectural elements. Four architectural smells illustrate the approach.

On the verification of architectural reconfigurations

In a reconfigurable system, the response to contextual or internal change may trigger reconfiguration events which, on their turn, activate scripts that change the system׳s architecture at runtime. To be safe, however, such reconfigurations are expected to obey the fundamental principles originally specified by its architect. This paper introduces an approach to ensure that such principles are observed along reconfigurations by verifying them against concrete specifications in a suitable logic. Architectures, reconfiguration scripts, and principles are specified in Archery, an architectural description language with formal semantics. Principles are encoded as constraints, which become formulas of a two-layer graded hybrid logic, where the upper layer restricts reconfigurations, and the lower layer constrains the resulting configurations. Constraints are verified by translating them into logic formulas, which are interpreted over models derived from Archery specifications of architectures and reconfigurations. Suitable notions of bisimulation and refinement, to which the architect may resort to compare configurations, are given, and their relationship with modal validity is discussed.

La logique déontique : une application de la logique à l'éthique et au discours juridique

Cet ouvrage a été rédigé en LaTeX, ce qui permet d'atteindre directement certaines sections, notes ou références bibliographiques par le biais des hyperliens.

Analyse de la structure logique des inférences légales et modélisation du discours juridique

Thèse par articles.

Lógica, lenguaje y significado. Lógica intensional y gramática lógica

Este texto representa el esfuerzo combinado de dos lógicos, dos filósofos y un lingüista. Esta empresa fue inspirada por la convicción de los autores de que la lógica y el lenguaje son inseparables, en particular en lo que respecta al análisis del significado. Una región interdisciplinaria emerge entre los límites de la filosofía, la lógica y la lingüística. Lógica, lenguaje y significado: lógica intensional y gramática lógica es una introducción a este campo, el cual aplica los sistemas lógico-formales al estudio del significado del lenguaje natural. El libro comienza con una introducción de los distintos principios de la semántica intensional y luego presenta varias lógicas intensionales, tales como la lógica proposicional modal, la lógica de predicados modal y la lógica temporal. También introduce la teoría de tipos, la lambda-abstracción y la sintaxis categorial.

A pattern language for goals

Previous work has established the value of goal-oriented approaches to requirements engineering. Achieving clarity and agreement about stakeholders’ goals and assumptions is critical for building successful software systems and managing their subsequent evolution. In general, this decision-making process requires stakeholders to understand the implications of decisions outside the domains of their own expertise. Hence it is important to support goal negotiation and decision making with description languages that are both precise and expressive, yet easy to grasp. This paper presents work in progress to develop a pattern language for describing goal refinement graphs. The language has a simple graphical notation, which is supported by a prototype editor tool, and a symbolic notation based on modal logic.

Lógica BDI fuzzy

Intendding to understand how the human mind operates, some philosophers and psycologists began to study about rationality. Theories were built from those studies and nowadays that interest have been extended to many other areas such as computing engineering and computing science, but with a minimal distinction at its goal: to understand the mind operational proccess and apply it on agents modelling to become possible the implementation (of softwares or hardwares) with the agent-oriented paradigm where agents are able to deliberate their own plans of actions. In computing science, the sub-area of multiagents systems has progressed using several works concerning artificial intelligence, computational logic, distributed systems, games theory and even philosophy and psycology. This present work hopes to show how it can be get a logical formalisation extention of a rational agents architecture model called BDI (based in a philosophic Bratman s Theory) in which agents are capable to deliberate actions from its beliefs, desires and intentions. The formalisation of this model is called BDI logic and it is a modal logic (in general it is a branching time logic) with three access relations: B, D and I. And here, it will show two possible extentions that tranform BDI logic in a modal-fuzzy logic where the formulae and the access relations can be evaluated by values from the interval [0,1]

An alternative approach for quasi-truth

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Reino da natureza, reino dos fins, e proto-reino: um estudo de traduções conservativas

We provide conservative translations from propositional modal logic KT (the simplest normal alethic logic) into propositional modal logic KD (the simplest normal deontic logic), and from this into the propositional modal logic K (the simplest normal logic simpliciter). Following an idea discussed by Jaakko Hintikka, these conservative translations are based on the third formulation of Kantian categorical imperative, the formulation of the Kingdom of Ends.

A syntactic realization theorem for justification logics

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms \$mathsfd\$, \$mathsft\$, \$mathsfb\$, \$mathsf4\$, and \$mathsf5\$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting's realization merging technique. We further strengthen the realization theorem for \$mathsfKB5\$ and \$mathsfS5\$ by showing that the positive introspection operator is superfluous.