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 G1 is finer than time granularity, while in Section 4 we compare our work granularity G2 or G1 is equivalent to G2). 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 = {G1, . . . , 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 → 2P 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 thatG(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}, andG(i) = ∅ as ¬(¬φ ∧ ¬ψ), ¬φ ∨ ψ, and (φ → ψ) ∧ (ψ → φ), Moreover, Fp (p will hold in the future), • The structure (N, <, V ) such that V (0) = {PG}, Gp (p will always hold in the future), Pp (p held in the V (1) = {QG, PG}, V (2) = {QG} does not induce past) and Hp (p always held in the past) are shorthands for, respectively, trueUp, ¬F¬p, trueSp and ¬P¬p, where the calendar G may be captured in our framework. For true = P ∨ ¬P , for some P ∈ P.
instance, G1 GroupInto G2 (each granule of G2 is ob- We interpret PPLTL over P-labelled linear time struc- tained by grouping granules of G1), G1 FinerThan G2 tures. The semantics of PPLTL is as follows.
(each granule of G1 is contained in some granule of G2),G1 SubGranularityOf G2 (each granule of G1 is equal Definition 3.5 (Semantics of PPLTL)
to a granule of G2) [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 η(G1) ∧ η(G2) ∧ 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 symbolsPH 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 Gis 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 ∧ ¬XPG ∧ XXPG)). 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, Xn(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 Xn(p) = XXn−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 ∧ ¬XPG ∧ XXPG))). 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) = ¬pU(p ∧ X(Count(p, k − 1))).
dar G = {G1, . . . , Gn}, the formula The formula ΩCMF below defines, on the time domain the set of all calendars with n granularities G1, . . . , 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 ) ∧ X27QCMF )) ∧ can verify whether it encodes a set of well-defined granular- G((QCMF ∧ FPCMF ) → ∃[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)SPG ∧ ¬(PG ∨ QG)UQG) 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