## Sole.dimi.uniud.it

**A logical approach to**
**represent and reason about calendars**
Department of Computer Science, University of Verona, Italy
Department of Sciences, University ‘G. D’Annunzio’ of Pescara, Italy
Department of Physical Sciences, University ‘Federico II’ of Napoli, Italy

**Abstract**
*• Expressiveness*. The class of granularities represented
in the formalism should be large enough to be of prac-

*In this paper, we propose a logical approach to repre-*
*sent and reason about different time granularities. We iden-*
*• Effectiveness*. The framework should provide algo-

*tify a time granularity as a discrete infinite sequence of time*
rithms to reason about different time granularities. In

*points properly labelled with proposition symbols marking*
particular, it should provide an effective solution to the

*the starting and ending points of the corresponding gran-*
well-known problems of

*consistency*,

*equivalence *and

*ules, and we intensively model sets of granularities with lin-*
*classification*. The

*consistency problem *is the prob-

*ear time logic formulas. Some real-world granularities are*
lem of deciding whether a granularity representation

*provided, to motivate and exemplify our approach. The pro-*
is well-defined. The algorithmic solution of the con-

*posed framework permits to algorithmically solve the con-*
sistency problem is important to avoid the definition of

*sistency, the equivalence, and the classification problems in*
inconsistent granularities that may produce unexpected

*a uniform way, by reducing them to the validity problem for*
failures in the system. The

*equivalence problem *is the
problem of deciding whether two different represen-tations define the same granularity. The decidabilityof the equivalence problem implies the possibility of

**1. Introduction**
effectively testing the semantic equivalence of two dif-ferent time granularity representations, making it pos-sible to use the smaller and more tractable one. The
The ability of providing and relating temporal represen-

*classification problem *solves the problem of deciding
tations at different ‘grain levels’ of the same reality is an
whether a natural number

*n *belongs to a granule of a
important research theme in computer science and a major
given granularity. The classification problem is strictly
requirement for formal specifications, temporal databases,
related to the granule conversion problem which al-
data mining, problem solving, and natural language under-
lows one to relate granules of a given granularity to
Any time granularity can be viewed as the partitioning
of a temporal domain in groups of elements, where each

*• Compactness*. The formalism should exploit regulari-
group is perceived as an indivisible unit (a granule). The
ties exhibited by the considered granularities to make
description of a fact can use these granules to provide it with
their representations as compact as possible.

a temporal qualification, at the appropriate abstraction level.

In order to represent and reason about time granularity, any
The frameworks to represent and reason about time granu-
formalism should satisfy the following requirements:
larity present in the literature can be classified into algebraic
frameworks and logical frameworks. Algebraic frameworks
particular structure. To allow such computational proper-
for time granularities have been proposed by Ning, Jajo-
ties, however, some assumptions have to be made about the
dia and Wang [13], Foster, Leban and McDonald [5], and
involved granularities, as, for example, some form of regu-
Niezette and Stevenne [12]. In an

*algebraic *(or

*operational*)
larity of the sizes of the granules.

framework, a

*bottom granularity *is assumed, and a finite set
In this paper, we propose a logical approach to represent
of

*calendar operators *are exploited to create new granular-
and reason about different time granularities. We identify a
ities by suitably manipulating other granularities. A granu-
time granularity with a discrete linear time structure prop-
larity is hence identified by an algebraic expression. Log-
erly labelled with proposition symbols marking the start-
ical approaches to represent and reason about time granu-
ing and ending points of the corresponding granules. We
larity, based on a many-level view of temporal structures,
make use of a linear time logic, interpreted over labelled
have been proposed by Montanari in [8], and further in-
linear time structures, to model possibly infinite sets of time
vestigated by Franceschet, Montanari, Peron and Policriti
granularities. Any linear time formula is associated with
in [6, 9, 10, 11]. In a

*logical *(or

*descriptive*) framework
a set of labelled linear time structures satisfying the for-
for time granularity, the different granularities and their in-
mula (the set of models of the formula). Since any prop-
terconnections are represented by means of mathematical
erly labelled linear time structure identifies a time granu-
structures called layered structures, consisting of a possibly
larity, we may model possibly infinite sets of time gran-
infinite set of related differently-grained temporal domains.

ularities by means of well-defined linear time formulas.

Suitable operators make it possible to move horizontally
Moreover, a single sequence may identify a finite number

