Techne: A(nother) Requirements Modeling Language
Alexander Borgida
Dept. of Computer Science
Rutgers University
borgida@cs.rutgers.edu
Neil Ernst
Dept. of Computer Science
University of Toronto
nernst@cs.toronto.edu
Ivan J. Jureta
FNRS & Info. Management
University of Namur
ijureta@fundp.ac.be
Alexei Lapouchnian
Dept. of Computer Science
University of Toronto
alexei@cs.toronto.edu
Sotirios Liaskos
School of Information Tech.
York University
liaskos@yorku.ca
John Mylopoulos
Dept. of Computer Science
University of Toronto
jm@cs.toronto.edu
Abstract
This paper introduces the requirements modeling lan-
guage called Techne, in response to a new core ontology
for requirements [5]. The basic elements of Techne models
are propositions that represent domain assumptions, goals,
quality constraints, or tasks. Moreover, goals and qual-
ity constraints may be mandatory or optional and there
can be preference relations defined over them. Given a re-
quirements problem consisting of mandatory/optional goals
and domain assumptions, a solution consists of a collection
of tasks and quality constraints which together satisfy all
mandatory goals and do as well as possible with respect to
optional ones. A formal semantics is provided for Techne,
along with a syntax, as well as illustrative examples.
1 Introduction
Requirements modeling languages have been part of the
very core of Requirements Engineering (RE) research since
the days of SADT [9], with KAOS [3], i* [11], and oth-
ers, serving as state-of-the-art for much of the on-going re-
search. Every requirements modeling language is grounded
in an ontology of requirements, i.e., a set of assumptions
about what requirements are. Traditionally, requirements
were viewed as functions the system-to-be ought to sup-
port. This view is reflected in SADT and other structured
analysis techniques of the ’70s and ’80s. More recently, an
intentional perspective on requirements has gained ground:
requirements are now viewed as stakeholder goals repre-
senting the intended purposes for the system-to-be. This de-
ceptively small shift in the underlying ontology for require-
ments has had tremendous impact on requirements elicita-
tion, modeling and analysis techniques.
Jureta et al. [5] proposed recently a new core ontology
for requirements which extends the goal-oriented perspec-
tive to allow for optional (“nice-to-have”) requirements and
preferences (“requirement A is referred over requirement
B”). The proposal also treats fully non-functional require-
ments (“softgoals”) in terms of approximations and quality
constraints. In all, the proposal is a rather drastic extension
of the small (and beautiful) set of concepts used in the past
to formalize requirements (cf., e.g., [3, 12]). The exten-
sion, by the way, was much needed to align RE theory with
RE practice where optionality and prioritization of require-
ments has been used routinely to manage requirements.
The main objective of this paper is to study the impact
of the extended ontology for requirements (hereafter core
ontology) on requirements modeling languages. We do so
by proposing a new requirements modeling language called
Techne, founded on the new core ontology. In addition, we
adopt the definition of the requirements problem that ac-
companies the new core ontology and apply it to our lan-
guage by defining precisely what does it mean for a speci-
fication (a set of tasks and associated quality constraints) to
satisfy a given set of mandatory/optional requirements.
The rest of the paper is structured as follows. We first
offer a nontechnical introduction to representation and rea-
soning in Techne via the standard meeting scheduler exam-
ple (x2). We subsequently overview the syntax and seman-
tics of Techne (x3) and discuss one approach to reasoning
on Techne models (x4). We close with a discussion of re-
lated work, and a summary of conclusions and directions
for future efforts (x5).
2 Techne Models
The purpose of Techne is to support the representation
and reasoning about instances of the requirements problem
and the alternative solutions to a given instance of the re-
quirements problem. As the requirements problem is de-

Scheduling is
convenient
Scheduling
is flexible
Accommodate many
change requests
Accommodate late
change requestsObtain change
requests via web
form
Change reqs can be
sent up to 3h prior
Quickly compute
possible dates&times
Easily collect
participants’ calendar
constraints
Easily obtain
participation answers
Meeting is
scheduled
Scheduling is
manual
Scheduling is
automated
I
Obtain
constraints via
web form
Collect participants’
calendar constraints
by phone
Obtain change
reqs by phone
Send location on
an interactive map
Send
invitations
by email
Connect email
application with an
online maps API
Send
confirmation
by email
Implement
web form for
constraints
Send link to web
form by email
Call each
participant
Implement
web form for
change reqs
Collect
constraints via
email
Request constraints
via emailUse standard
email application
Leave web form for
change reqs open
up to 3h prior
Leave web form for
change reqs open
up to 6h prior
I
ss
ss
g
q q
I
I
P
I
s
s s
g
I
gg
I
g
g
I
g
I
g
C
C
I
g
OC
t
g
t
t
I
I
t
I
g
I
P
t
I
t I
I
t
It
Change reqs can be
sent up to 6h prior
t
I
Inference
node
C
Conflict
node
P
Preference
node
O
Optionality
node
t
g
k
All participants
use email
Have all
participants’
emails
k
k
I
Domain
assumption node
Task node
Goal node
Quality
constraint nodeq
Softgoal nodes
Legend:
I
Figure 1. An r-net capturing requirements about the meeting scheduler problem.
fined via the concepts and relationships of the core on-
tology, Techne incorporates the requirements net (r-net),
which captures the instances of the concepts and relation-
ships of the core ontology. These instances are acquired via
requirements elicitation, or produced by the application of
RE methods. An r-net thereby represents the various goals,
tasks, softgoals, and so on, along with specific relationships
between these. Different parts of an r-net capture differ-
ent solutions to the same given requirements problem. To
facilitate the comparison of the solutions in terms of de-
sirability, Techne uses the solution net (s-net); an s-net is
obtained by a transformation of an r-net, and relates solu-
tions in terms of preference and optionality. The aim in this
section is to introduce the r-net and s-net via the standard
meeting scheduler requirements problem, and in doing so
recall the core ontology and highlight the salient features of
the two Techne models.
Suppose that we need to build a meeting scheduler sys-
tem. We can readily identify two ways, one automated and
another manual to schedule a meeting. The former could
involve the use of email and web forms. One web form
could be used by participants to provide their calendar con-
straints, while another web form could be used to enter the
requests to change the meeting date, time, and/or location.
The links to the web forms and the invitations to meetings
would be sent by email to all participants. The manual
approach could simply amount to arrange a meeting with
participants via phone calls. If we consider in more detail
each of these approaches, we can identify various functional
and nonfunctional requirements for the meeting scheduler,
along with tasks to perform in order to satisfy the various
requirements, preferences between goals, tasks, and others,
conflicts between some of them, and their refinements.
Concepts. An r-net for the meeting scheduler requirements
problem is shown in Figure 1. An r-net is a directed la-
beled graph. Each node is a proposition about the system-
to-be and/or its relevant environment. Figure 1 shows each
proposition next to a node (circle or triangle), whereby each
node is labeled by a symbol. The symbol indicates the con-
cept or relationship of the core ontology, of which the given
proposition is an instance. Following the core ontology, if
a proposition represents a condition that is believed to hold
about the system-to-be and/or its relevant environment, then
this proposition is an instance of the domain assumption
concept, and is labeled k. Desired conditions that should
be satisfied are captured via instances of the goal (g), qual-
ity constraint (q), and softgoal (s) concepts. A goal will
describe a verifiable functional condition (e.g., “g: Obtain
change requests via web form” in Figure 1), while a quality
constraint will further restrict the values of non-binary mea-
surable characteristics of the system-to-be (e.g., “q: Change
reqs can be sent up to 3h prior”). While a quality con-
straint will restrict the values of a quality defined over a
well-defined quality space, a softgoal will do so over qual-
2

