The business process planner relies on external services for particular tasks. The tasks performed by each of the providers or the planner are often NP-complete, e.g. the Traveling Salesman Problem. Therefore, finding a combined solution is a computationally (as well as conceptually) complex task. Such a central planner could be used in business process management in e.g. logistics service provider, manufacturer supply chain management, mid-size businesses relying on external web services and cloud computing. The main challenge is a high level of uncertainty and that each module can be described in a different language. The language is determined by its suitability for the task and the expertise of the local developers. To allow for multiple languages, we approach the problem of finding combined solutions model-theoretically. We describe a knowledge representation formalism for representing such systems and then demonstrate how to use it for representing a business process planner. We prove correctness of our representation, describe general properties of modular systems and ideas for how to automate finding solutions.
Formulating AI tasks as model finding has recently become very promising due to the overwhelming success of SAT (propositional satisfiability) solvers and related technology such as ASP (answer set programming) and SMT (satisfiability modulo theories). In our research direction we focus on a particular kind of model finding which we call model expansion. The task of model expansion underlies all search problems where for an instance of a problem, which we represent as a logical structure, one needs to find a certificate (solution) satisfying certain specification. For example, given a graph, we are looking for its 3-colouring in a classic NP-search problem. Such search problems occur broadly in applications; they include planning, scheduling, problems in formal verification (where we are looking for a path to a bug), computational biology, and so on. In addition to being quite common, the task of model expansion is generally simpler (for the same logic) than satisfiability from the computational point of view. Indeed, for a given logic L, we have, in terms of computational complexity,
MC(L)
MX(L)
Satisfiability(L);
where MC(L) stands for model checking (structure for the entire vocabulary of the
formula in logic L is given), MX(L) stands for model expansion (structure interpreting a
part of the vocabulary is given) and Satisfiability(L) stands for satisfiability task (where
we are looking for a structure satisfying the formula). A comparison of the complexity
of the three tasks for several logics of practical interest is given in [
The next step is to extend the framework to a modular setting. In [
In systems like our planner, a high level of uncertainty is present. In our framework, we can model the following types of uncertainty.
– Each agent can see only the inputs and the outputs of other modules, but not their internals. The modules are viewed as black boxes by the outside world. Modules communicate with each other through common vocabulary symbols. – Modules can be represented using languages that are not known to other modules.
Such languages can even be old and no longer supported, as is common for legacy systems. – Each module (an agent) can have multiple models (i.e., structures satisfying an axiomatization), each representing a possible plan of an individual module. This is a feature that generates uncertainty in planning. We view each module abstractly as a set of structures satisfying the axioms of the module.
The main challenge is that each module can be represented in a different language, reflecting the local problem’s specifics and local expertise. Thus, the only way to formalize such a system is model-theoretic. Our goal is not only to formalize, but to eventually develop a method for finding solutions to complex modular systems like the BPP. This is a computationally complex task. Our inspiration for finding solutions to such systems comes from “combined” solvers for computationally complex tasks such as Satisfiability Modulo Theories (SMT). There, two kinds of propagation work interactively – propositional satisfiability (SAT) and theory propagation. In the case of modular systems, each module will have a so-called oracle that is similar to solvers/propagators used in SMT. If the logic language used by a module has a clear model-theoretic semantics, such an oracle (propagator) is easy to construct, but in the most extreme cases, derivations can be even performed by a human expert. At the level of solving, oracles would interact using a common internal solver language with a clear formal semantics. We believe that a formal model-theoretic approach is the right approach to developing a general algorithm for solving modular systems such as the BPP. This is another important motivation for developing a rigorous model-theoretic framework.
In this paper, we demonstrate how to use ideas of model expansion and modular systems together to naturally represent modular systems such as BPP. We prove correctness of our formalization and explain how finding solutions to such systems can be automated.
A business process planner is an entity which plans a particular task by relying on external services for particular tasks. Often, in business, there are cases when one needs to buy services from other service providers. The planner combines services provided by different companies to minimize the cost of the enterprise. The customer needs to allocate required services to different service providers and to ask them for their potential plans for their share. These plans will then be used to produce the final plan, which can be a computationally complex task. The tasks performed by each of the providers are often NP-complete, e.g. the Traveling Salesman Problem. Therefore, finding a combined solution is a computationally (as well as conceptually) complex task. Such a central planner could be used in business process management in many areas such as: – Logistics Service Provider operates on the global scale, uses contracted carriers, local post, fleet management, driver dispatch, warehouse services, transportation management systems, e-business services as well as local logistics service providers with their own sub-modules. – Manufacturer Supply Chain Management uses a supply chains planner relying on transportation, shipping services, various providers for inventory spaces, etc.. It uses services of third party logistics (3PL) providers, which themselves depend on services provided by smaller local companies. – Mid-size Businesses Relying on External Web Services and Cloud Computing Such businesses often use data analysis services, storing, spreadsheet software (office suite), etc.. The new cloud-based software paradigm satisfies the same need in the domain of software systems.
R S
R1 S1 Provider1 P1
P1' P2' P3'
Planner R2 S2 Provider2 P2
R3 S3 Provider3 P3
P
The business process planner in Figure 1 takes a set S of services and a set R of restrictions (such as service dependencies or deadlines) and generates plan P . Each “Provideri” takes a subset of services Si and their restrictions Ri. Provideri generates a potential plan Pi for subset Si of services and returns it to “Planner”. Planner takes all these partial plans and, if not satisfied with them, reconsiders service allocations or providers. However, if satisfied, it outputs plan P by combining partial plans Pi. 3
In [
Recall that a vocabulary is a set of non-logical (predicate and function) symbols. An interpretation for a vocabulary is provided by a structure, which consists of a set, called the domain or universe and denoted by dom(:), together with a collection of relations and (total) functions over the universe. A structure can be viewed as an assignment to the elements of the vocabulary. An expansion of a structure A is a structure B with the same universe, and which has all the relations and functions of A, plus some additional relations or functions. The task of model expansion for an arbitrary logic L (abbreviated L-MX), is:
Given: (1) An L-formula
(2) A structure A for Find: an expansion of A, to with vocabulary
[ " and [ ", that satisfies .
We call , the vocabulary of A, the instance vocabulary, and " := vocab( ) n expansion vocabulary1. the Example 1. The following formula in the language of logic programming under answer set semantics constitutes an MX specification for Graph 3-colouring. ? ? ?
V (x): An instance is a structure for vocabulary = fEg, i.e., a graph A = G = (V ; E). The task is to find an interpretation for the symbols of the expansion vocabulary " = fR; B; Gg such that the expansion of A with these is a model of : 1 By “:=” we mean “is by definition” or “denotes”.
Given a specification, we can talk about a set (class) of ["-structures which satisfy the specification. Alternatively, we can simply talk about a set (class) of [ "-structures as an MX-task, without mentioning a particular specification the structures satisfy. Example 2 (BPP as Model Expansion). In Figure 1, both the planner box and the provider boxes can be viewed as model expansion tasks. For example, the box labeled with “Provider1” can be abstractly viewed as an MX task with instance vocabulary = fS1; R1g and expansion vocabulary " = fP1g. The task is: given some services S1 and some restrictions R1, find a plan P1 to deliver services in S1 such that all restrictions in R1 are satisfied.
Moreover, in Figure 1, the bigger box with dashed borders can also be viewed as an MX task with instance vocabulary 0 = fS; Rg and expansion vocabulary "0 = fP g. This task is a compound MX task whose result depends on the internal work of all the providers and the planner. 4
This section presents the main concepts of modular systems.
structures, where M is the instance vocabulary, "M is the expansion vocabulary. Each module can be axiomatized in a different logic. However, we can abstract away from the logics and study modular systems entirely model-theoretically.
A modular system is formally described as a set of primitive modules (individual
sets of structures) combined using the operations of:
1. Projection( (M )) to restrict a module’s vocabulary,
2. Composition(M1 B M2) to connect outputs of M1 to M2,
3. Intersection(M1 \ M2),
4. Union(M1 [ M2),
5. Feedback(M [R = S]) which connects output S of M to its inputs R.
Formal definitions of these operations were introduces in [
The initial development of of our algebraic approach was inspired by [
if "M1 \ "M2 = ; (no output interference). Module M1 is independent from M2 if
M1 \ "M2 = ; (no cyclic module dependencies).
Definition 3 (Modular Systems). Modular systems are built inductively from constraint modules using projection, composition, union and feedback operators: Base Case A primitive module is a modular system.
Projection For modular system M and M [ "M , modular system (M ) is defined such that (a) (M) = M \ , (b) " (M) = "M \ , and (c) B 2 (M ) iff there is a structure B0 2 M with B0j = B.
Composition For composable modular systems M and M 0 (no output interference) with M independent from M 0 (no cyclic module dependencies), M B M 0 is a modular system such that (a)
MBM0 = M [ ( M0 n "M ), (b) "MBM0 = "M [ "M0 , and (c) B 2 (M B M 0) iff Bjvocab(M) 2 M and Bjvocab(M0) 2 M 0.
Union For modular systems M1 and M2 with M1 \ M2 = M1 \"M2 = "M1 \ M2 = ;, the expression M1 [ M2 defines a modular system such that (a) M1[M2 =
M1 [ M2 , (b) "M1[M2 = "M1 ["M2 , and (c) B 2 (M1[M2) iff Bjvocab(M1) 2 M1 or Bjvocab(M2) 2 M2.
Feedback For modular system M and R 2 M and S 2 "M being two symbols of similar type (i.e., either both function symbols or both predicate symbols) and of the same arities; expression M [R = S] is a modular system such that (a) M[R=S] =
M n fRg, (b) "M[R=S] = "M [ fRg, and (c) B 2 M [R = S] iff B 2 M and RB = SB.
M1 \ "M2 =
Further operators for combining modules can be defined as combinations of basic
operators above. For instance, [
M2 \ "M1 = "M1 \ "M2 = ;.
( M [ "M )-structure B is a model of M if B 2 M .
Since each modular system is a set of structures, we call the structures in a modular system models of that system.
Example 3 (Stable Model Semantics). Let P be a normal logic program. We know S is a stable model for P iff S = Dcl(P S ) where P S is the reduct of P under set S of atoms (a positive program) and Dcl computes the deductive closure of a positive program, i.e., the smallest set of atoms satisfying it. Now, let M1(S; P; Q) be the module that given a set of atoms S and ASP program P computes the reduct Q of P under S. Also, let M2(Q; S0) be a module that, given a positive logic program Q, returns the smallest set of atoms S0 satisfying Q. Now define M as follows:
M :=
fP;Sg((M1 B M2)[S = S0]): Then, M represents a module which takes a ground ASP program P and returns all and only its stable models. Figure 2 shows the corresponding diagram of M . L Dcl
P’ Reduct L’
P
On a model-theoretic level, this module represents all possible ASP programs and all their solutions, where programs are encoded by structures. While such a module is certainly possible, a more practical use would be where one module corresponds to a particular ASP program such as the one for graph 3-colouring in Example 1. Nevertheless, the Example 3 is useful because it represents a well-known construction and illustrates several concepts associated with modular systems.
Example 4 (BPP as a Modular System). Figure 1 can be viewed as a modular representation of the business process planner. There, each primitive module is represented by a box with solid borders and our module of interest is the compound module which is shown by the box with dotted borders. This module is specified by the following formula:
BP P := fS;R;P g(Planner B ((Provider1 \ Provider2\ Provider3)[P10 = P1][P20 = P2][P30 = P3])): (1) As in Figure 1, the only vocabulary symbols which are important outside the big box with dashed borders are S, R and P . There are also three feedbacks from P1 to P10, P2 to P20, and P3 to P30. 5
In this section we give a detailed description of one of the many kinds of business process planners, i.e., a logistics service provider on the global scale which hires local carriers and warehouses. So, in Figure 1, “Planner” refers to the global entity and “Provider” refers to local entities.
The logistics provider need a plan to execute the services so that all restrictions are met. Some sample restrictions are: (1) latest delivery time (e.g., Halloween masks should be in stores before Halloween), (2) type of carrying vehicles (perishable products need refrigerator trucks), and (3) level of care needed (glass-works should be carried carefully).
We say that a plan P is good for a set of services S and restrictions R (Good(P; S; R)) if P does all services in S and satisfies all restrictions in R. For simplicity, here, we only consider time restrictions, i.e., the value of t(i) is the (latest) delivery time for item i. There are also functions s(:) and d(:) to indicate the source and the destination of an item. For an item i, a plan is a sequence of cities hc1; along with its pickup times pt(i; j) and arrival time at(i; j). So, we have that2: ; cni 8i 2 Items (P (i) = hc0; ; cni
c0 = s(i) ^ cn = d(i)); 8i 2 Items (P (i) = hc0; ; cni 8i 2 Items (P (i) = hc0; ; cni
8j 2 [1; n] (connected(cj 1; cj )); 8i 2 Items (P (i) = hc0; ; cni
8j 2 [0; n] (pt(i; j) at(i; j))); 8i 2 Items (P (i) = hc0; ; cni 8j 2 [1; n] (at(i; j) = pt(i; j at(i; n)
t(i)); 1) + time(cj 1; cj ))): Intuitively, these axioms tell us that a plan for each item should: (1) start at the source and end at the destination, (2) arrive at the destination sooner than their latest delivery time, (3) pass through cities which are connected to each other, (4) respect time constraints, i.e., be picked up at a city after they have arrived at that city, and (5) respect the distance between cities. Certainly, a good plan needs to satisfy all these conditions, but, of course, this does not give us a full axiomatization of the problem. Here, we do not even intend to do that, because we believe that this is enough for the reader to have a good idea on how such full axiomatizatins look like.
Given a definition of a good plan, one can define the intended solutions of a business process planner as below: Definition 5 (Intended Solutions). Let BP P be a business process planner with access to n providers. Structure B is an intended solution of BP P if: 1. P B is good for SB and RB, i.e., B j= Good(P; S; R), 2. All atomic actions A of P B (here, moving items between different cities) are doable by one of the n providers.
So, by Definition 5, if some set of services cannot be executed under some restrictions, there should not exist any solution for the whole modular system which interprets S by those services and R by those restrictions.
Now, to ensure that the intended solutions of modular system in Figure 1 coincide with the models of this modular system under our modular semantics, we use the declarative representations below for the modules: 2 We slightly abuse logic notations here to keep the axiomatization simpler. For example, we use the notation P (i) = hc0; ; cni to denote that item i takes a path starting at city c0 and then going to city c1 and so on until it getting to city cn. In practice, such a specification can be realized using two expansion function “len(:)” (to show the length of the path of an item) and “loc(:; :)” (to show its location). As an example, this is how the first axiom above is rewritten in terms of “len” and “loc”:
8i 2 Items (loc(i; 0) = s(i) ^ loc(i; len(i)) = d(i)):
Module “Planner” is the set of structures over vocabulary and " = fP; S1; ; Sn; R1; ; Rng which satisfies: = fR; S; P1; ; Png Good(P; S; R) ,
i2f1; ;ng P is a join of sub-plans Pi(for i 2 f1; ^
Good(Pi; Si; Ri); ; ng): This module is easily specifiable in extended FO.
Module “Provideri” is the set of structures over vocabulary = fRi; Sig and " = fPig which satisfy Good(Pi; Si; Ri). Each such module “Provideri” can be specified using mixed integer linear programming. Also, in practice, many such modules are realized using special purpose programs (so, no standard language). Our framework enables us to deal with such programs in a unified way.
Proposition 1 (Correctness). Structure B is in modular system BP P := fS;R;P g(Planner B ((Provider1 \ \ Providern)[P10 = P1] [Pn0 = Pn])) (where “Planner” and “Provideri”s are defined as above) iff B is an intended solution of BP P (according to Definition 5).
Proof. (1) Take B which satisfies all modules, each PiB has to be good for SiB and RB. i Therefore, P B is good for SB and RB. Thus, B is an intended solution of BP P . (2) Conversely, take an intended solution B. P B should be such that P B is good for SB and RB. So, set B0 to be an expansion of B such that PiB0 is the parts of P B which are executed by i-th provider. Also, SiB0 is those services that PiB0 executes and RiB0 is those restrictions satisfied by PiB0 , e.g., the latest delivery time of item a is the delivery time of a according to PiB0 . Now, PiB0 is good for SiB0 and RiB0 . So, B 2 BP P . 6
Complexity of the modular framework In this subsection, we summarize one of
our important results about the modular framework from [
R(v) R(v)
S(v):
R(u); E(u; v); not B(u): where S represents a set of source vertices of a graph, E represents the edges of the graph, B represents a set of blocked vertices of the graph and R represents a set of vertices which can be reached from a source vertex without passing any blocked vertices.
Through this section, let MR denote a primitive module which represents the MX task of Example 5. Obviously, MR = fS; E; Bg and "MR = fRg: Then, we have: Totality: Module MR is fS; E; Bg-fRg-total because for every interpretation of S, E and B, there is an interpretation for R which is a stable model of program 4. Determinacy: Module MR is fS; E; Bg-fRg-deterministic because for every interpretation of S, E and B, there is at most one interpretation for R which satisfies (4).
Monotonicity: Module MR is fEg-fS; Bg-fRg-monotone because if we fix the interpretation of symbols S and B and increase the set of edges E, then the interpretation of R (reachable vertices) increases.
Anti-monotonicity: Module MR is fEg-fS; Bg-fRg-anti-monotone because if we fix the interpretation of S and E and increase the set of blocked vertices (B), then, the set R of reachable vertices decreases.
Polytime Checkability/Solvability: Module MR is both polytime checkable (because one can check in polynomial time if a structure B belongs to MR) and polytime solvable (because, given interpretations to S, E and B, one can compute the only valid interpretation for R in polynomial time). However, the module MC which corresponds to the graph 3-coloring (Example 1) is polytime checkable but not polytime solvable (unless P=NP).
Now, we are ready to restate our main theorem from [
class of finite structures closed under isomorphism. Then, the following are equivalent: 1. K is in NP, 2. K is the models of a modular system where all primitive modules M are M -"M deterministic, M -total, M -vocab(K)-"M -anti-monotone, and polytime solvable, 3. K is the models of a modular system with polytime checkable primitive modules.
Note that Theorem 1 shows that when basic modules are restricted to polytime checkable modules, the modular system’s expressive power is limited to NP. Without this restriction, the modular framework can represent Turing-complete problems. As an example, one can encode Turing machines as finite structures and have modules that accept a finite structure iff it corresponds to a halting Turing machine.
Theorem 1 shows that the feedback operator causes a jump in expressive power from P to NP (or, more generally, from kP to kP+1).
Example 6 (Stable Model Semantics). In Example 3, firstly, note that primitive module M1 is fSg-total and fSg-fP g-fQg-anti-monotone, and also polytime solvable. Secondly, module M2 is fQg-total, fQg-fg-fS0g-monotone and, again, polytime solvable. However, the module M := fP;Sg((M1 B M2)[S = S0]) is neither total nor monotone or anti-monotone. Moreover, M represents the NP-complete problem of finding a stable model for a normal logic program. This shows how, in the modular framework, one can describe a complex modular system in terms of very simple primitive modules. Solving modular systems We would like to find a method for solving complex tasks such as the application in this paper, without limiting to the particular structure of Figure 1, and without committing to a particular language. The language is determined by its suitability for the task and the expertise of the local developers. For example, the planner module is more easily specified as a SAT (propositional satisfiability) problem, while some provider modules are most easily specified using MILP (mixed integer linear programming), and global constraints with CP (constraint programming). A module performing scheduling with exceptions is more easily specified with ASP (answer set programming).
In our research, we focus on the central aspect of this challenging task, namely on solving the underlying computationally complex task, for arbitrary modular systems and arbitrary languages suitable for specifying combinatorially hard search/optimization problems. Our approach is model-theoretic. We aim at finding structures satisfying multi-language constraints of the modular system, where the system is viewed as a function of individual modules. Our main goal is to develop and implement an algorithm that takes a modular system as its input and generates its solutions. Such a prototype system should treat each primitive module as a black-box (i.e., should not assume access to a complete axiomatization of the module). Not assuming complete knowledge is essential in solving problems like business process planning.
We take our inspiration in how “combined” solvers are constructed in the general
field of declarative problem solving. The field consists of many areas such as MILP, CP,
ASP, SAT, and each of these areas has many solvers, including powerful “combined”
solvers such as SMT, ASP-CP solvers. There are several methods e.g. cutting plain
techniques of ILP, the formal interaction between SAT and theory solvers in SMT, etc.
used in different communities. We made the fundamental observation [
In [
An early work on adding modularity to logic programs is [
Applications such as business process planning need an abstract notion of a module,
independent from the languages used. Our MX-based modular framework is well-suited
for this purpose. That cannot be said about many other approaches of adding modularity
to ASP languages and FO(ID) (such as those described in [
Modular programming enables ASP languages to be extended by constraints or
other external relations. This view is explored in [
Yet another direction to modularity is the multi-context systems. In [
In this paper, we introduced an important range of real-world applications, i.e., business
process planning. We discussed several examples of where this general scheme is used.
Then we represented this problem as a model expansion task in the modular setting
introduced in [
Reduction in Search Space We will improve our algorithm by using approximation
methods proposed in [