*within *a given temporal domain (displacement operators),
of different granularities (a calendar) by using a different
and to move vertically

*across *temporal domains (projection
couple of marking proposition symbols for any granular-
operators). Logical formulas allow one to specify properties
ity. Hence, well-defined linear time formulas may model
involving different time granularities in a single formula by
possibly infinite sets of calendars as well. The proposed
mixing displacement and projection operators.

framework permits to algorithmically solve the consistency,the equivalence, and the classification problems in a uni-
A comparison of the algebraic and the logical frame-
form framework by reducing them to the validity problem
for the considered linear time logic, which is known to be
frameworks have been applied to different application fields
decidable in polynomial space. Our approach is logical, and
hence it intrinsically differs from the algebraic one. How-
database context, granule conversion plays a major role be-
ever, the starting point of our approach and of the algebraic
cause it allows the user to view the temporal information
one is the same: the classical definition of time granular-
contained in the database in terms of different granularities,
ity given in [1]. Moreover, our logical approach differs
while in the context of verification, decision procedures for
from the above described logical one of Montanari et al for
consistency and model checking are unavoidable to validate
the following reason. While Montanari et al model differ-
the system. However, abstracting away from the applica-
ent time granularities by using multi-layered mathematical
tion fields of the two frameworks, a comparison is possible.

structures and use temporal logic formulas to capture

*prop-*
The main advantage of the algebraic framework is its nat-

*erties *of time granularities, we model both time granulari-
uralness: by applying user-friendly operations to existing
ties and their properties by using temporal logic formulas.

standard granularities like ‘days’, ‘weeks’, and ‘months’, a
Our solution enhances the flexibility of the task of granu-
quite large class of new granularities, like ‘business weeks’,
larity specification: the time granularity structure may be
‘business months’, and ‘years since 2000’, can be easily
changed by simply modifying the logical formula that de-
generated. The major weakness of the algebraic approach is
fines it, and the properties of the time granularity structure
that reasoning methods basically reduce to granule conver-
may be defined in the same logical language.

sions and semantic translations of statements. Little atten-
The rest of the paper is as follows. In Section 2 we
tion has received the investigation on algorithms to check
present some motivating examples. In Section 3 we pro-
whether some meaningful relation holds between granular-
pose our logical approach to represent and reason about
ities (e.g., to verify whether the granularity

*G*1 is finer than
time granularity, while in Section 4 we compare our work
granularity

*G*2 or

*G*1 is equivalent to

*G*2). Moreover, only
with related ones and we outline future work.

a finite number of time granularities can be represented. Onthe contrary, reasoning methods have been extensively in-vestigated in the logical framework, where both a finite and

**2. Motivating examples**
an infinite number of time granularities can be dealt with.

Theorem provers make it possible to verify whether a gran-
In introducing the needs of managing different granu-
ular requirement is consistent, while model checkers allow
larities, we will focus on an example coming from clinical
one to check whether a granular property is satisfied in a
medicine. In particular, we focus on the definition of spe-
cific granularities related to therapy plans. Intuitively, ther-

**3. A logical approach to represent and reason**
apy plans can be considered as the calendar according to

**about calendars**
which it is possible to properly observe the evolution of thepatient’s state.

In this section, we propose our logical approach to rep-
We consider here chemotherapies for oncological pa-
resent and reason about different time granularities.

tients, a topic which has been extensively considered bythe clinical research and that is precisely described and rec-

**3.1. Representing time granularity**
ommended in several clinical practice guidelines. In gen-eral, oncology patients undergo several chemotherapy cy-cles: each cycle can include the administration of several
We model time granularity according to the following
drugs, which the patient has to assume according to a spe-

**Definition 3.1 ***A *granularity

*is a mapping G *: N

*→ *2N

As an example, consider the following chemotherapy

*1. for all i < j, for any n ∈ G*(

*i*)

*and m ∈ G*(

*j*)

*, n < m;*
“The recommended CMF1 regimen consists of 14days of oral cyclophosphamide with intravenous

*2. for all i < j, if G*(

*j*) =

*∅, then G*(

*i*) =

*∅;*
methotrexate, and 5-fluorouracil on days 1 and 8.

This is repeated every 28 days for 6 cycles.”

*3. for any i ∈ *N

*, G*(

*i*)

