Automated support to enterprize modeling has increasingly become a subject of interest for organizations seeking solutions for storage, distribution and analysis of knowledge about business processes. This interest has recently resulted in approving the standard for specifying Semantics of Business Vocabulary and Business Rules (SBVR). Despite the existence of formally grounded notations, up to now SBVR still lacks a sound and consistent logical formalization which would allow developing automated solutions able to check the consistency of a set of business rules. This work reports on the attempt to provide logical foundations for SBVR by the means of de ning a speci c rst-order deonticalethic logic (FODAL). The connections of FODAL with the modal logic QK and the description logic ALCQI have been investigated and, on top of the obtained theoretical results, a special tool providing automated support for consistency checks of a set of ALCQI-expressible deontic and alethic business rules has been implemented.
Automated support to enterprize modeling has increasingly become a subject of
interest for organizations seeking solutions for storage, distribution and analysis
of knowledge about business processes. One of the most common approaches for
describing business and the information used by that business is the rule-based
approach [
Several attempts have been made so far in order to provide a logical
formalization for structural and operational rules in SBVR and its notations. The most
signi cant related work includes several formalizations of the purely structural
fragment of ORM2, including translation to rst-order predicate logic (FOL)
[
In this paper we de ne a multimodal rst-order deontic-alethic logic (FODAL) with sound and complete axiomatization that captures the desired semantics of and interaction between business rules. We then report on the logical properties of such formalization and its connections with the modal logic QK and the description logic ALCQI. Finally we present the tool which provides automated support for consistency checks of a set of ALCQI-expressible deontic and alethic ORM2 constraints. Additionally, it implements the translation of aforementioned class of ORM2 constraints into an OWL2 ontology.
The rest of the paper is organized as follows. In the second section an overview of the SBVR standard and its ORM2 notation is given. Third section describes the proposed logical formalization in terms of rst-order deontic-alethic logic (FODAL) along with its syntax, semantics and complete and sound axiomatization. Next two paragraphs are devoted to modeling SBVR rules with FODAL and checking their consistency with the help of this logic, while in the sixth section a connection with standard modal logic is introduced. Finally, the last paragraph describes the tool developed to provide automated support for consistency checks together with translation to OWL2. 2
A core idea of business rules formally supported by SBVR is the following [
Noun and verb concepts. According to the SBVR 1.0 speci cation [
A verb concept (or fact type) represents the notion of relations and is de ned as \a concept that is the meaning of a verb phrase". A fact type can have one (characteristic), two (binary ) or more fact type roles.
Business rules. The main types of rules de ned in SBVR standard are
structural business rules and operative business rules (See Figure 1). Structural
(de nitional ) rules specify what the organization takes things to be, how do the
members of the community agree on the understanding of the domain [
Conceptual model. An SBVR conceptual model CM = hS; F i is a structure intended to describe a business domain, where S is a conceptual schema, declaring fact types and rules relevant to the business domain, and F is a population of facts that conform to this schema. Business rules de ned in the conceptual schema S can be considered as high-level facts (i.e., facts about propositions) and play a role of constraints, which are used to impose restrictions concerning fact populations.
The SBVR standard provides means for formally expressing business facts
and business rules in terms of fact types of pre-de ned schema and certain logical
operators, quanti ers, etc. These formal statements of rules may be transformed
into logical formulations, which can in turn be used for exchange with other
rules-based software tools. Such logical rule formulations are equivalent to
formulae in 2-valued rst-order predicate calculus with identity [
In order to express the structural or operational nature of a business rule, the corresponding rule formulation uses any of the basic alethic or deontic modalities. Structural rule formulations use alethic operators: = it is necessary that and = it is possible that ; while operative rule formulations use deontic modal operators O = it is obligatory that, P = it is permitted that, as well as F = it is forbidden that.
Notations for business vocabulary and rules. There are several
common means of expressing facts and business rules in SBVR, namely through
statements, diagrams or any combination of those, each serving best for
different purposes ([
One of the most promising notations for SBVR is Object-Role Modeling
(ORM2), which is a conceptual modeling approach combining both formal,
textual speci cation language and formal graphical modeling language [
r = Each visitor has at most one passport.
An example illustrating ORM2 graphical notation is introduced on Figure 2.
The advantage of ORM2 over other notations is that it is a formal language
per se, featuring rich expressive power, intelligibility, and semantic stability [
Aforementioned existing translations to standard logics may be seen as attempts to provide a logical formalization for structural and operational rules. However, since they consider only the purely structural fragment of ORM2, they are not capable of providing consistency checks for a combined set of possibly interacting alethic and deontic business rules. 1 Since the nature of business rules implies the absence of uncertainty, it means that the resulting rst-order formulae will not contain free variables, i.e. will be closed formulae. Then an SBVR rule may be represented by an expression resulted from application of modalities and boolean connectives to a set of closed FOL formulae r^i .
In this section we describe our attempt to provide logical foundations for SBVR
by the means of de ning a speci c multi-modal logic. The basic formalisms we
use to model business rule formulations are standard deontic logic (SDL) and
normal modal logic S4, which are both propositional modal logics. We then
construct a rst-order deontic-alethic logic (FODAL) { a multimodal logic, as a
rst-order extension of a combination of SDL and S4 to be able to express
business constraints de ned in SBVR. In order to construct the rst-order extension
for the combined logic we follow the procedure described in [
The alphabet of FODAL contains the following symbols: { a set of propositional connectives : :; ^. { a universal quanti er: 8 (for all ). { an in nite set P = fP11; P 1; :::; P 2; P22; :::; P1n; P2n; :::g of n-place relation sym2 1 bols (also referred to as predicate symbols ). { an in nite set V = fv1; v2; :::g of variable symbols.
{ modal operators: alethic { (necessity ) and deontic { O (obligation). FODAL formulae. The formulae of FODAL are de ned inductively in the following way: { Every atomic formula is a formula. { If X is a formula, so is :X. { If X and Y are formulae, then X ^ Y is a formula. { If X is a formula, then so are X and OX.
{ If X is a formula and v is a variable, then 8vX is a formula.
The existential quanti er (9) as well as other propositional connectives (_; !; $) are de ned as usual, while additional modal operators ( ; P ; F ) are de ned in the following way: : :
P :O:
F
O: (1) A FODAL formula with no free variable occurrences is called a closed formula or a sentence. A modal sentence is a sentence whose main logical operator is a modal operator. An atomic modal sentence is a modal sentence which contains one and the only modal operator. 3.2
Since SBVR itself interprets constraints in the context of possible worlds which correspond to states of the fact model (i.e. di erent fact populations), the choice of varying domain Kripke semantics is intuitively justi ed. Also, since SBVR rule formulations may includes two types of modalities: deontic and alethic, - we utilize the notion of two-layer Kripke frames with accessibility relations RO and R respectively.
Augmented frame. A varying domain augmented bimodal frame is a relational structure Fvar = hW; RO; R ; Di, where hW; RO; R i is a two-layer Kripke frame, W is a non-empty set of worlds, R( ) are binary relations on W and D is a domain function mapping worlds of W to non-empty sets. A domain of a possible world w is then denoted as D(w) and a frame domain is de ned as D(F) = SfD(wi)jwi 2 Wg.
In order to correctly capture the behavior and interaction of the alethic and
deontic modal operators it is necessary to constrain the corresponding
accessibility relations: the alethic accessibility is usually taken to be a re exive and
transitive relation (S4) [
Moreover, since one of the objectives of the formalization under development is to de ne the consistency of the set of business rules, it should also take into account the existing interaction between alethic and deontic modalities. The desired interaction can be verbalized as \Everything which is necessary is also obligatory" and then expressed as a following FODAL formula:
X ! OX (2) It can be proved that the formula 2 de nes a special subclass of S4 KD-frames.
Theorem 1. The modal formula X ! OX de nes the subclass of augmented
bimodal S4 KD-frames F = hW; RO; R ; Di such that RO R , where R
is a preorder and RO is serial. We then call such frame a FODAL frame.
Proof: For the complete proof please refer to [
mented frame Fvar = hW; RO; R ; Di is a function which assigns to each mplace relation symbol P and to each possible world w 2 W some m-place relation on the domain D(w) of that world. I can be also interpreted as a function that assigns to each possible world w 2 W some rst-order interpretation I(w). A FODAL varying domain rst-order model is a structure M = hW; RO; R ; D; Ii, where hW; RO; R ; Di is a FODAL frame and I is an interpretation in it.
Truth in a model. The satis ability relation between FODAL models and formulae is then de ned in the usual way, using the notion of valuation which maps variables to elements of the domain.
Let M = hW; RO; R ; D; Ii be a FODAL model, X; Y and be FODAL formulae. Then for each possible world w 2 W and each valuation on D(M) the following holds: { if P is a m-place relation symbol, then M; w P (x1; :::; xm) if and only if ( (x1); :::; (xm)) 2 I(P; w) or, equivalently, I(w) F OL P (x1; :::; xm), { M; w :X if and only if M; w 2 X, { M; w X ^ Y if and only if M; w X and M; w Y , { M; w 8x if and only if for every x-variant 0 of at w, M; v , { M; w 9x if and only if for some x-variant 0 of at w, M; v , { M; w { M; w { M; w { M; w
X if and only if for every v 2 W such that wR v, M; v
X if and only if for some v 2 W such that wR v, M; v OX if and only if for every v 2 W such that wROv, M; v P X if and only if for some v 2 W such that wROv, M; v X, X, X, X. 3.3
A F ODAL axiom system for rst-order alethic-deontic logic is de ned following
the approach presented in [
Axioms. All the formulae of the following forms are taken as axioms. (Tautologies S4)
Any FOL substitution-instance of a theorem of S4 (Tautologies KD)
Any FOL substitution-instance of a theorem of KD (4) 8x 8x( ! 8x8y ! 8y8x 8y(8x (x) !
(y)) ; provided x is not free in ) ! (8x
! 8x ) (Vacuous 8) (8 Distributivity) (8 Permutation) (8 Elimination)
(Necessary O)
(Modus Ponens) (Deontic Necessitation) ! O !
O (3) (5) (6) (7) (8) (9) (10) (11) (Alethic Necessitation) (8 Generalization) 8x Theorem 2. The F ODAL axiom system is complete and sound with respect to the class of FODAL frames.
Proof: For the complete proof please refer to [
Given an SBVR conceptual schema S we de ne the following translation ( ) from elements of S to notions of rst-order deontic-alethic logic: { For each noun concept A from S, (A) is an unary predicate in FODAL. { For each verb concept R from S, (R) is an n-ary predicate in FODAL (n 2).
Recall that an SBVR business rule may be represented by an expression resulted from application of modalities and boolean connectives to a set of closed rstorder formulae r^i . Then for each SBVR rule r from S, its FODAL formalization (r) is de ned inductively as follows: { { { {
(r^) = r^, where r^ is an non-modal SBVR expression and r^ is its rst-order translation, (:r) = : (r); (r1 r2) = (r1) (r2); 2 f^; _; !; $g, where r1 and r2 are rule formulations,
( r^) = (r^) and (Or^) = O (r^): Example 1. Assume the following set of business rules, expressed in SBVR Structured English: (r1) Each car rental is insured by exactly one credit card. (r2) Each luxury car rental is a car rental. (r3) It is obligatory that each luxury car rental is insured by at least two credit cards.
Then the corresponding FODAL formulas are the following: (r1) = 8x91y(CarRental(x) ^ Insured(x; y)), (r2) = 8x(LuxuryCarRental(x) ! CarRental(x)), (r3) = O(8x9 2y(LuxuryCarRental(x) ^ Insured(x; y))).
While our F ODAL formalization of SBVR rules provides logical mechanism
supporting rule formulations with multiple occurrences of modalities, SBVR
standard mostly focuses on normalized business constraints [19, p.108] that may
be expressed by rule statements of the form of atomic modal sentences or by
statements reducible to such a form via mechanisms provided by F ODAL
axiomatization. As a matter of fact, restricting the domain of interest only to such
atomic modal rule formulations allows to obtain some useful results concerning
satis ability reduction and connection to standard logics, as shown in [
Hereafter we will only consider SBVR rules expressible in one of the following forms of atomic modal sentences: O
P (12) where is any closed w of rst-order logic.
In the case of having negation in front of the modal operator, we assume application of the standard modal negation equivalences in order to obtain the basic form of the initial rule.
FODAL regulation. A FODAL regulation is a set of FODAL atomic modal sentences formalizing structural and operational rules of an SBVR conceptual schema S. We introduce the following designations: (r ) =
; (rO ) = O ; (r ) =
; (rP ) = P ; = f 1; :::; ^ = k; k ^ i=1 1; :::;
l; O 1; :::; O m; P 1; :::; P ng l ^ i=1 i ^ i ^ where every i; i; i; i is a closed rst-order logic formula.
The nal objective of the proposed formalization is to provide an automation solution with reasoning support for SBVR business modeling and business processes monitoring. It is well known that when reasoning about some particular universe of discourse, consistency is essential.
Assume a FODAL regulation representing a set of structural and operative business rules. The task of consistency check for is de ned as procedure which analyzes the given set and decides whether the rules do not contradict each other, i.e. there is no formula such that ` ^ : ?.
A FODAL regulation is called internally inconsistent when the speci ed constraints contradict each other when the system is populated. We then de ne a minimal inconsistent set ? such that ? ` ? and 8 ?; 0 ?.
We distinguish several types of inconsistency depending on types of modalities of rules involved. The set is called alethic inconsistent if it is inconsistent and the minimal inconsistent set ? contains formulae of only alethic nature, i.e. ? . The set is called deontic inconsistent if it is inconsistent and the minimal inconsistent set ? contains formulae of only deontic nature, i.e. ? O. Otherwise, if ? [ O, the set is called cross inconsistent.
According to the completeness of the FODAL logic we have that 0 if and only if there exists a FODAL model M and a possible world w in it, such that M; w ^ : . Therefore, it is su cient to state the satis ability of the conjunction of all formulae of the set: ^ = k ^ i=1 i ^ l ^ i=1 i ^ Bearing in mind the fact that the regulation may only contain FODAL atomic modal sentences and taking into account the properties of accessibility relations of the FODAL frame F, we can obtain the following result: Theorem 3. A FODAL regulation ^ = Vik=1 i ^ Vli=1 i ^ Vim=1 O i ^ Vin=1 P i is FODAL-satis able if and only if each of the following formulae N ; O; Qj ; Pj is independently rst-order satis able:
k N = ^ i=1 m O = ^
i=1 Qj = j ^ Pj = j ^ i ^ k ^ i=1
i i i ^ k ^ i=1 m ^ i=1 i; 8j = 1 : : !:l k ^ i=1
Observe that satis ability of N follows naturally from satis ability of any Qj . The same holds for O and Pj respectively. However, the satis ability checks for 15a and 15b should be examined explicitly, since may only contain necessity and obligation rules. Moreover, such de nition allows to detect the actual source of unsatis ability of the FODAL regulation .
Modularity of the approach. It should be noted that the developed approach of satis ability reduction possesses a property of modularity, i.e. it does not depend on the formalism behind the rule bodies i; i; i and i, as long as formalism-speci c satis ability relation is provided. 6
As a matter of fact, the FODAL logic inherits the property of undecidability from
both its component logics: standard predicate modal logics QS4 and QKD are
undecidable [
F = hW; RO; R ; Di and a possible world w0 2 W, a monomodal simulating pointed frame Fw0 is de ned as a tuple hWs; Rs; Ds; w0i, such that: s { Ws includes w0 and all its deontic and alethic successors:
Ws = fw0g[fv j (w0; v) 2 ROg[fv j (w0; v) 2 R g = jsince RO R is re exivej = fv j (w0; v) 2 R g. { Rs = f(w0; v) j (w0; v) 2 R g, and
with Rs. { Ds is a domain function on Ws such that Ds(v) = D(v) [ f where Ds 2= D is a new service domain symbol.
R
and Ds g; 8v 2 W ,
s s; s are modal operators associated Since the de nition of Rs does not preserve speci c properties of RO and R , the resulting frame Fsw0 belongs neither to serial nor to transitive nor to re exive class of frames and therefore can be classi ed as a K-frame.
Monomodal translation. Given a FODAL regulation expressed as a conjunction of FODAL atomic modal sentences 14, a monomodal translation of regulation M T R( ^) is de ned inductively as follows: M T R( ) = ; where
is an objective FODAL formula; M T R( 1 ^ 2) = M T R( 1) ^ M T R( 2); where 1 and 2 are FODAL atomic M T R( M T R( ) = ) =
modal sentences; sM T R( ); s(M T R( ) ^ );
M T R(O ) = M T R(P ) = s(:
! M T R( )); s(M T R( ) ^ : ); where is a objective FODAL formula and is a 0-place predicate symbol, i.e. propositional letter, encapsulating the nature of the original modality of the rules of possibility and permission.
Simulated pointed model. Given a FODAL model M = hF; Ii and a possible world w0 2 W, a simulated pointed model Msw0 is de ned as a tuple hFsw0 ; Isi such that: { Fw0 = hWs; Rs; Ds; w0i is a monomodal simulating pointed frame for F = s hW; RO; R ; Di and a possible world w0 2 W, { Is is a rst-order interpretation on the frame Fsw0 such that:
For each v 2 Ws and for every n-place predicate P , Is(P; v) = I(P; v), For each v 2 Ws such that (w0; v) 2 RO, Is( ; v) = ?,
For each v 2 Ws such that (w0; v) 2= RO, Is( ; v) = f Ds g.
We now state formally that the translation given above is truth-preserving with respect to varying domain semantics.
Theorem 4. For any FODAL regulation possible world w0 of a model, we have that , any FODAL model M and any M; w0 if and only if
Msw0 ; w0
M T R( );
(16)
where Msw0 is a simulated pointed model for M and w0:
Proof: For the complete proof please refer to [
Therefore, the truth-preserving translation M T R de ned for FODAL regulations
enables the transfer of decidability results from well-studied fragments of
predicate modal logics ([
The ORM2 automated reasoning support tool is implemented in Java and
includes a parser for ORM2 Formal Syntax [
The algorithm of the developed automated reasoning support tool relies on two fundamental results.
Firstly, it implements the procedure de ned in [
Secondly, in order to check the consistency of a set of business rules expressed
in ALCQI-de nable fragment of ORM2, we utilize the modularity of the
approach de ned in Section 5 and adapt the result of satis ability reduction for
the case of general description logic DL. The satis ability relation for ORM2 is
then provided by the semantic-preserved translation from ORM2 Formal Syntax
to ALCQI [
N
DL Qj = j u = k l i=1 i=1 i;
i Theorem 5. A FODAL regulation = f 1; :::; k; 1; :::; l; O 1; :::; O m; P 1; :::; P ng, expressed in DL-de nable fragment of ORM2, is internally consistent if and only if each of the following description logic formulae N DL , ODL , QjDL , PjDL is independently satis able in DL:
DL lk DL lm lk
DL Pj = j u
O m l i=1 = i u i=1 k l i=1 i u
i i=1
Thus, we can reduce the consistency of a given set of constraints to ALCQI satis ability, which in turn can be interpreted as unsatis able concepts' check in resulting OWL2 ontology. Indeed, whenever a formula in ALCQI is unsatisable, it means that the concept de nition expressed by this formula contains a contradiction which prevents the concept from having a model, i.e. the concept is forced to not have any instances, hence is unsatis able. In the following section we will demonstrate the functionality of the implemented tool by means of a real-life example of its usage. The graphical user interface of a tool is introduced on Figure 5 and contains controls which allow to select an input le, underlying reasoner, output le and output format for resulting ontology (if needed). The consistency check for an input ORM2 schema is performed after loading the input le and the result of the check is communicated by visual ag as well as by a detailed log in the corresponding window.
Checking the consistency of a given ORM2 schema. In order to illustrate the functionality of the consistency check we will consider the ORM2 schema obtained by merging two conceptual models (e.g. A and B) and depicted on the Figure 4. This schema contains the following set of con icting business rules: (R1A) Each car rental is insured by exactly one credit card. (R1B) Each luxury car rental is a car rental. (R2B) It is obligatory that each luxury car rental is insured by at least two credit cards.
Fig. 4. Inconsistent ORM2 Schema
The given set of constraints can be fully expressed in ALCQI description logic, therefore we can use the developed reasoning support tool for consistency check. The schema on Figure 4 is internally inconsistent with respect to obligation (R2B) since the latter clearly contradicts the structural constraint (R1A) which, together with is-a constraint on luxury car rental, simply does not support more than one credit card. Therefore, for any luxury car rental the obligatory cardinality constraint cannot be satis ed. The same conclusion is indeed inferred by the implemented tool on Figure 5.
Fig. 5. The Graphical User Interface 8
In this paper we introduced a logical formalization of the Semantics of Business Vocabulary and Rules standard (SBVR) by de ning a rst-order deontic-alethic logic (FODAL) with its syntax, semantics and complete and sound axiomatization, that captures the semantics of and interaction between business rules.
We also showed that satis ability in FODAL logic may be reduced to a standard rst-order satis ability for a class of formulas restricted to atomic modal sentences. Moreover, in order to establish a relationship with a standard logical formalism, we de ned a truth-preserving translation from a fragment of bimodal FODAL into quanti ed monomodal logic QK, that can be used to facilitate the transfer of decidability results from well-studied fragments of predicate modal logics to FODAL.
Finally we presented the ORM2 reasoning tool which provides an automated support for consistency checks of the conceptual model along with its translation to OWL2 ontology. The main functionality of the tool is a consistency check of a set of ALCQI-expressible deontic and alethic business rules. Another important task supported by the tool is translation of the aforementioned fragment of an ORM2 schema into an OWL2 ontology, which, however, does not support any modalities except necessity due to lack of notions representing deontic constraints in OWL2.
The future research in the eld of logical formalization of SBVR aims at studying the problem of entailment with respect to possible interaction of alethic and deontic modalities. Another future course of work includes de ning an approach to translate an ORM2 schema with its alethic and deontic rules to SWRL or some other extension of OWL2.