ities with ill-defined quality spaces (e.g., “s: Accommodate
late change requests”). Tasks, i.e., instances of the task
concept (t), capture the intentions to satisfy goals, quality
constraints, and softgoals in some known manner: e.g., “t:
Use standard email application” in Figure 1.
Relationships. Instances of domain assumptions give us
instances of the relationships. E.g., if we believe that “satis-
fying the conjunction of two goals A and B is enough to
satisfy the goal C”, then this is an instance of a domain
assumption, which gives the relationship between the con-
junction of the goals A and B, and the goal C. While not
all domain assumptions convey relationships (e.g., “k: All
participants use email” in Figure 1), we are interested in
four relationships that some domain assumptions do con-
vey: the binary inference (I), conflict (C), and preference
(P), and the unary optionality (O). An instance of infer-
ence relates a set of instances of any concept or relation-
ship to another instance of a concept or relationship, to con-
vey that satisfying the conjunction of the former satisfies
the latter. It is straightforward to see that an inference node
can capture the usual (goal) refinement relationship (e.g.,
[3]), the means-ends and task decomposition relationships
[11], and the approximation relationship, standing between
a softgoal and its proxies (which are instances of other con-
cepts and/or relationships in the core ontology) [5]. If two
propositions/nodes are linked via a conflict node, then these
propositions cannot be satisfied together.
Attitudes (i.e., emotions, feelings, and moods) are cap-
tured via instances of optionality and preference relation-
ships. Optionality is an attribute of any of the said concepts
indicating its optional or compulsory status: e.g., a candi-
date system-to-be must satisfy all compulsory goals, while
it would be good if it satisfied as many of the optional goals
as feasible. In Figure 1, the goal “g: Send location on an
interactive map” is made optional by an optionality node
connected to that goal. An instance of the preference rela-
tionship compares instances of any concept or relationship
in terms of desirability: e.g., a preference will indicate that
a goal is strictly preferred to another goal, that satisfying
some goal is preferred to executing some plan, or that one
preference is more important than another preference. Any
preference node indicates strict preference: e.g., in Figure
1, a preference node indicates that the quality constraint “q:
Change reqs can be sent up to 3h prior” is strictly preferred
to the quality constraint “q: Change reqs can be sent up to
6h prior”.
R-nets and Usual Models. An r-net differs from the usual
goal-oriented requirements models in several respects. (1)
It can represent the instances of all concepts of the core on-
tology, along with the inference, conflict, preference, and
optionality relationships. (2) An r-net is versatile: we can
relate any node to any other node via an inference node,
a conflict node, or preference node. We can therefore ex-
press preferences over preferences, preferences over infer-
ence applications, conflicts between preferences, conflicts
between inference applications, and optional preferences,
among others. (3) An r-net abstracts from the RE method
used to obtain the content represented in that r-net. For
example, we could have used the usual goal refinement
method to conclude that the conjunction of the three goals
“g: Obtain change requests via web form”, “g: Send invita-
tions by email” and “g: Obtain constraints via web form”,
refines the goal “g: Scheduling is automated”. Techne is
only interested in how the former goals relate to the latter
goal in terms of satisfaction, and is uninterested by what
RE method was applied to obtain the goals, or to conclude
the way ones affect the satisfaction of the others. In a sum-
mary then, Techne covers fully the core ontology, has a syn-
tax that obeys less constraints than alternative goal-oriented
modeling languages in RE (e.g., we can accommodate via
inference nodes not only the goal refinement relationship
of KAOS, but also the means-ends and task decomposition
relationships of i*, and the softgoal approximation relation-
ship), and is not specialized and thereby constrained to par-
ticular RE methods.
Reasoning. A solution to the requirements problem is a
combination of tasks and domain assumptions, such that
the execution of the tasks in the conditions given by do-
main assumptions entails the satisfaction of all compulsory
goals and quality constraints, and of zero or more optional
goals and quality constraints. Given the r-net in Figure 1
the question to ask is if there are solutions in that r-net.
If solutions are present, the next relevant question is how
they compare in terms of preference and optionality. These
questions are answered by the application of reasoning pro-
cedures on an r-net (cf., x4). To find a solution, we perform
simulation: we assume that some sets of tasks are executed,
and we traverse the r-net in order to determine the conse-
quences of the execution of these tasks on the satisfaction
of goals, quality constraints, and so on. E.g., if we assume
that the task “t: Use standard email application” is exe-
cuted (equivalently, satisfied or true), and that the domain
assumptions “k: All participants use email” and “k: Have
all participants emails” are true, then inference nodes tell
us that the goals “g: Send confirmation by email” and “g:
Send invitations by email” are satisfied/true. If we assume
the truth of the task “t: Call each participant”, the goal “g:
Obtain change reqs by phone” will be satisfied, but neither
“q: Change reqs can be sent up to 3h prior” nor “q: Change
reqs can be sent up to 6h prior” will be satisfied, since there
the said goal is related to these two quality constraints via
conflict nodes.
S-Net. The purpose of an s-net is to represent the compar-
ison of solutions identified via simulation. If we perform
simulations on the r-net in Figure 1, we will observe that
some softgoals are not satisficed at all: e.g., “s: Accommo-
3