*is a convex interval.*
Moreover, it may happen that the beginning of a cycle is
Following the classical definition given in [1], the domain
delayed a few days, due to patient’s blood analysis results.

of a granularity

*G *is called

*index set *and an element of the
Figure 1 provides a graphical representation of the recom-
codomain of

*G *is called a

*granule*. The definition of granu-
mended CMF regimen. According to this scenario, we can
larity above specializes the definition given in [1], assuming
easily identify some requirements related to the definition
that both the index set and the domain of granules are the
linear discrete domain (N

*, <*). The first condition states thatgranules in a granularity do not overlap and that their index
1.

*Definition of therapy-related granularities*.

order is the same as their time domain order. The second
granularities should be suitably specified for different
condition states that the subset of the index set that maps
patients, according to the moment at which they start a
to nonempty granules forms an initial segment. The third
condition avoids granularities with gaps inside the granules(this assumption will be relaxed in the following).

2.

*Definition of granularities having some degree of un-*
Let

*G *=

*{G*1

*, . . . , Gn} *be a

*finite *set of granulari-

*certainty*. There is, indeed, the need of representing
ties (we will refer to

*G *as a

*calendar*), and let

*PG *=
the fact that two consecutive cycles may be separated

*| *1

*≤ i ≤ n} *be a set of proposition symbols
by some days, due to the patient’s conditions.

associated with the calendar

*G*. Given an alphabet of propo-sition symbols

*P ⊇ PG*, we shall consider in the following
3.

*Verification of consistency between an assigned ther-*
*P*-labelled (discrete) linear time structures having the form

*apy and the recommended regimen*. Given a therapy
(N

*, <, V *), where (N

*, <*) is the set of natural numbers with
assigned to a patient with the specification of days
the usual ordering, and

*V *: N

*→ *2

*P *is a labelling func-
and corresponding drug assumptions, it is important to
tion mapping natural numbers to sets of proposition sym-
be able to determine whether the therapy is consistent
bols. The idea is to identify a time granularity

*G*, according
to Definition 3.1, with a linear time structure, properly la-belled with proposition symbols taken from

*{PG, QG}*: the
4.

*Assignment of a therapy according to the recom-*
starting (resp. ending) point of an arbitrary granule of

*G *in

*mended regimen and to other granularity-related con-*
the structure is labelled by

*PG *(resp.

*QG*).

*straints*. It could be necessary, for organizational rea-sons, to avoid that some specific drug administrations

**Definition 3.2 ***A labelled linear time structure *(N

*, <, V *)

*is*
happen during the weekend: for example, in specifying
a CMF therapy, we could avoid that the administration

*G ∈ V *(

*i*)

*for some i ∈ *N

*, then either QG ∈ V *(

*i*)

*or QG ∈ V *(

*j*)

*for some j > i such that PG ∈ V *(

*k*)
1CMF stands for the chemotherapy based on the drugs Cyclophos-

*for each i < k ≤ j and QG ∈ V *(

*k*)

*for each i ≤ k <*
phamide, Methotrexate, and 5-Fluorouracil.

*delays of 0-5 days between acycle and the next one*
**Figure 1. Granularities involved in a chemotherapy treatment.**
*• if QG ∈ V *(

*i*)

*for some i ∈ *N

*, then either PG ∈ V *(

*i*)
any granularity, since it is not

