=Paper=
{{Paper
|id=Vol-209/paper-2
|storemode=property
|title=Specifying the Collaborative Tagging System
|pdfUrl=https://ceur-ws.org/Vol-209/saaw06-full04-mesnage.pdf
|volume=Vol-209
|dblpUrl=https://dblp.org/rec/conf/semweb/MesnageJ06
}}
==Specifying the Collaborative Tagging System==
https://ceur-ws.org/Vol-209/saaw06-full04-mesnage.pdf
Specifying the Collaborative Tagging System ∗
Cédric Mesnage Mehdi Jazayeri
cedric.mesnage@lu.unisi.ch mehdi.jazayeri@lu.unisi.ch
Faculty of Informatics Faculty of Informatics
University of Lugano University of Lugano
Via G. Buffi 13 Via G. Buffi 13
6900 Lugano, Switzerland 6900 Lugano, Switzerland
The world is the totality of facts, not of things. is clearly not possible to formally specify the workings of the
(Ludwig Wittgenstein, [9], proposition 1.1) entire Internet. However, to be able to understand, explain,
and extend the behavior of aspects of any complex system,
we need a high-level precise description of those aspects. For
ABSTRACT a system as large and complex as the Internet, we should be
The collaborative tagging system is an interaction between able to build such a high-level description incrementally and
humans, terms and objects over time which results in a col- independently for different aspects. In this paper, we show
lectively organized knowledge. In this paper, based on the how this can be done for collaborative tagging, one of the
study of existing software systems, we present the specifica- emerging popular applications on the Internet.
tions of the collaborative tagging system written in TLA+.
Collaborative tagging [7] is an extension of the tagging ac-
tivity introduced in several popular websites such as Flickr
Keywords or del.icio.us. It has proven successful in these websites as
Collaborative Tagging, Specifications, TLA+, precise de- a way of sharing resources (i.e. photos, bookmarks).
scription
Collaborative tagging has also attracted the interest of re-
1. INTRODUCTION searchers [7] who are trying to understand the foundations of
To analyse emergent web applications scientifically, we need the activity, its current implementations, and possible role
precise abstract definitions of the fundamental elements in- in the collective intelligence idea. Collaborative tagging is
teracting in the systems in which these applications are suc- not merely a computer science problem in that it attempts
cessful. In this paper, we present the logic specifications to enable the collaboration of large numbers of humans in
of the abstractions interacting in the collaborative tagging collectively reviewing and structuring large amounts of infor-
system. mation with little restrictions imposed by the system. Many
contributions have been done lately[10, 6, 8, 1, 4]. We refer
Long-living software systems grow more complex over time. primarily to [1] and [4].
The behavior of such systems is not always well-understood
and is often a source of maintenance and extendibility prob- This paper has two primary goals: to show a precise de-
lems. The Internet, which started as a simple protocol (IP), scription (specification) of collaborative tagging, and to give
is now one of the more complex software systems ever as- an example of incremental derivation of specifications for
sembled, consisting of millions of components and applica- Internet-based services.
tions interacting with millions of users. New applications on
the Internet emerge regularly introducing new concepts and 1.1 Definitions
behaviors. These new concepts interact in sometimes unin- Since this paper is about precise descriptions, we start with
tended ways with other parts of the Internet making it ever a set of definitions in order to avoid misunderstanding on the
more difficult to understand the behavior of the Internet. It meaning of the main terms we use. Many of these definitions
∗This work is funded by the European Project can be found in the Oxford Dictionary. The glossary is given
“Nepomuk, the social semantic desktop”. in Figure 1.
http://www.semanticdesktop.org
To avoid ambiguity inherent in the use of the word “tag” as
both noun and verb, in this paper we use the word “tag” only
as a verb, that is, the actual act of tagging. For noun usage,
we use “term” to name the keyword used to tag. This avoids
confusion and enhances clearness of the specifications.
The collaborative tagging system is an interaction between
humans, terms and objects over time which results in a col-
lectively organized knowledge. In this paper we present and
explain specifications of this system. The next subsections of
this introduction describe briefly and informally this system
as seen in existing software and present the methodology we
choose to write the specifications. In order to facilitate the
Specification In [2] Michael Jackson claims that understanding of the specifications, we describe the abstrac-
tions involved in the collaborative tagging system specifica-
The terminology of software development is tion and first describe the collaborative tagging memory as
mostly in a chaos that correctly reflects the a module. We use model-checking to demonstrate the va-
chaotic state of the field. Usage of the word lidity of these specifications. Finally, we propose how our
specification is no exception. work can be extended in different directions.
(Michael Jackson, page 193)
But here we take as definition 1.2 The Collaborative Tagging System
The collaborative tagging system emerges from many new
A specification is a written description of software systems (i.e Del.icio.us, Flickr, Technorati, Con-
what a system is supposed to do. notea, CiteUlike, RawSugar...). It is a way of categorizing
(Leslie Lamport, [3], paragraph 4, page 1) knowledge by freely assigning sets of terms to objects (often
to web pages or bookmarks).
Collaborative produced or conducted by two or more par-
ties working together. A fundamentally new concept introduced by the new gener-
ation of Web applications such as collaborative tagging is to
Tagging attach a label to.
include and trust the user in further evolution of the system
System a set of connected things or parts forming a com- (and its associated information). In fact, anyone can create
plex whole. new terms in a simple way. The users feel that trust, and
we believe it explains the success of these software systems.
Engineering Engineering requires not just the ability to
use mathematics, but the ability to understand what, Another important aspect is collaboration. In traditional
if anything, the mathematics tells us about an actual software, an expert or a set of experts creates a thesaurus of
system. (Leslie Lamport, [3], page 21) categories and takes care of indexing documents themselves.
This avoids the insertion of erroneous data, but also the
Behavior The way in which a natural phenomenon or a
insertion of different aspects and viewpoints on the objects.
machine works or functions.
The collaborative tagging system allows anyone to index any
Abstraction The process of considering something inde- object without any restriction with meaningful terms. The
pendently of its associations, attributes, or concrete notion of meaningfulness is subjective, but the combination
accompaniments. of points of views from many people is more complete than
the one of only a chosen subset (experts). The resulting
Trust Firm belief in the reliability, truth, ability, or taxonomy is often called a folksonomy.
strength of someone or something.
Though simple in terms of software, this system exhibits
Term A word or phrase used to describe a thing or to ex- complex collective behaviors. As the number of people work-
press a concept, esp. in a particular kind of language ing collectively grows, the system of interaction between
or branch of study. them must be simplified. In a democratic political system,
Human A human being, esp. a person as distinguished the voting system is an example of a simple interaction to
from an animal or (in science fiction) an alien. decide collectively at a large scale. To organize knowledge
together, the interaction system between humans must be
Object A thing external to the thinking mind or subject. as simple as possible.
Phenomenon The object of a person’s perception; what Recent fundamental work as been done by analysing Del.icio.us[1]
the senses or the mind notice. and Flickr[4] tagging memory. In [1], Golder compares the
Observation The action or process of observing something tagging system to a typical filesystem organization
or someone carefully or in order to gain information.
Representation A mental state or concept regarded as In contrast to a hierarchical file system, a non-
corresponding to a thing perceived. exclusive, flat tagging system could, unlike the
system described above, identify such an article
Transcription A written or printed representation of as being about a great variety of things simulta-
something. neously...
Memory Something remembered from the past.
They describe how synonymous and polysemous aspects of
Figure 1: Fundamental glossary. terms can be solved in a collaborative tagging system and
define tagging as
Tagging is fundamentally about sensemaking.
They identified different ways people use terms to tag than implementation-oriented notations. Typically, a logi-
cal notation is most appropriate. For this purpose, we have
chosen to use TLA+ (Temporal Logic of Actions). We do
• Identifying what (or who) it is about. not discuss here the different values of such languages and
choose to use TLA+. Any number of equivalent notations
• Identifying what it is.
could be used for this purpose. One advantage of TLA is
• Identifying who owns it. that it comes with a model checker (TLC), which efficiently
validates the model and its properties.
• Refining categories.
Temporal Logic of Actions is a first order logic enriched
• Identifying qualities or characteristics.
with temporal operators. We describe in this section the key
• Self reference. aspects of such specifications and the language specifics. We
emphasize that the main purpose of writing specifications is
• Task organizing. to understand the system. According to Lamport:
in [4] Marlow gives a model of tagging which is represented The hardest part of writing a specification is
as a bipartite graph showing resources (what we call objects choosing the proper abstraction.
in this paper) on the left hand side and users on the right
The art of abstraction is learned only through
hand side. The edges between resources and users carry
experience.
some terms and represent an act of tagging (what we call
an observation in the following sections). He also identifies (Leslie Lamport, [3], page 24)
some aspects of tagging software systems :
Thus a large part of our effort has gone into deciding the ab-
• Tagging Rights. stractions to specify. We hope to give the reader the benefit
of our experience gained in formulating the specifications.
• Tagging Support. Note that such specifications may be defined for a system
that is yet to be built (forward engineering) in order to un-
• Aggregation.
derstand the requirements and help in evaluating the design
• Type of Object. alternatives, or for an existing system in order to understand
it better and help in enhancing it (reverse engineering).
• Source of Material.
In our case, the purpose of the specifications is to formally
• Resource Connectivity.
define possible behaviors of the studied system. A behavior
• Social Connectivity. is described by Leslie Lamport as
These empirical studies, together with our own understand- A behavior is an infinite sequence of states.
ing of existing software systems have been helpful in writing A behavior describes a potential history of the
the collaborative tagging specifications. In addition to these universe.
two works, there has been considerable research activity in
(Leslie Lamport, [3], paragraph 4, page 18)
this area recently [7].
1.3 Writing Specifications in TLA+ but for practical reasons, we consider only a subset of the
The role of specifications is both well-known and contro- abstractions which make sense to consider in the study of a
versial in the practice of software development. Here we particular system. In Figure 2, we present a behavior of the
are dealing with specifications of a system, as opposed to a HourClock example shown in [3]. In this representation only
specification of a design or architecture. We are using the two variables are considered, hr the current hour and tmp
term and the process in the sense of Lamport: the current temperature. Each state is represented by the
values of the variables. The process of writing specifications
is to first identify this kind of behavior and then formally
Specifying a system helps us to understand it. define the actions which describe a correct behavior.
(Leslie Lamport, [3], paragraph 4, page 1)
A specification in TLA+ (despite the declaration of vari-
ables and extensions needed) starts with a predicate which
The specification then can be used as a medium of commu- describes the potential initial state of a behavior. This is
nication among people about the system. The specification usually a conjunction of expressions describing the possible
may, for example, be used by software architects to design a values of the considered variables. The following predicate
particular implementation of the system. The specifications describes the initial state of the temperature hour clock ex-
∆
are thus a bridge between the requirements and the imple- ample. The = is read “is defined as equal to”.
mentation. They are also a means of defining the relation-
ship between the system and the real world. Thus, specifica- To describe the evolution from one state to another, one
tions must be specified at a much higher level of abstraction must define actions which are formulas containing variables
» – » –
hr = 11 hr = 12 phenomena are observable facts. Differing from typical se-
→ →
tmp = 23.5 tmp = 23.5 mantic systems, the facts are considered outside of the sys-
» – » –
hr = 12 hr = 12 tem. Only the human perceptions of the facts are considered
→ →
tmp = 23.4 tmp = 23.3 valuable. We do not have direct access to the facts, neither
» –
hr = 1 can we formulate them. We can feel an object, but we do
→ ··· not know what it really is.
tmp = 23.3
Through the senses, humans perceive the phenomena. The
Figure 2: An example behavior of the Hour Clock, resulting observations are the data of our system. Indeed
which also takes care of the temperature. the only thing that is known are the observations. Obser-
∆ vations are subjective, therefore different humans will have
HCTMPInit = different observations of the same phenomenon. Some per-
∧ hr ∈ {1, . . , 12} ceive the color, some others the shape or any other aspect.
∧ tmp ∈ Reals A fundamental premise of collaborative tagging is that the
combination of all these observations is the best picture we
enriched with a 0 which represent the value of the variable can get of the real phenomenon which occurred.
in the next state. The following predicate defines the hour
clock main action (which is to go from one hour to another When a human observes a phenomenon, he thinks a mental
and to pass to the value 1 after the 12), we don’t consider representation. This helps him to reason about the phe-
the temperature here: nomenon. Depending on the aspects he perceived in his ob-
servation, he mentally associates terms to the phenomenon.
∆
HCini = hr ∈ {1, . . , 12} These terms may be different for each human who observed
∆
HCnxt = hr 0 = (hr %12) + 1 the phenomenon so we need to consider them all.
A specification is a single formula which should satisfy both To be able to combine the mental representations of differ-
the initial predicate and the next-state actions for any step ent humans, we first need humans to express them. They
of the possible behaviors of the system. That is where we can not directly express their representations so they share
use the temporal operator 2 called “box” which expresses observations together with the terms they use in their men-
a formula which is “always true”. We can then write the tal scheme. This we call transcription. In the collaborative
specifications of the hour clock as follows tagging system, humans write their observations by tagging.
∆
HCSpec = HCini ∧ 2HCnxt When one assigns a tag to an object, the system stores the
observation in a memory. This memory is the set of all tran-
But as we have seen in Figure 2, some steps do not change scripted observations. A written observation is the associa-
the value of the variable hr especially if we consider a state tion of the human (the writer), the object of the observation,
being a state of the whole universe. Temporal logic of ac- the term of his representation and the date when he wrote
tions here introduce the concept of stuttering steps which it.
consider the possibility of having one or more variables left
unchanged from one state to another If we consider the vari- Other humans can then retrieve these observations from the
able hr as the stuttering variable, we write it as follows: collaborative tagging memory. When reading the observa-
∆ tions of other humans, the reader changes his representa-
HCSpec = HCini ∧ 2[HCnxt]hr
tions of the object as he now perceives the observations made
by different humans.
We now have the HCSpec formula which, if satisfied by a be-
havior, validates the behavior of the described system. This
Reading and writing are the two operations of the memory,
short description of the TLA+ language should be enough to
tagging and retrieving the two operations of the collabora-
enable the reader to understand the following system spec-
tive tagging system. We present in the next subsections the
ifications. The language is described fully in [3] which is
specification of the memory and of the whole system.
also available on the TLA Web page1 . The TLA system is
accompanied by a model checker, TLC, that may be used
The abstractions and the specifications presented here re-
to validate properties of well-defined specifications.
flect our understanding of many existing software systems
and of an ideal one. We try to be as generic and general as
2. THE COLLABORATIVE TAGGING SYS- possible to specify the collaborative tagging system and not
TEM SPECIFICATIONS a collaborative tagging software system.
To explain the specifications we first need to go back to the
abstractions of the collaborative tagging system. The col-
laborative tagging system is an interaction between humans,
terms and objects. In Figure 3 we give a graphic represen-
tation of this interaction which we explain in this section.
The environment of the collaborative tagging system is the
set of all phenomena emerging from the real world. The
1
http://research.microsoft.com/users/lamport/tla/tla.html
Figure 3: Diagram of the collaborative tagging system and its environment.
The phenomena are the environment of the system. Observations are the human perceptions of the phenomenon.
The representations are the mental association of terms to the observations. The transcription is the process of
writing the observations, what we call tag. The collaborative tagging memory stores observations.
2.1 The Collaborative Tagging Memory The next state actions of the memory are defined as Write(line
We define a module to specify the collaborative tagging 23), Read (line 27) and NextNow (line 31). A Write action
memory. The full specification of this module is presented occurs if there exists a human, an object and a term such
in Figure 5. The predicate on line 4 defines the initial state that the operation write for the time of now is true(line
of this system. We need to consider the time, represented 24-25). A write action leaves the variables buffer and now
by the variable now which is initially any value in the Time unchanged(line 26).
set(line 5). The Observations is the variable which stores
the data of our memory(line 6). In any initial state, the The Read action occurs if there exists a human, an object or
observations set may contain any observation that has been a term such that the operation read is true for the human as
done in the past. One particular observation is defined as the reader and the requests on the term and the object(line
a record which consists of values for a human, an object, 28-29). The read operation changes the buffer but leaves
a term and a date. Records allow us to write expressions the variables now and Observations unchanged(line 30).
like observation.human which represents the value of the
human in this particular observation. The set observation The NextNow action adds a second to the now variable if
in the initial state is a subset of the set of all records for any the resulting value is still in Time. It leaves the variables
human, object, term and date of the past(line 7-8). The buffer and Observations unchanged(line 32).
variable buffer is a function which for any human returns a
set of observations he requested. In the initial state this is We now define the next state action of the whole memory
set to the empty set for any human as no one has requested NextCollaborativeTaggingMemory as being the disjunction
anything yet(line 9). of the actions Write, Read and NextNow (line 33-34).
From the definition of the initial predicate, we can deter- The specification of the memory is defined by the predicate
mine the constants and variables we use. The constants CollaborativeTaggingMemorySpec which is the conjunction
can be seen as parameters of the system. When using the of the initial predicate and the temporal expression which re-
TLC model checker, the constants are set to particular val- flects that for all states, the next state action is true. There
ues. On line 3 we define the constants Humans(the set of all can be stuttering steps which leave the value of the variables
humans interacting with the memory), Terms(the set of all unchanged(line 37).
terms used in the memory), Objects(the set of all objects ob-
served), Time(the set of all values of time considered). This We now have the full specification of the collaborative tag-
is a tradeoff as new humans might enter the system during ging memory. In the following subsection we show how we
its lifetime, new terms could be created as new objects de- used the model checker to verify it.
fined, and the time passes without stopping. In a realistic
system, these constants would be variables. The reader can Model Checking The Collaborative Tagging Memory
understand constants as types.
Module
The variables defined on line 4 represent what change during The TLA+ language comes with a model checker, TLC. We
the life of the system. In this case the behavior is represented used it all along the writing process and it has been valuable
by the value of the Observations(the set of all observations in the refinement of the specifications. The model checker
written so far), now the time of now in number of seconds, takes a configuration file which give values to the constants
buffer (the state of the requests made by readers). and states the properties to be checked. Figure 4 shows the
configuration file we use to model check the collaborative
The type invariant property on line 16 defines that the be- tagging memory.
havior must respect the TypeInvariant for every state. The CONSTANTS
type invariant (line 10-15) is quite straightforward as the Humans = {"human:bob", "human:alice"}
variables now and Observations must be in any state allowed Objects = {"object:1","object:2"}
by the initial predicate. The function buffer must respect Terms = {"term:1","term:2"}
that for any reader, the set of observations requested is a Time = {1,2}
subset of the stored observations(line 15). SPECIFICATION CollaborativeTaggingMemorySpec
PROPERTY TypeInvariantProperty
This system being a memory storing the result of transcrip-
tions, its fundamental operations are defined as read (line
19) and write(line 17). The write operator defines the next Figure 4: The configuration file used to model check
state of the variable Observations as being the union of the the collaborative tagging memory specification.
current value of it and of the new observation that is written.
The model checker generated 66307 states and found 65792
The read operator is a bit more complex as it takes a reader distincts states without errors. The difference reflects the
and a set of requests. It defines the value of the next state number of ways which reach states with same values. It
of the function buffer and changes the value associated to means that the type invariant property is respected for any
the human reader . It sets this to the set of all observations state and that the specification permits to cover all these
which satisfy at least one request(line 20-22). Each request states.
is a record consisting of a type(either human, object, term
or date) and a value that is requested for that type. The
reader can then feel free to read the buffer prepared for him.
module CollaborativeTaggingMemory
1 extends Naturals, TLC
2 constants Humans, Terms, Objects, Time
3 variables Observations, now , buffer
∆
4 InitCollaborativeTaggingMemory =
5 ∧ now ∈ Time
6 ∧ Observations ∈
7 subset {[human 7→ human, object 7→ object, term 7→ term, date 7→ date] :
8 human ∈ Humans, object ∈ Objects, term ∈ Terms, date ∈ {t ∈ Time : t ≤ now }}
9 ∧ buffer = [human ∈ Humans 7→ {}]
∆
10 TypeInvariant =
11 ∧ now ∈ Time
12 ∧ Observations ∈
13 subset {[human 7→ human, object 7→ object, term 7→ term, date 7→ date] :
14 human ∈ Humans, object ∈ Objects, term ∈ Terms, date ∈ {t ∈ Time : t ≤ now }}
15 ∧ ∀ reader ∈ Humans : buffer [reader ] ∈ subset Observations
∆
16 TypeInvariantProperty = 2TypeInvariant
∆
17 write(writer , object, term, date) = Writing adds a new observation.
18 Observations 0 = Observations ∪ {[human 7→ writer , object 7→ object, term 7→ term, date 7→ date]}
∆
19 read (reader , requests) = Reading puts the requested observations in a buffer for the reader.
20 buffer 0 = [buffer except ![reader ] = {
21 observation ∈ Observations : ∃ request ∈ requests :
22 observation[request.type] = request.value}]
∆
23 Write =
24 ∃ human ∈ Humans : ∃ term ∈ Terms : ∃ object ∈ Objects :
25 ∧ write(human, object, term, now )
26 ∧ unchanged hnow , buffer i
∆
27 Read =
28 ∃ human ∈ Humans : ∃ term ∈ Terms : ∃ object ∈ Objects :
29 read (human, {[type 7→ “term”, value 7→ term], [type 7→ “object”, value 7→ object]})
30 ∧ unchanged hnow , Observationsi
∆
31 NextNow =
32 (now + 1) ∈ Time ∧ now 0 = now + 1 ∧ unchanged hObservations, buffer i
∆
33 NextCollaborativeTaggingMemory = A next state is defined by either reading, writing or passing the time.
34 Read ∨ Write ∨ NextNow
∆
35 CollaborativeTaggingMemorySpec =
36 ∧ InitCollaborativeTaggingMemory
37 ∧ 2[NextCollaborativeTaggingMemory]hnow , Observations, buffer i
Figure 5: The CollaborativeTaggingMemory specification
2.2 The Collaborative Tagging System CONSTANTS
Humans = {"human:bob", "human:alice"}
Figure 7 presents the full collaborative tagging system spec-
Objects = {"object:1","object:2"}
ifications. According to Figure 3, the collaborative tagging
Terms = {"term:1","term:2"}
system contains a collaborative tagging memory that we
Time = {1,2}
specified in the previous subsection. We instanciate the
memory module (line 4) and define as constants and vari-
SPECIFICATION CollaborativeTaggingSpec
ables the same one of this module. We introduce a new vari-
PROPERTIES ConsistencyProperty TypeInvariantProperty
able Representation which represents the state of the mind
of each human. The initialization predicate consists of the
initialization of the memory and the definition of the repre- Figure 6: The configuration file used to model check
sentations variable(line 11-12). A representation is a record the collaborative tagging system specification.
which consists of a human, an object and a term; initially,
the representations is any subset of all possible representa-
tions. We explain line 13 at the end of this subsection. we obtain the same results.
The two actions shown in Figure 3 are tag(line 21) and
retrieve(line 19). These are both interfaces to the collab- 3. FUTURE WORK
orative tagging memory.
3.1 Possible next steps
The next state actions are defined as Tag and Retrieve pred- Given a valid specification of collaborative tagging as pre-
icates on lines 30 and 23. The Retrieve action occurs if the sented here, there are several ways that it can be exploited.
reader has a representation which can help him to read ob- The most concrete step is to use it as a guide in design and
servations from the memory which change his representation architecture of an implementation. For example, the spec-
(lines 25-29). The Tag action occurs if the writer has a rep- ification can be used to guide the choice of data structures
resentation that he can write as an observation(lines 31-33). and representations for observations. We discuss this in the
next subsection.
The next state action Next is defined as the disjunction of
the NextNow action from the memory and for any human Another possibility is to explore enhancements to collabo-
either the Tag or the Retrieve action(line 34-36). rative tagging in a semantic way. For example, what is the
effect of associating several terms at the same time with an
The full specification predicate is shown on lines 37 and 38. object? Is that different from assigning each of the terms
It is the conjunction of the Init predicate and for all states separately?
of the Next action.
Third, we could define other Internet services such as col-
We introduce here a theorem that is implied by the specifi- laborative search and then explore the interaction of these
cation: “Humans know something about the world”. This services with collaborative tagging. This, indeed, can be the
is defined on lines 5 to 8 as being equals to: for all humans way to gain control over the ever-expanding set of services
there exists a representation owned by the human. Every- and understand their implications as they are introduced.
one knows at least something about the world, otherwise he
could not tag, neither retrieve anything and the property 3.2 Implementation proposals
Consistency would never occur. The consistency property
We are currently working on the implementation of these
is defined as eventually every human has the same represen-
specifications in the Gnowsis semantic desktop [5], defined
tation(line 14-18).
as:
“A Semantic Desktop is a device in which an individual
Model Checking The Collaborative Tagging Specifica- stores all her digital information like documents, multime-
tion dia and messages. These are interpreted as Semantic Web
To model check the theorem presented previously, we need resources, each is identified by a Uniform Resource Identi-
to check that the property ConsistencyProperty is respected. fier (URI) and all data is accessible and queryable as RDF
We introduce in the Init conjunction the predicate graph. Resources from the web can be stored and authored
HumansKnowSomethingAboutTheWorld . Otherwise the prop- content can be shared with others. Ontologies allow the user
erty never occurs. This is called an implied init. Figure 6 to express personal mental models and form the semantic
presents the configuration file used to model check the col- glue interconnecting information and systems. Applications
laborative tagging system. respect this and store, read and communicate via ontologies
and Semantic Web protocols. The Semantic Desktop is an
The data given as argument to the model checking is the enlarged supplement to the user memory.”
same we used to model check the collaborative tagging mem-
ory. TLC found 65792 distinct states and 329216 states were In the specifications, we did not care if the tagging memory
generated. The number of distincts states is the same as is distributed or centralized, for implementation purposes
with the collaborative tagging memory, which sounds natu- in the case of a desktop software system, we propose to
ral as we use the same data and that the tag and retrieve implement this memory as distributed amongst users and
actions are mappings to the read and write actions. This shared through the use of RSS (Really Simple Syndication)
gives us confidence in the validity of both specifications as using the XML format of Figure 8.
module CollaborativeTagging
1 extends Naturals, TLC
2 constants Humans, Terms, Objects, Time
3 variables Observations, Representations, buffer , now
4 instance CollaborativeTaggingMemory
∆
5 HumansKnowSomethingAboutTheWorld = Everyone has at least one representation of something.
6 ∀ human ∈ Humans :
7 ∃ representation ∈ Representations :
8 representation.human = human
∆
9 Init = The memory is initialized, every human has representations.
10 ∧ InitCollaborativeTaggingMemory
11 ∧ Representations ∈ subset {[human 7→ human, object 7→ object, term 7→ term] :
12 human ∈ Humans, object ∈ Objects, term ∈ Terms}
13 ∧ HumansKnowSomethingAboutTheWorld
∆
14 Consistency = Eventually everyone has the same representation of every object.
15 ∀ human ∈ Humans : ∀ other ∈ (Humans \ {human}) :
16 {hr .object, r .termi : r ∈ {r ∈ Representations : r .human = human}} =
17 {hr .object, r .termi : r ∈ {r ∈ Representations : r .human = other }}
∆
18 ConsistencyProperty = 3Consistency
∆
19 retrieve(reader , requests) = The retrieve action is defined as an interface to reading from the memory.
20 read (reader , requests)
∆
21 tag(writer , object, term, date) = The tag action is defined as an interface to writing to the memory.
22 write(writer , object, term, date)
∆
23 Retrieve(reader ) = When someone retrieves observations, it changes his representation.
24 unchanged hnow , buffer , Observations, Representationsi ∧
25 ∀ representation ∈ Representations :
26 ∧ representation.human = reader
27 ∧ retrieve(reader , {[type 7→ “object”, value 7→ representation.object], [type 7→ “term”, value 7→ representation.term]})
28 ∧ Representations 0 = Representations ∪
29 {[human 7→ reader , object 7→ observation.object, term 7→ observation.term] : observation ∈ buffer [reader ]}
∆
30 Tag(writer ) = When someone has representations, he can write them.
31 unchanged hRepresentations, buffer , now , Observationsi ∧
32 ∀ representation ∈ Representations :
33 representation.human = writer ∧ tag(writer , representation.object, representation.term, now )
∆
34 Next = The time passes or humans can either tag or retrieve.
35 ∨ (NextNow ∧ unchanged hRepresentations, buffer , Observationsi)
36 ∨ (∀ human ∈ Humans : Tag(human) ∨ Retrieve(human))
∆
37 CollaborativeTaggingSpec =
38 Init ∧ 2[Next]hnow , Observations, Representations, buffer i
39 theorem CollaborativeTaggingSpec ⇒ HumansKnowSomethingAboutTheWorld ∧ ConsistencyProperty
Figure 7: The CollaborativeTagging system specification
The specifications of the collaborative tagging system helped 5. REFERENCES
us to understand the least data needed in order for a soft- [1] Scott Golder and Bernardo A. Huberman. The
ware system to behave like the collaborative tagging system. structure of collaborative tagging systems. Journal of
In these specifications, an observation is a relation between Information Science, 32(2):198–208, April 2006.
a human, an object, a term and a date. If we consider the
human and the object being identified by URIs (Uniform [2] Michael Jackson. Software requirements &
Resource Identifier) as they are all considered as resources specifications: a lexicon of practice, principles and
in current systems, the term as a string, and the date as prejudices. ACM Press/Addison-Wesley Publishing
a date, we can determine the collaborative tagging XML Co., New York, NY, USA, 1995.
schema which defines CollaborativeTaggingMemory consist- [3] Leslie Lamport. Specifying Systems: The TLA+
ing of one or more observations as follows. (This schema Language and Tools for Hardware and Software
will be documented and available soon on the collaborative- Engineers. Addison-Wesley Longman Publishing Co.,
tagging.org website.) : Inc., Boston, MA, USA, 2002.
2006.
[5] Leo Sauermann, Ansgar Bernardi, and Andreas
Dengel. Overview and outlook on the semantic
desktop. In Proceedings of the 1st Workshop on The
Semantic Desktop at the ISWC 2005 Conference, 2005.
[6] Patrick Schmitz. Inducing ontology from flickr tags. In
Collaborative Web Tagging Workshop at WWW2006,
Edinburgh, Scotland, May 2006.
[7] Frank Smadja, Andrew Tomkins, and Scott Golder.
Collaborative web tagging workshop. In WWW2006,
Edinburgh, Scotland, 2006.
Figure 8: The XML Schema of the collaborative tag- [8] Jennifer Trant and Bruce Wyman. Investigating social
ging observations. tagging and folksonomy in art museums with
steve.museum. In Collaborative Web Tagging
Workshop at WWW2006, Edinburgh, Scotland, May
The specifications lead to an understanding of the services 2006.
provided by both the collaborative tagging system and the
collaborative tagging memory. This simplifies the writing [9] Ludwig Wittgenstein. Tractatus Logico-Philosophicus.
of WSDL(Web Services Description Language) documents Routledge, 1922.
describing these services. We plan to do it lately together
with the implementation of these services within Gnowsis. [10] Zhichen Xu, Yun Fu, Jianchang Mao, and Difu Su.
Towards the semantic web: Collaborative tag
suggestions. In Collaborative Web Tagging Workshop
4. CONCLUSION at WWW2006, Edinburgh, Scotland, May 2006.
This paper contributes to the emerging collaborative tagging
field with the formal specifications in TLA+ of both the
collaborative tagging memory and the collaborative tagging
system. We gave confidence in the validity of these by using
the TLC model checker. It results in a better understanding
of possible software systems respecting these specifications.
We enunciated a theorem resulting from this understanding.
We proposed an XML schema to uniformly represent the
collaborative tagging observations.
We hope that others will enhance and continue to validate
the properties of the collaborative tagging system specifi-
cation. Over time, modular and incremental specifications,
such as given here, are the only way to understand and ex-
plain how complex, interacting, evolving systems work. We
hope that a collection of such specifications about impor-
tant services on the Internet will enable us to reason about
the interactions of existing and emerging services and their
behaviors.