q: Change reqs can be sent up to 3h prior
g: Send location on
an interactive map
Figure 2. An s-net.
date many change requests” has no incoming lines at all, so
that its satisfaction is unknown. This absence of informa-
tion is not an uncommon situation, for an r-net is built itera-
tively. In order to accommodate incompleteness and incon-
sistency, we have four truth values in the Techne language:
the usual T and F, for true (satisfied) and false (not satis-
fied) respectively, U for unknown, and D for disputed (i.e.,
some evidence concludes the satisfaction, some the denial
of the node). We can still compare quasi-solutions in Figure
1 in an s-net. Suppose that we consider two quasi-solutions,
say (K1;T1) and (K2;T2), from those in Figure 1, both in-
volving automated scheduling. Suppose further that there
are two differences between these two quasi-solutions: one
is that (K2;T2) satisfies the quality constraint “q: Change
reqs can be sent up to 3h prior” and the (K1;T1) instead
satisfies “q: Change reqs can be sent up to 6h prior”, while
the other difference is that the (K1;T1) satisfies the op-
tional goal “g: Send location on an interactive map” and
(K2;T2) does not satisfy that optional goal. The s-net that
compares these two quasi-solutions is shown in Figure 2. A
node in an s-net is a (quasi-)solution. A link goes from
a solution A to another solution B iff either (i) A satis-
fies some optional node that B does not (in this case, the
link is labeled with that optional node), or (ii) A satisfies a
node, which is preferred to another node that B satisfies (in
this case, the link is labeled with that preferred node). An
s-net thereby summarizes the information relevant for the
comparison of an (quasi-)solutions. Note that an s-net does
not answer the question of which (quasi-)solution to choose
among those available; instead, an s-net acts as a decision
aid. In this sense, we see from Figure 2 that (K1;T1) is
a “better” quasi-solution than (K2;T2) over one criterion
(i.e., the quality constraint “q: Change reqs can be sent up
to 3h prior”), while (K2;T2) is better than (K1;T1) over
another criterion (i.e., the optional goal “g: Send location on
an interactive map”). Which one will be chosen depends on
the decision rule applied in a particular s-net; decision rules
are not in the scope of Techne.
3 Language
Techne has two parts. The first part is Techne logic (TL),
and is defined on a particular kind of r-nets, called attitude-
free r-nets, and serves for the representation and identifica-
tion (but not comparison) of solutions (cf., x3.1). The sec-
ond part augments TL, in the sense that it enables reasoning
about how theories of TL compare over some specific crite-
ria (cf., x3.2).
3.1 Techne Logic
Let p; q; r; s, indexed or primed when necessary, denote
propositions, whereby a proposition is (as usual) a share-
able content of beliefs, desires, or intentions, and the pri-
mary bearer of truth and falsity [10]. To remain general, we
make no assumption on the formalism, in which a proposi-
tion is expressed: it is thereby unimportant if the proposi-
tion is in natural language, or is a well-formed formula with
no free variables in some logic. A proposition p alone is not
very interesting for the engineer, for it does not say whether
the condition it describes is desired, believed, or otherwise,
that is, if p is a goal, quality constraint, or otherwise. The
elicitation of requirements provides a set of propositions P
about the system-to-be and its relevant environment. The
core ontology [5] provides a pragmatic characterization of
the propositions: e.g., if p is believed by the stakeholders,
then it is an instance of the domain assumption concept.
The idea in Techne is to set each proposition p 2 P as a
node in a graph, called requirements net, or r-net, whereby
the pragmatic characterization is captured by assigning la-
bels to the propositions/nodes. An r-net is a directed labeled
graph, in which any two nodes can be connected by at most
one link. Each proposition consequently carries one of the
labels shown in the legend in Figure 1, whereby a label is
intended to symbolize the concept or relationship that the
given node instantiates.
We can obtain from any r-net R, the attitude-free r-net
R by removing all preference and optionality nodes, along
with all links of R connected to these preference and op-
tionality nodes. An R thereby carries no information that
allows the comparison of solutions, but still allows us to
represent the instances of all concepts of the core ontology,
along with the inference and conflict relationships between
these instances.
The purpose of TL is to provide formal semantics to the
nodes and links in attitude-free r-nets. We can otherwise
perform no meaningful simulation on attitude-free r-nets in
the aim of identifying solutions. To achieve this aim, the
first step amounts to map the syntactic atoms of attitude-free
r-nets to a symbolic syntax, which has standard negation
and conjunction connectives, from which we define disjunc-
tion and material implication as abbreviations in the usual
way. We can subsequently provide formal semantics (i.e.,
truth values) to well-formed formulas in TL in a standard
way, and compute truth values via truth tables. Since we
are not interested only in truth and falsity as usual, but also
wish to accommodate incomplete information and incon-
sistency (cf., x2), we will have four possible truth values:
fT;F;D;Ug.
Syntax of R. We distinguish three kinds of syntax for
4

attitude-free r-nets. The visual syntax is the syntax used to
draw Techne models, such as the one shown in Figure 1;
its syntactic elements are graphical primitives (circles, tri-
angles, and lines with arrows) and letters used to label these
primitives. In the graph syntax, and for a set of proposi-
tions P , any instance of a concept of the core ontology is
written x(p) (with p 2 P ), where x 2 fk; t; g;q; sg are sym-
bols for, respectively, an instance of the domain assump-
tion, task, goal, quality constraint, and softgoal concepts.
The relationship nodes written in graph syntax make ex-
plicit the nodes that they relate. E.g., the domain assump-
tion k(q) = “the conjunction of goals g(p1); : : : ; g(pn) re-
fines the goal g(p)” gives an inference node, which we write
I(q; fg(p1); : : : ; g(pn)g; g(p)). E.g., the domain assump-
tion k(q) = “the conjunction of goals g(p1); : : : ; g(pn)
is in conflict with the goal g(p)” gives a conflict node
C(q; fg(p1); : : : ; g(pn)g; g(p)). Finally, we have the sym-
bolic syntax, which rewrites the visual and graph expres-
sions as well-formed formulas of a propositional logic.
Each of the first three columns in Table 1 provides the
rules for generating valid expressions in each kind of syn-
tax, and the correspondence between the elements of each
kind of syntax. Valid expressions are generated inductively
as usual, starting in each column from the first and moving
to the last row.
An R obeys a set of syntactic constraints, which are ap-
parent from the inductive definition of (any of the three
kinds of) syntax in Table 1. E.g., we cannot have a line
between two instances of concepts (i.e., two nodes taking
labels from the set fk; t; g;q; sg). This is due to the need
to make explicit the relationship between the instances of
concepts, so that in a connected R, we need to have at least
an inference or conflict node to relate nodes that represent
instances of concepts.
Two observations are in order regarding the move from
visual/graph to symbolic syntax. (1) An inference node is
rewritten as the implication of the conclusion node from the
conjunction of the premise nodes, while the conflict node
amounts to the implication of a negation from the conjunc-
tion of the attacking nodes. Relying on material impli-
cation is not the best choice for Techne, but is the only
choice that would not violate the space constraints on the
present discussion. Material implication suffers from well-
known paradoxes, and is to be replaced in a future variant
of Techne. (2) Several inference nodes that have the same
conclusion are considered as alternatives, and are placed in
disjunction. The the rationale is that any, some, or all of the
implications and their assumptions (i.e., x is called an as-
sumption in x ! y) need to verify to reach the conclusion.
If there are several conflict nodes that attack the same node,
these nodes are also related via disjunction. Again, the ra-
tionale is that any of the conflict nodes and their premises
need to hold for the target to be negated.
:
D D
T F
F T
U U
(a) Negation.
^ D T F U
D D D F F
T D T F U
F F F F F
U F U F U
(b) Conjunction.
T
>
>
>
U