*G*-consistent (indeed,

*or PG ∈ V *(

*j*)

*for some j < i such that QG ∈ V *(

*k*)
the granules

*G*(0) =

*{*0

*, *1

*} *and

*G*(1) =

*{*1

*, *2

*} *inter-

*for each j ≤ k < i and PG ∈ V *(

*k*)

*for each j < k ≤*
In the following we show how a set of granularities can
The above conditions say that every point labelled with

*PG*
be defined in an intensional declarative manner by means
has to match with a unique point labelled with

*QG*, and vice
of a formula of a propositional linear time logic (instead
versa. It is easy to see that every

*G*-consistent labelled linear
of defining it extensively as done in Example 3.3). We
time structure induces a granularity

*G*: given a

*G*-consistent
will use Past Propositional Linear Time Logic (PPLTL for
labelled linear time structure

*M *= (N

*, <, V *), a granule of
short) [4], interpreted over labelled linear time structures.

*M *with respect to

*G *is a set

*{n, n*+1

*, . . . , n*+

*k}*, for some
A PPLTL-formula intensionally defines a possibly infinite

*n, k ≥ *0, such that

*PG ∈ V *(

*n*),

*QG ∈ V *(

*n *+

*k*) and

*QG ∈*
set of labelled linear time structures, which correspond to

*V *(

*n *+

*j*) for all 0

*≤ j < k*. The granularity

*G *induced by
the linear time structures satisfying the formula. Since, as

*M *is such that

*G*(

*i*) is the

*i*-th granule of

*M *with respect to
shown above, consistently labelled linear time structures

*G*, if any, and

*G*(

*i*) =

*∅ *otherwise. Similarly, a granularity
correspond to granularities, we can use suitable linear time

*G *induces a

*G*-consistent labelled linear time structure.

formulas to define sets of granularities. We proceed by in-troducing the syntax and the semantics of PPLTL.

**Example 3.3 **We give two examples of labelled linear time

structures that induce well-defined granularities and one ex-

**Definition 3.4 **(

*Syntax of *PPLTL)

ample of a labelled linear time structure that does not corre-spond to a granularity.

*Formulas of *PPLTL

*are inductively defined as follows:*
*• *The structure (N

*, <, V *) such that

*V *(

*i*) =

*{P*
*• any proposition symbol P ∈ P is a *PPLTL

*formula;*
is even, and

*V *(

*i*) =

*{QG} *iff

*i *is odd, induces the

*• if φ and ψ are *PPLTL

*formulas, then φ ∧ ψ and ¬φ*
uniform, continuous and total granularity

*G *such that

*G*(

*i*) =

*{*2

*· i, *2

*· i *+ 1

*}*
The structure (N

*, <, V *) such that

*V *(0) =

*{P*
*if φ and ψ are *PPLTL

*formulas, then *X

*φ, φ*U

*ψ,*
X

*−*1

*φ and φ*S

*ψ are *PPLTL

*formulas.*
*G}*,

*V *(3) =

*{PG}*,

*V *(5) =

*{QG} *induces
the non-uniform, non-continuous, non-total granular-
Formulas

*φ ∨ ψ*,

*φ → ψ*, and

*φ ↔ ψ *are defined
ity

*G *such that

*G*(0) =

*{*0

*, *1

*}*,

*G*(1) =

*{*3

*, *4

*, *5

*}*, and

*G*(

*i*) =

*∅*
as

*¬*(

*¬φ ∧ ¬ψ*),

*¬φ ∨ ψ*, and (

*φ → ψ*)

*∧ *(

*ψ → φ*),
Moreover, F

*p *(

*p *will hold in the future),

*• *The structure (N

*, <, V *) such that

*V *(0) =

*{PG}*,
G

*p *(

*p *will always hold in the future), P

*p *(

*p *held in the

*V *(1) =

*{QG, PG}*,

*V *(2) =

*{QG} *does not induce
past) and H

*p *(

*p *always held in the past) are shorthands for,
respectively, trueU

*p*,

*¬*F

*¬p*, trueS

*p *and

*¬*P

*¬p*, where
the calendar

*G *may be captured in our framework. For
true =

*P ∨ ¬P *, for some

*P ∈ P*.

instance,

*G*1 GroupInto

*G*2 (each granule of

*G*2 is ob-
We interpret PPLTL over

*P*-labelled linear time struc-
tained by grouping granules of

*G*1),

*G*1 FinerThan

*G*2
tures. The semantics of PPLTL is as follows.

(each granule of

*G*1 is contained in some granule of

*G*2),

*G*1 SubGranularityOf

*G*2 (each granule of

*G*1 is equal

**Definition 3.5 **(

*Semantics of *PPLTL)

to a granule of

*G*2) [13]. As an example, the relation

*Let M *= (N

*, <, V *)

*be a P-labelled linear time struc-*
FinerThan can be captured by the following formula:

*ture and i ∈ *N

*. The truth of a *PPLTL

*-formula ψ in Mwith respect to the point i, denoted M, i |*=

*ψ, is defined as*
*η*(

*G*1)

*∧ η*(

*G*2)

*∧ *G((

*PG → α*)

*∧ *(

*Q*
*P ∈ V *(

*i*)

*for P ∈ P*
*M, i |*=

*φ and M, i |*=

*ψ*
*it is not the case that M, i |*=

*φ*
*M, j |*=

*ψ for some j ≥ i and*
Hence, the calendars with

*n *granularities that are totally or-

*M, j |*=

*ψ for some j ≤ i and*
dered with respect to the FinerThan relation are defined by

*M, k |*=

*φ for each j < k ≤ i*;

*i > *0

*and M, i − *1

*|*=

*ψ.*
*We say that M is a model of ψ if M, *0

*|*=

*ψ.*
**Example 3.6 **We give some examples of how PPLTL-

formulas can encode sets of granularities.

The above framework does not consider granularities withgaps inside the granules (only convex granules are treated).

*• *The set of all

*G*-consistent granularities (according to
However, it can be easily extended to cope with non-convex
Definition 3.2) is captured by the following PPLTL-
granules. The idea is to use symbols

*PG *and

*QG *to delimit
the granules of a granularity

*G *as done before, and symbols

*PH *and

*Q*
to bound the gaps inside the granules of

*G*.

*η*(

*G*) = G((

*PG → α*)

*∧ *(

*QG → β*))

*,*
In this way we have that the description of the gaps of

*G*is itself a granularity

*HG*. Note that

*HG *is finer than

*G*.

Indeed, every internal gap of

*G *(a granule of

*HG*) is a sub-
set of some granule of

*G*. Moreover, there are no granules

*G ∨ *X(

*¬*(

*PG ∨ QG*)U(

*¬PG ∧ QG*))
of

*G *that are entirely covered by gaps (granules of

*H*
*G ∨ *X

*−*1(

*¬*(

*PG ∨ QG*)S(

*PG ∧ ¬QG*))

*.*
*HG *GroupInto

*G *does not hold.

*• *The (singleton containing the) granularity

*G *such that

*G*(

*i*) =

*{*2

*· i, *2

*· i *+ 1

*}*
We conclude this section by reconsidering the chemother-
apy treatment described in Section 2.

**Example 3.7 **Let us assume that

*OC *(cyclophosphamide),

*G ∧ *G(

*PG → *(

*¬QG ∧ ¬*X

*PG ∧ *XX

*PG*))

*.*
*IM *(intravenous methotrexate) and

*F I *(5-fluorouracil) are
proposition symbols corresponding to the drugs of the CMF
The infinite set of granularities obtained by an arbi-
regimen. We preliminary introduce some useful shorthands.

trarily right-shifting

*G *(i.e., the non-anchored version
For a formula

*p*, X

*n*(

*p*) stands for “

*p *holds in

*n *time in-
of

*G*), where

*G*(

*i*) =

*{*2

*· i, *2

*· i *+ 1

*}*, for each

*i ∈ *N,
stants”, and is defined as follows: X0(

*p*) =

*p*, and X

*n*(

*p*) =
XX

*n−*1(

*p*). For 0

*≤ n ≤ m*,

*∀*[

*n, m*](

*p*) (resp.

*∃*[

*n, m*](

*p*))

*η*(

*G*)

*∧ *F(

*P*
stands for “

*p *holds everywhere (resp. somewhere) in the
time interval [

*n, m*]”, and is defined as

*G ∧ ¬*X

*PG ∧ *XX

*PG*)))

*.*
Finally,

*Count*(

*p, n*) stands for “

*p *holds
A finite number of different granularities may be addressed
exactly

*n *times in the future” and is defined as follows:
in the same formula by using different pairs of mark-

*Count*(

*p, *0) = G(

*¬p*) and

*Count*(

*p, n*) =

*¬p*U(

*p ∧*
X(

*Count*(

*p, k − *1))).

dar

*G *=

*{G*1

*, . . . , Gn}*, the formula
The formula Ω

*CMF *below defines, on the time domain
the set of all calendars with

*n *granularities

*G*1

*, . . . , Gn*.

N of days, a granularity CMF according to the recommen-
Meaningful relations between granularities belonging to

**Consistency, equivalence and classification. **As far as

consistency is concerned, given a PPLTL-formula

*ϕ*, one
G(

*PCMF → *(

*∀*[0

*, *26](

*¬QCMF *)

*∧ *X27

*QCMF *))

*∧*
can verify whether it encodes a set of well-defined granular-
G((

*QCMF ∧ *F

*PCMF *)

*→ ∃*[1

*, *5]

*PCMF *)

*∧*
ities (according to Definition 3.1) by checking the validity
G(

*PCMF → *(

*∀*[0

*, *13](

*OC ∧ IM*)

*∧ F I ∧ *X7(

*F I*)

*∧*
of the formula

*ϕ → η*(

*G*).

*∀*[14

*, *27](

*¬OC ∧ ¬IM ∧ ¬F I*)))
The equivalence problem for two sets of granularities de-
The first conjunct says that CMF is a granularity. The sec-
1 and

*ϕ*2, respectively, is reduced to checking the
ond and the third conjuncts say, respectively, that the gran-
Finally, the classification problem, that is, the problem of
ularity CMF consists of 6 granules (cycles) each of 28 ele-
checking whether a natural number

*n *belongs to a granule
ments (days). The fourth conjunct states that each cycle is
of a granularity

*G *defined by a PPLTL-formula

*ϕ *can be
separated by time intervals not exceeding 5 units. Finally,
solved as follows. We have that

*n ≥ *0 is contained in some
the fifth conjunct associates the drugs to each day in the
granule of any granularity defined by

*ϕ *if the formula

*ϕ →*
cycle, according to the recommendation (the first 14 days
cyclophosphamide and intravenous methotrexate, with 5-

*n*(

*G*) is valid, where

*αn*(

*G*) is the formula:
fluorouracil on days 1 and 8, and no drugs during the second
Xn(

*¬*(

*PG ∨ QG*)S

*PG ∧ ¬*(

*PG ∨ QG*)U

*QG*)
It is worth pointing out that the model checking and the va-
It is worth noting that in the above example only a
lidity problems for linear time logics have been extensively
bounded form of uncertainty is involved. Indeed, two suc-
studied. Both the problems belong to the complexity class
cessive cycles may be separated by no more than 5 time
PSPACE (polynomial space) [4], and efficient procedures
units (in the chosen granularity). However, there exist ap-
plications calling for

*unbounded uncertainty*. For instance,two therapy cycles that are arbitrarily distant. Our frame-work can cope with unbounded uncertainty as well.

**4. Related and future work**
**3.2. Reasoning about time granularity**
A related recent approach to represent and reason about
time granularity has been proposed by Wijsen [14] and re-
Besides representing sets of granularities and relations
fined by Dal Lago and Montanari [3]. Wijsen modelled infi-
among them, our framework permits to automatically solve
nite granularities as infinite strings over a suitable finite al-
phabet. The resulting string-based model is then used to for-mally state and solve problems of granularity equivalence

**Automatic verification of granularity properties.**
and minimality. Dal Lago and Montanari gave an automata-
verifying properties against models, we can exploit in a nat-
theoretic counterpart of the string-based model. They used
ural way the mature technology of

*model checking *[2]. A
single string automata, that is, finite-state automata accept-
labelled structure representing a concrete set of granulari-
ing a single infinite string, to represent in a compact way
ties can be suitably encoded in the format required by the
time granularities and to give an algorithmic solution to the
chosen model checker and it can be checked against a for-
problems of equivalence and classification of time granular-
mula of a propositional linear logic which describes the re-
ities. The resulting formalism satisfies the requirements of
quired property. For instance, with reference to our clini-
effectiveness and compactness. As for expressiveness, it is
cal example, a concrete chemotherapy plan can be checked
not able to represent

*dynamic granularities*, that is, granu-
for consistency against the formula Ω

*CMF *describing the
larities that are not anchored to the underlying time domain.

chemotherapy regimen (as described in the requirement 3
A typical example of dynamic granularity is a repeating pat-
tern that can start at an arbitrary time point. Our formalism

**Automatic generation of granularities. **Given a formula

has the expressive power to represent both static and dy-

*ϕ *defining a set of granularities, it it possible to automati-
namic granularities. Dynamic ones are encoded by tempo-
cally generate the labelled linear time structures satisfying
ral formulas representing a possibly infinite set of granu-

*ϕ*. More technically, it is possible to construct a finite state
larities. Moreover, our formalism is effective: consistency,
automaton which accepts the set of structures satisfying the
equivalence, and classification problems can be algorithmi-
formula

*ϕ*. Any concrete labelled linear time structure satis-
cally solved in a uniform and elegant way. However, our
fying the formula

*ϕ *can be obtained by suitably unravelling
formalism lacks compactness: the representation formula
the automaton. For instance, we can obtain all of the possi-
can be very long whenever a periodic granularity has a long
ble schedules for a chemotherapy according to the regimen
prefix or period (for instance, in the case of the Gregorian
encoded by the formula Ω

*CMF *.

calendar). We aim at finding a possible way out to this prob-
lem within our logical framework. A solution may reside in
[11] A. Montanari and A. Policriti. Decidability results for
the use of a

*metric *linear time logic, which extends linear
metric and layered temporal logics.

*Notre Dame Jour-*
time logic with methods to express

*quantitative *temporal

*nal of Formal Logic*, 37:260–282, 1996.

[12] M. Niezette and J. Stevenne. An efficient symbolic
representation of periodic time. In

*Proceeding of the*
**References**
*International Conference on Information and Knowl-edge Management*, volume 752 of

*Lecture Notes in*
[1] C. Bettini, S. Jajodia, and X. S. Wang.

*Time Granular-*
*Computer Science*, pages 161–168, Baltimore, Mary-

*ities in Databases, Data Mining, and Temporal Rea-*
[13] P. Ning, S. Jajodia, and X. S. Wang. An algebraic
[2] E. M. Clarke, O. Grumberg, and D. A. Peled.

*Model*
representation of calendars.

*Annals of Mathematics*
*Checking*. The MIT Press, Cambridge, Massachusetts,

*and Artificial Intelligence*. To appear.

[14] J. Wijsen. A string based-model for infinite granulari-
ties. In

*Proceedings of the AAAI Workshop on Spatial*
*and Temporal Granularity*, pages 9–16. AAAI Press,

*International Symposium on Spatial and Temporal*
*Databases*, volume 2121 of

*Lectures Notes on Com-puter Science*, pages 279–298, Los Angeles, CA,USA, 2001.

[4] E.A. Emerson. Temporal and modal logic. In J. van
Leeuwen, editor,

*Handbook of Theoretical ComputerScience, Vol. B*, pages 995–1072. Elsevier SciencePublishers B.V., 1990.

[5] D. Foster, B. Leban, and D. McDonald. A representa-
tion for collections of temporal intervals. In

*Proceed-ings of the American National Conference on ArtificialIntelligence*, pages 367–371, 1986.

[6] M. Franceschet and A. Montanari. Branching within
time: an expressively complete and elementarily de-cidable temporal logic for time granularity.

*Journal ofLanguage and Computation*. To appear.

[7] M. Levine, C. Sawka, and D.M. Bowman. Clinical
practice guidelines for the care and treatment of breastcancer: 8. adjuvant systemic therapy for women withnode-positive breast cancer (2001 update).

*CanadianMedical Association Journal*, 164, 2001.

[8] A. Montanari.

*Metric and Layered Temporal Logic*
*for Time Granularity*. ILLC Dissertation Series 1996-02, Institute for Logic, Language and Computation,University of Amsterdam, 1996.

[9] A. Montanari, A. Peron, and A. Policriti. Extending
Kamp’s theorem to model time granularity.

*Journal ofLogic and Computation*. To appear.

[10] A. Montanari, A. Peron, and A. Policriti.

able theories of

*ω*-layered metric temporal structures.

*Logic Journal of the IGPL*, 7(1):79–102, 1999.

Source: http://sole.dimi.uniud.it/~massimo.franceschet/publications/time02.pdf

PAKISTAN MARINE ACADEMY LIST OF CANDIDATES ELIGIBILE FOR ENTRANCE TEST(NTS) FOR ADMISSION TO 50TH BATCH Father Name Father Name Father Name Father Name Father Name Father Name CHAUDRY NOHSIN ALI JILLANI CHAUDRY WAQAR AHMED Father Name Father Name GULZAR HUSSAIN BANGASH H.SARDAR HUSSAIN (12/02/1991)2037 HAFIZ SYED AHMAD HASSAN SYED IRSHAD AHMAD SHAH Father Name H

CARDIAC MEDICATION INFORMATION FOR ADULT PATIENTS Acyclovir (Brand Names: Zovirax, others) What is this medicine for? - used to prevent or treat infections caused by Herpes viruses or varicella (chickenpox) What is my dose? _________ mg (________ml or ______ tablets/capsules) by mouth every _________ or apply __________ as directed every __________________ How should I take this