>
>
>
Dvt
OO
F



(c) Lattice.
Figure 3. Truth tables and the lattice.
Semantics of R. The syntactic elements of the sym-
bolic syntax obtain semantics through Techne structures. A
Techne structure is a tuple (T ;D), where T maps a syntac-
tic element to a truth value. The codomain of T includes
four truth values taken from Belnap’s four valued logic [1]:
T, F, D, and U correspond to, respectively known-only-
true, known-only-false, known-both-true-and-false, and un-
known truth values. D maps a syntactic element to an in-
stance of a concept or relationship of Techne (cf., x2; the
codomain includes all possible instances of all concepts
(i.e., domain assumption, task, goal, quality constraint,
softgoal) and relationships (i.e., inference and conflict)
that we wish to represent in attitude-free r-nets. Entailment
in Techne, denoted j=T is defined inductively via Techne
structures in the last column of Table 1.
We define truth tables for negation (cf., Figure 3(a)) and
conjunction (cf., Figure 3(b)) via the lattice in Figure 3(c).
That it is a lattice means that it is a partial order vt, for
which a unique greatest lower bound (meet) and least upper
bound (join), denoted respectively x ut y and x tt y, exist
for each pair (x; y) of members of the ordered set of truth
values. The lattice shown in Figure 3(c) is complete, mean-
ing that it includes a meet and join for any subset of truth
values (cf., e.g., [4]). Intuitively, the lattice in Figure 3(c)
indicates the direction, in which truth “increases” (from bot-
tom to top in Figure 3(c)). The four truth values “increase”
from F, over U and D, to T. The truth tables for conjunction
and disjunction follow immediately from the order defined
via vt, by taking that meet ut stands for conjunction ^ and
join tt for disjunction _.
This leads us the notion of semantic entailment of a well-
formed formula from another well-formed formula in TL;
or, by equivalence of syntactic elements (cf., Table 1), the
semantic entailment of a subgraph of an attitude-free r-net
from another subgraph of the attitude-free r-net.
Definition 3.1. R-(Sub)Net Entailment. Let and 0 be
two well-formed formulas in TL. We say that entails 0,
and write j=T 0, iff for all Techne structures (T ;D), we
have T ( ) vt T ( 0).
Semantic entailment in TL corresponds to semantic en-
tailment in Belnap’s four valued logic. While TL takes truth
values and truth tables from Belnap’s logic, it remains orig-
inal in the definition of syntax and Techne structures, and in
the mapping from the syntactic elements to the instances of
the concepts and relationships of the core ontology.
5

Table 1. Visual, graph, and symbolic syntax, and the semantics of attitude-free r-nets in Techne.
Visual
syntax:
Well-formed subgraph in graph
syntax:
Well-formed formula in symbolic
syntax:
Semantics:
k p k(p), i.e., a domain assumption
node;
k(p) (T ;D) j=T k(p) iff T (k(p)) = T and D(k(p)) is an in-
stance of the domain assumption concept;
t p t(p), i.e., a task node; t(p) (T ;D) j=T t(p) iff T (t(p)) = T and D(t(p)) is an instance
of the task concept;
g p g(p), i.e., a goal node; g(p) (T ;D) j=T g(p) iff T (g(p)) = T andD(g(p)) is an instance
of the goal concept;
q p q(p), i.e., a quality constraint node; q(p) (T ;D) j=T q(p) iff T (q(p)) = T and D(q(p)) is an in-
stance of the quality assumption concept;
s p s(p), i.e., a softgoal node; s(p) (T ;D) j=T s(p) iff T (s(p)) = T and D(s(p)) is an instance
of the softgoal concept;
... I
... ... I(p; f i j 1  i  m 1g; m),
i.e., an inference node;
(
V
1im1 i)! m (T ;D) j=T (
V
1im1 i) ! m iff
T ((
V
1im1 i) ! m) = T and
D((
V
1im1 i) ! m) is an instance of the in-
ference rule relationship;
... C
... ... C(p; f i j 1  i  m1g; m),
i.e., a conflict node;
(
V
1im1 i)! : m (T ;D) j=T (
V
1im1 i) ! : m iff
T ((
V
1im1 i) ! : m) = T and
D((
V
1im1 i) ! : m) is an instance of the
conflict rule relationship;
... I
... ...
...
... ...
I
fI(pj ; f i;j j 1  i  mg; ) j
2  j  ng, i.e., a set of inference
nodes concluding the same node;
W
2jn((
V
1im i;j)! ) (T ;D) j=T
W
2jn((
V
1im i;j) ! ) iff
T (
W
2jn((
V
1im i;j) ! )) = T and for each
2  j  n, D((
V
1im i;j) ! ) is an instance of
the inference rule relationship;
... C
... ...
...
... ...
C
fC(pj ; f i;j j 1  i  mg; ) j
2  j  ng, i.e., a set of conflict
nodes attacking the same node;
W
2jn((
V
1im i;j)! : ) (T ;D) j=T
W
2jn((
V
1im i;j) ! : ) iff
T (
W
2jn((
V
1im i;j) ! : )) = T and for each
2  j  n,D((
V
1im i;j)! : ) is an instance of the
conflict rule relationship;
f i j 1  i  mg, i.e., a set of
well-formed subgraphs;
V
1im i (T ;D) j=T
V
1im i iff T (
V
1im i) = T and for
each 1  i  m, D( i) is an instance of a concept deter-
mined according to the rules above;
The following also apply: (T ;D) j=T i ^ j iff (T ;D) j=T i and (T ;D) j=T j ;
(T ;D) j=T : iff (T ;D) 6j=T ;
j ! j abbreviates : i _ j ; and j _ j abbreviates :(: i ^ : j).
3.2 Comparison of Solutions
Comparing solutions requires a precise characterization
of what a solution is in an attitude-free r-net R in TL,
and how preference and optionality relate solutions in an
r-net R. To define the solution concept, we use particu-
lar kinds of subgraphs of R or R. Namely, a G-subnet
G = (V (G); L(G)) is a subgraph of an r-net R, i.e.,
V (G)  V (R) and L(G)  L(R), such that: (1) V (G)
partitions onto (a) the set of all goals from R, and (b) the
set of all domain assumptions from R, each of which re-
lates at least one goal to at least another goal in R; and (2)
L(G) contains all links from R that connect in R any two
members of V (G). With this in mind, it is straightforward
to define K-, T-, Q-, and S-subnets, so that we omit these
definitions. The purpose of each of these subnets is to group
all instances of specific concepts within a single graph. This
leads us to the definition of the solution concept.
Definition 3.2. Solution. In Techne, (Ki;Ti;G;Q) is a so-
lution of the requirements problem iff:
1. Gc and Qc are subnets of, resp., G and Q; and
2. Ki;Ti j=T G;Q.
Observe that a solution is by definition a subnet of an
attitude-free r-net R, and a subnet of the corresponding r-net
R. Also, a solution is by definition an admissible solution,
that is, one satisfying all the conditions that must be satis-
fied if the stakeholders are not to reject that solution. For
our meeting scheduler requirements problem, a way to read
some solution (Ki;Ti;G;Q) is that K indicates assump-
tions about the conditions, in which the system-to-be oper-
ates (e.g., all participants use email), T indicates what the
system-to-be does within/to its environment (e.g., calendar
6

constraints are requested via email), G highlights the stake-
holders’ goals that it satisfies (e.g., meeting is scheduled),
and Q qualifies the goal-satisfying behavior of the system-
to-be (e.g., late change requests can be accommodated).
Suppose now that we have identified n solutions:
(K1;T1;G;Q); : : : ; (Kn;Tn;G;Q). These solutions differ
in terms of how many of the optional goals and optional
quality constraints they satisfy, and how the goals and qual-
ity constraints they satisfy relate to one another in terms of
preference. Different Techne structures satisfy different so-
lutions. We therefore need means to compare Techne struc-
tures, and thereby solutions, which leads to the notion of
substructure in Techne.
Definition 3.3. Substructure. Let (T ;D) and (T 0;D) be
two Techne structures for an attitude-free r-net R. We say
that (T 0;D) is a substructure of (T ;D) in , and write
(T 0;D) <T (T ;D)
iff (i) T and T 0 have the same domain, (ii) all syntactic
elements of R except  obtain the same truth value from
both T and T 0, and (iii) T 0() @t T (). 1
The substructure concept allows us to define what it means
for a solution to be strictly more desirable than another one.
Definition 3.4. Better Solution. Let (Ki;Ti;G;Q) and
(Kj ;Tj ;G;Q), with i 6= j, be two solutions. We say that
the solution (Ki;Ti;G;Q) is strictly more desirable than
(Kj ;Tj ;G;Q) in , and write
(Kj ;Tj ;G;Q) T (Ki;Ti;G;Q)
iff for any two Techne structures (T ;D) and (T 0;D) such
that (T ;D) j=T Ki;Ti and (T 0;D) j=T Kj ;Tj , either of
the two conditions below holds:
1. (T 0;D) <T (T ;D);
2. there is a strict preference (e.g., P(q; ; 0)) in R for 
over 0, T 0() @t T () and T (0) @t T 0(0).
The first condition in Definition 3.4 will verify when an
(compulsory or optional)  obtains a “higher” truth value
(in terms of the lattice of truth values – cf., Figure 3(c)) in
the Techne structures of the solution (Ki;Ti;G;Q) com-
pared to the truth value it obtains in the Techne structures
of the solution (Kj ;Tj ;G;Q). Comparison in terms of op-
tionality will thus be performed through the first condition.
The second condition in Definition 3.4 allows us to per-
form comparisons in terms of preferences. That condition
tells us to strictly prefer that of the two solutions, which
assigns a “higher” truth value to the preferred syntactic ele-
ment (above, ) and a lower truth value to the less preferred
1T 0() @t T () is abbreviation for “T 0() vt T () and not T () vt
T 0()”.
syntactic element (above, 0), whereby vt orders the truth
values according to the lattice (cf., Figure 3(c)). E.g., it fol-
lows then that we will strictly prefer a solution that assigns
T to  and F to 0 to another solution that does the reverse;
also, we will strictly prefer a solution that assigns U to  and
F to 0, to the one that assigns F to  and T to 0.
The relation T is specific to , which makes  a crite-
rion of comparison. To say that a solution is better than
another one is specific to a chosen criterion. Solutions
are consequently compared using a family of irreflexive
binary relations (Tc )c2C, where C is the set of criteria.
The criteria are by definition elicited, since they are cap-
tured in an r-net. Members of C may be optional elements,
and individual elements, which are subject to preferences.
Some of these elements are obtained by the approxima-
tion of softgoals, so that criteria contain proxies for soft-
goals. Solutions can compare on potentially many dimen-
sions, the number of which is jCj. E.g., while we may have
(Kj ;Tj ;G;Q) Tg(p1) (Ki;Ti;G;Q), we could also have
(Ki;Ti;G;Q) Tg(p2) (Kj ;Tj ;G;Q). g(p2) and g(p2) may
be incomparable in terms of preference (i.e., it is not mean-
ingful to give a preference between them), so that Techne
does not give a general rule as to which of the two solutions
to choose. It will be up to the stakeholders and the engineer
to choose one of the two.
To facilitate the comparison of solutions, Techne uses
solution nets. An s-net is a directed labeled graph, in which
each node is a solution. Each criterion c from (Tc )c2C is
the member of the set of labels of links in an s-net. If we
have only two solutions, such that (Kj ;Tj ;G;Q) Tg(p1)
(Ki;Ti;G;Q) and (Ki;Ti;G;Q) Tg(p2) (Kj ;Tj ;G;Q),
then the corresponding s-net will have two nodes, one for
each solution, and two links, one labeled g(p1) that runs
from (Ki;Ti;G;Q) to (Kj ;Tj ;G;Q), while the other link
will be labeled g(p2), and will run from (Kj ;Tj ;G;Q) to
(Ki;Ti;G;Q). An s-net for the meeting scheduler problem
is shown in Figure 2.
4 Reasoning on Techne Models
Simulation amounts to hypothesize the execution of a
subnet of the T-subnet in an attitude-free r-net, then deter-
mine the effects of the hypothetical executions on the truth
value of goals, quality constraints, and so on. Simulation
is used to determine if some given tuple (Ki;Ti;G;Q) is a
solution. Simulation is performed on an attitude-free r-net
R and a tuple (Ki;Ti;G;Q), such that each of the subnets
in the tuple is a subnet of R.
For the simulation of (Ki;Ti;G;Q) in R, the first step
is to make two assumptions: (1) 8 2 Ki; T () = T, and
(2) 8 2 Ti; T () = T. The second step is to compute
the truth values of the other syntactic elements of R other
than Ki and Ti. This amounts to calling EVALUATE( R; r),
where r is composed exactly of the subnets Ki and Ti.
7

Given the truth values for a subnet r of an attitude-free
r-net R, we define below the algorithm EVALUATE, which
computes the truth values of the syntactic elements of R that
are not in r. Starting from the nodes in r, the algorithm tra-
verses R and computes the truth values of the visited nodes.
For a given node p 2 V ( R), the NODELABEL procedure
computes the truth value of p by applying the truth tables
on the truth values propagated to p over the links that end in
p. We discuss the NODELABEL procedure first (cf., x4.1),
and then EVALUATE (cf., x4.2).
4.1 Node Labeling
NODELABEL uses the functions val, deleteDuplicates, and
concl. val maps a node either to a truth value, or the value
N . val(v 2 V ( R)) returns N iff v was not already pro-
cessed by NODELABEL, or if v =2 V (r) (i.e., its truth value
was not assumed at the outset); otherwise, val(v) returns
the truth value returned previously by NODELABEL, or the
truth value assumed at the outset for v.
The function deleteDuplicates returns, for a given col-
lection, the set of all distinct elements in the collection.
The function concl takes a pair of truth values, and re-
turns a set (potentially a singleton) of truth values. concl is
defined over the truth table for implication and returns the
possible truth values for the conclusion of an implication.2
Say that we have an implication x ! y, and that we know
the truth value val(x) of x and the truth value val(x ! y)
of the implication x ! y. concl(val(x); val(x ! y)) re-
turns the truth values of y that are allowed by the truth table
for implication: there we will have, val(x) is a row head,
val(x ! y)) is in at least one cell of the row of val(x), so
that concl(val(x); val(x! y)) is at least one of the column
heads. E.g., concl(U;T) = fD;Tg; concl(T;F) = fTg.
The functions ut and tt return, respectively the meet
and join for a given set of truth values, according to the
truth ordering defined by vt in Figure 3(c).
The procedure NODELABEL involves the collect and se-
lect steps.
Collect. The for each loop performs the collection of
truth values, from which one will be subsequently selected.
For a given node v 2 V ( R), the for each loop considers
each node w 6= v; w 2 V ( R) such that there is a line
wv 2 L( R), fromw to v. Ifw is an inference node that con-
cludes v, i.e., w = I(
; Y;X) and v 2 X , we need to distin-
guish two cases: (i) if we do not know the truth value val(w)
of w, then we assume that the truth value of w is U and
add U to the collection DI; (ii) if we know the truth value
val(w), then concl(val(
V
2Y ); val(w)) gives the set of
truth values for the implication w, and we cautiously take
the meet of that set, i.e., utconcl(val(
V
2Y ); val(w)),
2It is straightforward to build the truth table for implication from the
Table 1 and Figure 3.
Algorithm 1 Node Labeling
Input: An attitude-free r-net R and a node v 2 V ( R);
Output: Exactly one of the members of T = fT;T;F;D;Ug;
1: procedure NODELABEL( R; v)
Collect values:
2: Empty the collections DI and DC
3: Empty the sets DuI and D
u
C
4: for each w 2 V ( R) s.t. 9wv 2 L( R) do
5: if w = I(
; Y;X), v 2 X , val(w) = N then
6: Add U to DI
7: else if w = I(
; Y;X), v 2 X , val(w) 6= N then
8: Add utconcl(val(
V
2Y ); val(w)) to DI
9: else if w = C(
; Y;X), v 2 X , val(w) = N then
10: Add U to DC
11: else if w = C(
; Y;X), v 2 X , val(w) 6= N then
12: Add :(utconcl(val(
V
2Y ); val(w))) to DC
13: end if
14: end for
Select a value:
15: DuI deleteDuplicates(DI)
16: DuC deleteDuplicates(DC)
17: if DuI [D
u
C = ; then
18: if val(v) 6= N then
19: Return val(v) and stop.
20: else
21: Return U and stop.
22: end if
23: else
24: Return utfttDuI ;utD
u
Cg and stop.
25: end if
26: end procedure
according to the truth-partial ordering vt of the truth lat-
tice, and add this to the collection DI. The collection DI
obtains the truth values resulting from all w that are infer-
ence nodes and conclude v. This same rationale applies
if w = C(
; Y;X) and v 2 X . We also distinguish two
cases: (i) if we do not know the truth value val(w) of w,
then we assume that the truth value of w is U and add U to
the collection DC; (ii) if we know the truth value val(w),
then concl(val(
V
2Y ); val(w)) gives the set of truth val-
ues for the implication w, and we cautiously take the meet
of that set, i.e., utconcl(val(
V
2Y ); val(w)), and add its
negation to the collection DC. The collection DC obtains
the truth values resulting from all w that are conflict nodes
and attack v.
Select. The deleteDuplicates function is used to produce
two sets: the sets DuI and D
u
C carry all distinct truth values
from, respectively, DI and DC. We then distinguish two
cases. If DuI [ D
u
C is empty, then there are no inference
nodes that conclude v and no conflict nodes that attack v.
We therefore check if v already has a truth value (which
happens if its truth value was assumed at the outset of the
reasoning procedure): (i) if it does have a truth value, then
this truth value is kept; (ii) if it does not have a truth value,
we assign U to it. Instead, if DuI [ D
u
C is not empty, we
compute the joins of, respectively DuI and D
u
C, and return
the meet of these two.
8

TT
D
T
F
T
T
T
T
T
(a) What is the truth value of g(r)?
T
T
T U
T
D
(b)
Scheduling is
automated
Send
invitations
by email
Send
confirmation
by email
Use standard
email application
g
I
g
g
t I
I
All participants
use email
Have all
participants’
emails
k
k
... ...
...
T
T
T
T
T
T
T
U
U
(c)
Figure 4. Illustration of node labeling and evaluation.
For illustration, and to see why we return the meet of the
join of DuI and of the meet of D
u
C, consider the hypothetical
attitude-free r-net written using graph syntax in Figure 4(a).
The following are the computations performed by the pro-
cedure NODELABEL to determine the truth value of g(r) in
Figure 4(a):
 concl(val(g(p1) ^ s(p2)); val(I(q1; fg(p1); s(p2)g; g(r)))) =
concl(T;T) = fTg;
 concl(val(g(p3) ^ g(p4)); val(C(q2; fg(p3); g(p4)g; g(r)))) =
concl(D;T) = fT;Ug;
 concl(val(g(p5); val(I(q3; g(p5); g(r)))) = concl(F;T) =
fD;T;F;U;Tg;
 concl(val(g(p6); val(C(q4; g(p6); g(r)))) = concl(T;T) = fTg;
 utfTg = T; :(utfT;Ug) = U; utfD;T;F;U;Tg = F;
 :(utfTg) = F;
 DI = (T;F); DC = (U;F); DuI = fT;Fg; D
u
C = fU;Fg;
 utfttDuI ;utD
u
Cg = utfT;Fg = F;
 The truth value of g(r) is F.
Proposition 4.1. Procedure NODELABEL applied to a
node v of a finite attitude-free r-net R (i) does not loop in-
definetly, (ii) returns the truth value for v that is not dif-
ferent from a truth value that the truth tables allow us to
compute for v, given the syntactic translation rules and the
semantics in Table 1, and (iii) has the worst running time
in O(4!(inDegree( R; v) + 2)), where inDegree( R; v) is the
number of links in R that end in v.
Proof. Cf., Appendix A.
4.2 Evaluation
We start from an attitude-free r-net R and its subnet r.
We assume a truth value for each node in V (r). The aim
is to determine the truth values of all nodes in V ( R). If
we assume that R is acyclical, doing this is straightforward,
and formalized in Algorithm 2.3 It is not difficult to see that
3The presence of cycles gives rise to nontrivial complications. Two
such complications are the possibility for truth values to be unstable, and
potential absence of unique truth values. The identification of stable and
unique truth values increases the complexity of the evaluation algorithm.
We leave the treatment of cyclical attitude-free r-nets for future work.
Algorithm 2 Evaluation
Input: An attitude-free r-net R, a subnet r thereof, and a truth value for
each node in the subnet r;
Output: For each node in V ( R), one truth value from fT;F;D;Ug;
1: procedure EVALUATE( R; r)
2: Empty the queue Q
3: Add all nodes in V (r) to the queue Q
4: for each v in Q do
5: for each w 2 V ( R) s.t. 9vw 2 L( R) do
6: NODELABEL( R;w)
7: Add w to Q
8: end for
9: Delete v from Q
10: end for
11: for each v 2 V ( R) s.t. val(v) = N do
12: Assign U to v
13: end for
14: end procedure
Algorithm 2 equates to a breadth first search (e.g., [6]), that
is launched from each node in r and traverses the graph over
all outgoing links of a node. The second outer for each loop
assigns the U truth value to all nodes that were not traversed
by the first outer for each loop: any such vertex v has an
unknown truth value, i.e., (v) = N .
Proposition 4.2. Procedure EVALUATE applied to a sub-
net r of a finite and acyclic attitude-free r-net R (i) does
not loop indefinetly, (ii) for each node v 2 V ( R), re-
turns the truth value for v that is not different from a truth
value that the truth tables allow us to compute for v, given
the syntactic translation rules and the semantics in Table
1, and (iii) has the upper bound on the running time in
O(Pr(jV (r)j + jL( R)j)), where Pr is the number of sim-
ple paths in V ( R) such that each of these paths starts in a
node of r.
Proof. Cf., Appendix B.
We take two examples for illustration. Consider first the
attitude-free r-net in Figure 4(b). Suppose that T is as-
signed at the outset to both t(p1) and I(p2; t(p1); g(p3)).
Since I(p2; t(p1); g(p3)) is true, we know that the implica-
tion t(p1) ! g(p3) is true. To determine the truth value of
9

g(p3), we consult the truth table for implication, and con-
clude that g(p3) receives the truth value T. Since we lack
information already to compute the truth value of g(p4), we
assume that its truth value is U. By using the translation
rules on I(p5; fg(p3); g(p4); g(p5)g), we have the implica-
tion (g(p3) ^ g(p4)) ! g(p5). Since g(p3) is T and g(p4)
is U, the conjunction g(p3) ^ g(p4) is U. We assumed at
the outset that the implication (g(p3) ^ g(p4)) ! g(p5) is
T. With this in mind and from the truth table for implica-
tion, we see that g(p5) can be any of fD;Tg. We take the
meet of this set, utfD;Tg, which is D according to the lat-
tice in Figure 3(c). In the second example, shown in Figure
4(c) we have assumed the truth of the task, two domain as-
sumptions, and two inferences on the left-hand side of the
figure. This led us to label T the goals “g: Send invitations
by email” and “g: Send confirmation by email”. Without
making additional assumptions, we can only conclude U on
the inference that concludes the goal “g: Scheduling is au-
tomated”, and subsequently U on that same goal.
5 Conclusions and Future Work
We have proposed a novel requirements modeling lan-
guage called Techne, summarized its logical semantics and
presented basic algorithm for reasoning with Techne mod-
els. These models (r-nets) are directed labeled graphs with
many-sorted nodes, some of which represent propositions
such as goals, quality constraints, softgoals, tasks, while
other propositions represent background knowledge, pref-
erences and other logical relationships. These nodes are
connected by simple edges, so that all aspects of the require-
ments are reified. A requirements problem is defined by an
r-net along with information as to whether its goal/quality
elements are mandatory (“must-have” requirements) or op-
tional (“nice-to-have”). The semantics of Techne define so-
lutions to a given requirements problem as a set of tasks
and quality constraints which together satisfy all mandatory
requirements and do as well as possible with respect to op-
tional ones and preferences. In general, a given require-
ments problem will admit many such solutions, incompara-
ble to each other.
Techne constitutes a significant departure from require-
ments modeling languages in the family of KAOS and i*
in a number of directions. First, the language is proposi-
tional, i.e., its primitive units are propositions, rather than
offering an ontology of actors, actions, entities/relationships
and the like. Second, the language takes a clear stand as
to what constitutes a solution to a requirements problem.
This has been an open issue with requirements languages
that used softgoals and qualitative contributions from one
requirement to another (whereby fulfillment of one require-
ment helps/hurts fulfillment of another). Indeed, Techne
replaces such partial contributions with the notions of op-
tional requirements, preferences and optimal fulfillment: an
admissible solution A is better than another B if it does bet-
ter with respect to optional requirements and preferences
(but both must satisfy mandatory ones). This means that in
Techne, a requirements problem constitutes an optimization
problem, rather than a satisfaction (or “satisficing”) one.
Finally, Techne treats softgoals as first-class citizens along
with goals, rather than as secondary criteria useful for com-
paring alternative solutions to goals.
The notion of optional requirements and preferences was
inspired by earlier results in Knowledge Representation [2].
Liaskos [8] has already adopted such results to propose an
expressive language for representing preferences within a
goal-oriented framework. Techne is less expressive, com-
putationally more tractable, and also offers a more seamless
integration of requirements concepts included in the core
ontology into a coherent modeling language.
Much remains to be done in turning Techne into a use-
ful tool for requirements engineers. Firstly, we will extend
the modeling framework to support social concepts, as pro-
vided in i*. Secondly, we have come to appreciate the im-
portance of contextual modeling, where, for instance, the
requirements for a given sales system may be different de-
pending on the type of customer or the size of the sale.
Lapouchnian and Mylopoulos [7] make a proposal which
we intend to incorporate in future versions of Techne. Fi-
nally, the reader may have noticed that there is no sublan-
guage within Techne for expressing quality constraints. We
actually envision Techne being augmented with such a sub-
language that allow one to express quality constraints on the
development process, run-time performance of the system-
to-be, design artifacts (e.g., architecture) and more. We see
such an extension as being defined by a collection of classes
and associations (the things that can be talked about) along
with a logical language in the family of OCL where one can
express constraints such as “At least 95% of all sales pro-
cess instances are completed”, or “the development process
will last at most 6 months”.
A Proof of Proposition 4.1
Proof. (i) Termination. We first prove that NODELABEL
applied to a node v of a finite attitude-free r-net R (i) does
not loop indefinetly. The for each loop considers once each
node w 6= v such that there is a link wv 2 L( R), from
w to v. Since R is finite, the for each loop always termi-
nates. As the number of links ending in v is finite, so will
be the size of DI and DC, and consequently of DuI and D
u
C .
NODELABEL therefore never loops indefinetly for a finite
R.
(ii) Correctness. We prove that NODELABEL applied to a
node v of a finite attitude-free r-net R (ii) returns the truth
value for v that is not different from a truth value that the
truth tables allow us to compute for v, given the syntactic
10

translation rules and the semantics in Table 1. To prove
this, it is enough to prove that NODELABEL computes the
truth value of a node v by (A) taking into account all im-
plications that conclude that node, (B) using truth tables of
Techne to compute the truth of the conclusion of each impli-
cation, and (C) using translation rules from Table 1 to write
the implications that it uses when computing the truth value
of the conclusion of each implication. Proposition (A) is ev-
ident from the for each loop, which will traverse all nodes
w such that there is a line wv 2 L( R), and thereby all in-
ference and conflict nodes that, respectively, conclude and
attack a given node v. Proposition (B) follows immediately
from the definition of the functions val and concl, called in
NODELABEL. That Proposition (C) is true can be seen from
the if block in the for each loop, the way that NODELABEL
uses the collections DI and DC and the sets DuI and D
u
C .
(iii) Complexity. Let F = fT;F;D;Ug. We finally prove
that NODELABEL applied to a node v of a finite attitude-
free r-net R (iii) has the worst running time in O((jFj
1)!(inDegree( R; v)+2)), where inDegree( R; v) is the num-
ber of links in R that end in v. The for each loop consid-
ers exactly once each node w 6= v such that there is a link
wv 2 L( R). We assume that evaluating
V
2Y is triv-
ial. In the worst case, concl(val(
V
2Y ); val(w)) = T,
and so for each considered w. Consequently, the for each
loop runs in O(inDegree( R; v)(jFj 1)!). Computing the
meet (or join) for T takes (jTj 1)! since the meet (and
join) is defined via a partial order, which is by definition
reflexive, transitive, and anti-symmetric. The selection step
involves the deletion of duplicates in DI, DC, and C, and
the computation of the join for DuI , the meet for D
u
C , and
of the meet of fttDuI ;utD
u
Cg. Assuming that the dele-
tion of duplicates is trivial, computing utfttDuI ;utD
u
Cg
takes 2((jTj 1)!) in the worst case, when DuI = D
u
C =
T. It follows that NODELABEL has the worst running
time in O(inDegree( R; v)(jFj 1)! + 2(jFj 1)!), that is,
O((jFj 1)!(inDegree( R; v) + 2)) when applied to a node
v of a finite R.
B Proof of Proposition 4.2
Proof. (i) Termination. We first prove that EVALUATE ap-
plied to a subnet r of a finite and acyclic attitude-free r-net R
(i) does not loop indefinetly. Since R is acyclic, the number
of times a node will be traversed by the first outer for each
loop equals the number of simple paths from each member
of V (r). The number of simple paths in a finite acyclic di-
rected graph is finite, so that each node will be traversed a
finite number of times. At every traversal of a node, that
node is removed from Q, so that Q will ultimately empty
and the first outer for each loop will terminate. The sec-
ond outer for each loop considers at most all nodes exactly
once, so that it terminates as well. It follows that EVAL-
UATE will never loop indefinetly for an acyclic and finite
R.
(ii) Correctness. The first outer for each loop calls
NODELABEL on each node it traverses, and each time it
traverses that node. Observe that if there is a path from
each of some two members w1 and w2 of V (r) to a node v,
and there is no path from another node in V (r) to v, then
NODELABEL( R; v) will be called exactly twice. If the path
from w1 to v is longer than the path from w2 to v, then the
first NODELABEL( R; v) call will be made when the first
outer for each loop considers v along the shorter path. That
first call will provide a preliminary truth value for v. This
value is preliminary, since not all nodes on the loonger path
will have been evaluated when the loop reaches v along
the shorter path. The second NODELABEL( R; v) call will
provide the definite truth value. Correctness of EVALUATE
therefore depends on the correctness of NODELABEL. Fol-
lowing Proposition 4.1, EVALUATE is correct when applied
to an acyclic and finite R.
(iii) Complexity. It is straightforward to see that the number
of times a node v will enter the queue Q equals the total
number of simple paths to v from all members of V (r). The
upper bound on the running time is then in O(Pr(jV (r)j+
jL( R)j)), where Pr is the number of simple paths in V ( R)
such that each of these paths starts in a node of r.
References
[1] N. D. Belnap, Jr. A useful four-valued logic. In J. M. Dunn and
G. Epstein, editors, Modern Uses of Multiple-Valued Logic. D. Rei-
del Publishing Co., 1977.
[2] M. Bienvenu, C. Fritz, and S. A. McIlraith. Planning with qualitative
temporal preferences. In Knowl. Rep. and Reasoning, 2006.
[3] A. Dardenne, A. van Lamsweerde, and S. Fickas. Goal-directed re-
quirements acquisition. Sci. Comput. Program., 20(1-2):3–50, 1993.
[4] M. L. Ginsberg. Multivalued logics: a uniform approach to reasoning
in artificial intelligence. Comput. Intell., 4:265–316, 1988.
[5] I. J. Jureta, J. Mylopoulos, and S. Faulkner. Revisiting the core on-
tology and problem in requirements engineering. In 16th IEEE Int.
Requirements Engineering Conf., 2008.
[6] D. E. Knuth. The Art Of Computer Programming, volume 1. Boston:
Addison-Wesley, 3rd edition, 1997.
[7] A. Lapouchnian and J. Mylopoulos. Modelling domain variability
with contexts. Submitted for publication.
[8] S. Liaskos. Acquiring and Reasoning about Variability in Goal Mod-
els. PhD thesis, Dept. Comput. Sci., University of Toronto, 2008.
[9] D. A. Marca and C. L. McGowan. SADT: structured analysis and
design technique. McGraw-Hill, Inc., 1987.
[10] M. McGrath. Propositions. In Edward N. Zalta, editor, The Stanford
Encyclopedia of Philosophy. Fall 2008.
[11] E. Yu. Towards modeling and reasoning support for early require-
ments engineering. In Proceedings of the IEEE International Sym-
posium on Requirements Engineering, 1997.
[12] P. Zave and M. Jackson. Four dark corners of requirements engineer-
ing. ACM T. Softw. Eng. Methodol., 6(1):1–30, 1997.
11