Linear-time temporal logics with Presburger constraints: an overview ★

References

• ABADI , M. 1989 . The power of temporal proofs . Theoretical Computer Science , 65 : 35 – 83 .
   Web of Science ®Google Scholar
• ALUR , R. and DILL , D. 1994 . A theory of timed automata . Theoretical Computer Science , 126 : 183 – 235 .
   Web of Science ®Google Scholar
• ALUR , R. and HENZINGER , T. 1994 . A really temporal logic . Journal of the Association for Computing Machinery , 41 ( 1 ) : 181 – 204 .
   Web of Science ®Google Scholar
• ALUR , R. , FEDER , T. and HENZINGER , T. 1996 . The benefits of relaxing punctuality . Journal of the Association for Computing Machinery , 43 : 116 – 146 .
   Web of Science ®Google Scholar
• BAADER , F. and HANSCHKE , P. 1991 . A scheme for integrating concrete domains into concept languages . 12th International Joint Conference on Artificial Intelligence . 1991 , Sydney , Australia. pp. 452 – 457 .
   Google Scholar
• BALBIANI , P. and CONDOTTA , J. Computational Complexity of propositional linear temporal logics based on qualitative spatial or temporal reasoning . Frontiers of Combining Systems (FroCoS'02), vol. 2309 of Lecture Notes in Artificial Intelligence . Edited by: ARMANDO , A. pp. 162 – 173 . Berlin : Springer .
   Google Scholar
• BARNABA , M. F. and CARO , F. D. 1985 . Graded Modalities . Studia Logica , 44 ( 2 ) : 197 – 221 .
   Google Scholar
• BERTINO , E. , BETTINI , C. , FERRARI , E. and SAMARATI , P. 1996 . Supporting Periodic Authorizations and Temporal Reasoning in Database Access Control . 22nd VLDB . 1996 , Bombay , India. pp. 472 – 483 .
   Google Scholar
• BÉRARD , B. , BIDOIT , M. , FINKEL , A. , LAROUSSINIE , F. , PETIT , A. , PETRUCCI , L. and SCHNOEBELEN , P. 2001 . Systems and Software Verification, Model-Checking Techniques and Tools , Springer-Verlag .
   Google Scholar
• BOIGELOT , B. 1998 . Symbolic methods for exploring infinite state spaces , Université de Liège . PhD thesis
   Google Scholar
• BOIGELOT , B. and WOLPER , P. 2002 . “ Representing arithmetic constraints with finite automata: an overview ” . In ICLP 2002, vol. 2401 of Lecture Notes in Computer Science , Edited by: STUCKEY , P. 1 – 19 . Springer .
   Google Scholar
• BOJAŃ CZYK , M. , MUSCHOLL , A. , SCHWENTICK , T. , SEGOUFIN , L. and DAVID , C. 2006 . “ Two-variable logic on words with data ” . In ICS'06 , 7 – 16 . IEEE .
   Google Scholar
• BONEVA , I. and TALBOT , J. 2005 . “ Automata and Logics for Unranked and Unordered Trees ” . In RTA'05, vol. 3467 of Lecture Notes in Computer Science 500 – 515 .
   Google Scholar
• BOUAJJANI , A. , ECHAHED , R. and HABERMEHL , P. 1995 . On the verification problem of nonregular properties for nonregular processes . LICS'95 , : 123 – 133 .
   Google Scholar
• BOUAJJANI , A. and HABERMEHL , P. 1996 . “ Constrained Properties, Semilinear Sets, And Petri Nets ” . In CONCUR'96, vol. 1119 of Lecture Notes in Computer Science , 481 – 497 . Springer .
   Google Scholar
• BOUAJJANI , A. , ESPARZA , J. and MALER , O. 1997 . “ Reachability Analysis of Pushdown Automata: Application to Model Checking ” . In CONCUR'97, vol. 1243 of LNCS , 135 – 150 . Springer .
   Google Scholar
• BOZZELLI , L. and GASCON , R. 2006 . “ Branching-time temporal logic extended with Presburger constraints ” . In LPAR'06 , Springer . Lecture Notes in Computer Science, to appear
   Google Scholar
• BRESOLIN , D. , MONTANARI , A. and PUPPIS , G. 2004 . “ Time Granularities and Ultimately Periodic Automata ” . In JELIA'04, vol. 3229 of Lecture Notes in Computer Science , 513 – 525 . Springer .
   Google Scholar
• BRUYÈRE , V. , DALL'OLIO , E. and RASKIN , J. 2003 . “ Durations, ParametricModel-Checking in Timed Automata with Presburger Arithmetic ” . In STACS'03, vol. 2607 of Lecture Notes in Computer Science , 687 – 698 . Springer .
   Google Scholar
• BULTAN , T. , GERBER , R. and PUGH , W. 1997 . “ Symbolic model checking of infinite state systems using Presburger arithmetic ” . In CAV'97, vol. 1254 of Lecture Notes in Computer Science , 400 – 411 . Springer .
   Google Scholar
• CALVANESE , D. and GIACOMO , G. D. 2005 . “ Expressive Description Logics ” . In Description Logics Handbook , 178 – 218 . Cambridge University Press .
   Google Scholar
• TEN CATE , B. and FRANCESCHET , M. 2005 . “ On the complexity of hybrid logics with binders ” . In CSL'05, vol. 3634 of Lecture Notes in Computer Science , 339 – 354 . Springer .
   Google Scholar
• ČERĀNS , K. 1994 . “ Deciding Properties of Integral Relational Automata ” . In ICALP-21, vol. 820 of Lecture Notes in Computer Science , 35 – 46 . Berlin : Springer .
   Google Scholar
• CERRITO , S. , MAYER , M. C. and PRAUD , S. First-Order Linear Temporal Logic over Finite Time Structures . 6th Int. Conference on Logic Programming and Automated Reasoning, Tbilisi, Republic of Georgia (LPAR'99), vol. 1705 of Lecture Notes in Computer Science . Edited by: GANZINGER , H. , MCALLESTER , D. and VORONKOV , A. pp. 62 – 76 . Springer .
   Google Scholar
• CHITIC , C. and ROSU , D. 2004 . On validation of XML streams using finite state machines . WebDB, Paris , : 85 – 90 .
   Google Scholar
• COMON , H. and JURSKI , Y. Multiple counters automata, safety analysis and Presburger arithmetic . Proc. Computer Aided Verification, Vancouver, vol. 1427 of Lecture Notes in Computer Science . Edited by: HU , A. and VARDI , M. pp. 268 – 279 . Berlin : Springer .
   Google Scholar
• COMON , H. and CORTIER , V. Flatness is not a weakness . 14 Int. Workshop Computer Science Logic, vol. 1862 of Lecture Notes in Computer Science . pp. 262 – 276 . Springer-Verlag .
   Google Scholar
• COMBI , C. , FRANCESCHET , M. and PERON , A. A logical approach to represent and reason about calendars . Int. Symposium on Temporal Representation and Reasoning . pp. 134 – 140 . IEEE Computer Society Press .
   Google Scholar
• CORTIER , V. 2002 . About the Decision of Reachability for Register Machines . Theoretical Informatics and Applications , 36 ( 4 ) : 341 – 358 .
   Web of Science ®Google Scholar
• DAMS , D. 1999 . Flat fragments of CTL and CTL*: separating the expressive and distinguishing powers . Logic Journal of the IGPL , 7 ( 1 ) : 55 – 78 .
   Google Scholar
• DANG , Z. , PIETRO , P. S. and KEMMERER , R. 2003 . Presburger Liveness Verification of Discrete Timed Automata . Theoretical Computer Science , 299 : 413 – 438 .
   Web of Science ®Google Scholar
• DAVID , C. 2004 . Mots et données infinies , LIAFA . Master's thesis
   Google Scholar
• DECHTER , R. 1992 . From local to global consistency . Artificial Intelligence , 55 : 87 – 107 .
   Web of Science ®Google Scholar
• DEGTYAREV , A. , FISHER , M. and LISITSA , A. 2002 . Equality and monodic first-order temporal logic . Studia Logica , 72 : 147 – 156 .
   Google Scholar
• DEMRI , S. and D'SOUZA , D. 2002 . “ An automata-theoretic approach to constraint LTL ” . In FST&TCS'02, Kanpur, vol. 2556 of Lecture Notes in Computer Science , Edited by: AGRAWAL , M. and SETH , A. 121 – 132 . Berlin : Springer .
   Google Scholar
• DEMRI , S. and D'SOUZA , D. August 2003 . An automata-theoretic approach to constraint LTL , August , LSV . report num. LSV-03-11, 40 pages. Extended version of [DEM 02]. Under submission
   Google Scholar
• DEMRI , S. 2004 . “ LTL over Integer Periodicity Constraints (Extended Abstract) ” . In FOSSACS'04, vol. 2987 of Lecture Notes in Computer Science , Edited by: WALUKIEWICZ , I. 121 – 135 . Berlin : Springer .
   Google Scholar
• DEMRI , S. and GASCON , R. 2005 . Verification of Qualitative ℤ-Constraints . Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), vol. 3653 of Lecture Notes in Computer Science . Aug. 2005 , San Francisco, CA , USA. Edited by: ABADI , M. and DE ALFARO , L. pp. 518 – 532 . Springer .
   Google Scholar
• DEMRI , S. , LAZIĆ , R. and NOWAK , D. On the freeze quantifier in constraint LTL: decidability and complexity . 12th Int. Symp. on Temporal Representation and Reasoning . Burlington , Vermont . pp. 113 – 121 . IEEE Computer Society Press .
   Google Scholar
• DEMRI , S. and NOWAK , D. 2005 . “ Reasoning about transfinite sequences (extended abstract) ” . In ATVA'05, vol. 3707 of Lecture Notes in Computer Science , 248 – 262 . Springer .
   Google Scholar
• DEMRI , S. 2006 . LTL over integer periodicity constraints . Theoretical Computer Science , 360 ( 1–3 ) : 96 – 123 .
   Web of Science ®Google Scholar
• DEMRI , S. , FINKEL , A. , GORANKO , V. and VAN DRIMMELEN , G. 2006 . Towards a modelchecker for counter systems . Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA'06), vol. 4218 of Lecture Notes in Computer Science . 2006 , Beijing , ROC. pp. 493 – 507 . Springer .
   Google Scholar
• DEMRI , S. and GASCON , R. 2006 . The effects of bounding syntactic resourses on Presburger LTL , LSV . report num. LSV-06-5, 36 pages
   Google Scholar
• DEMRI , S. and LAZIĆ , R. 2006 . “ LTL with the freeze quantifier and register automata ” . In LICS'06 , 17 – 26 . IEEE .
   Google Scholar
• DEMRI , S. , LAZIĆ , R. and NOWAK , D. 2006 . On the freeze quantifier in constraint LTL: decidability and complexity . Information and Computation , to appear. Extended version of [DEM 05b]
   Web of Science ®Google Scholar
• DEMRI , S. and LUGIEZ , D. Presburger Modal Logic is PSPACE-complete . 3rd International Joint Conference on Automated Reasoning (IJCAR'06), Seattle, vol. 4130 of Lecture Notes in Computer Science . pp. 541 – 556 . Springer .
   Google Scholar
• DEUTSCH , A. , SUI , L. and VIANU , V. 2004 . Specification and verification of data-driven web services . PODS'04, Paris , : 71 – 82 .
   Google Scholar
• FINE , K. 1972 . In so many possible worlds . Notre Dame Journal of Formal Logic , 13 ( 4 ) : 516 – 520 .
   Google Scholar
• FINKEL , A. , WILLEMS , B. and WOLPER , P. 1997 . “ A Direct Symbolic Approach to Model Checking Pushdown Systems (Extended Abstract) ” . In INFINITY'97, vol. 9 of ENTCS , Elsevier Science .
   Google Scholar
• FINKEL , A. and SUTRE , G. Decidability of reachability problems for classes of two counters automata . 17th Ann. Symp. Theoretical Aspects of Computer Science, vol. 2256 of Lecture Notes in Computer Science . pp. 346 – 357 . Springer-Verlag .
   Google Scholar
• FINKEL , A. and LEROUX , J. 2002 . “ How to compose Presburger accelerations: Applications to broadcast protocols ” . In FST&TCS'02, Kanpur, vol. 2256 of Lecture Notes in Computer Science , Edited by: AGRAWAL , M. and SETH , A. 145 – 156 . Berlin : Springer .
   Google Scholar
• FISCHER , M. and RABIN , M. Super-exponential complexity of Presburger arithmetic . Complexity of Computation, vol. 7 of SIAM-AMS proceedings . Edited by: KARP , R. pp. 27 – 42 . American Mathematical Society .
   Google Scholar
• FITTING , M. 2002 . Modal logic between propositional and first-order . Journal of Logic and Computation , 12 ( 6 ) : 1017 – 1026 .
   Web of Science ®Google Scholar
• FRENCH , T. 2003 . “ Quantified Propositional Temporal Logic with Repeating States ” . In TIME-ICTL 2003 , 155 – 165 . IEEE Computer Society .
   Google Scholar
• GABBAY , D. , KURUCZ , A. , WOLTER , F. and ZAKHARYASCHEV , M. 2003 . Manydimensional modal logics: theory and practice , Cambridge University Press .
   Google Scholar
• GABELAIA , D. , KONTCHAKOV , R. , KURUCZ , A. , WOLTER , F. and ZAKHARYASCHEV , M. 2003 . “ On the computational complexity of spatio-temporal logics ” . In FLAIRS'03, St Augustine, Florida 460 – 464 .
   Google Scholar
• GASTIN , P. and KUSKE , D. 2003 . “ Satisfiability and model checking for MSO-definable temporal logics are in PSPACE ” . In CONCUR'03, vol. 2761 of Lecture Notes in Computer Science , 222 – 236 . Springer .
   Google Scholar
• GASCON , R. Verifying qualitative and quantitative properties with LTL over concrete domains . Proceedings of the 4th Workshop on Methods for Modalities (M4M'05), vol. 194 of Informatik Bericht . pp. 54 – 61 . Humboldt Universität zu Berlin .
   Google Scholar
• GINSBURG , S. and SPANIER , E. 1966 . Semigroups, Presburger formulas and languages . Pacific Journal of Mathematics , 16 ( 2 ) : 285 – 296 .
   Web of Science ®Google Scholar
• HENZINGER , T. Half-order modal logic: how to prove real-time properties . 9th Annual ACM Symposium on Principles of Distributed Computing . pp. 281 – 296 . ACM Press .
   Google Scholar
• HIRSHFELD , Y. and RABINOVICH , A. 2003 . Future temporal logic needs infinitely many modalities . Information and Computation , 187 ( 2 ) : 196 – 208 .
   Web of Science ®Google Scholar
• HIRSHFELD , Y. and RABINOVICH , A. 2004 . Logics for real time: decidability and complexity . Fundamenta Informaticae , 62 : 1 – 28 .
   Web of Science ®Google Scholar
• HODKINSON , I. , KONTCHAKOV , R. , KURUCZ , A. , WOLTER , F. and ZAKHARYASCHEV , M. On the computational complexity of decidable fragments of first-order linear temporal logics . 10th Int. Symp. Temporal Representation and Reasoning and 4th Int. Conf. Temporal Logic (TIME-ICTL) . pp. 91 – 98 . IEEE .
   Google Scholar
• VAN DER HOEK , W. and DE RIJKE , M. 1995 . Counting objects . Journal of Logic and Computation , 5 ( 3 ) : 325 – 345 .
   Google Scholar
• HOLLUNDER , B. and BAADER , F. 1991 . “ Qualifying number restrictions in concept languages ” . In KR'91 335 – 346 .
   Google Scholar
• IBARRA , O. 1978 . Reversal-bounded multicounter machines and their decision problems . Journal of the Association for Computing Machinery , 25 ( 1 ) : 116 – 133 .
   Web of Science ®Google Scholar
• IBARRA , O. , SU , J. , DANG , Z. , BULTAN , T. and KEMMERER , A. 2000 . “ Counter Machines: Decidable Properties and Applications to Verification Problems ” . In MFCS'00, vol. 1893 of Lecture Notes in Computer Science , 426 – 435 . Springer .
   Google Scholar
• IBARRA , O. and DANG , Z. On removing the stack from reachability constructions . International Symposium on Algorithms and Computation (ISAAC'01), vol. 2223 of Lecture Notes in Computer Science . Edited by: EADES , P. and TAKAOKA , T. pp. 244 – 256 . Springer .
   Google Scholar
• KAMP , J. 1968 . Tense Logic and the theory of linear order , USA : UCLA . PhD thesis
   Google Scholar
• KRÖ;GER , F. 1990 . On the interpretability of arithmetic in temporal logic . Theoretical Computer Science , 73 : 47 – 61 .
   Web of Science ®Google Scholar
• LAFOURCADE , P. , LUGIEZ , D. and TREINEN , R. 2005 . “ Intruder deduction for AC-like equational theories with homomorphisms ” . In RTA'05, vol. 3467 of Lecture Notes in Computer Science , 308 – 322 . Springer .
   Google Scholar
• LAGO , U. D. and MONTANARI , A. Calendars, time granularities, and automata . Int. Symposium on Spatial and Temporal Databases, vol. 2121 of Lecture Notes in Computer Science . pp. 279 – 298 . Berlin : Springer .
   Google Scholar
• LAGO , U. D. , MONTANARI , A. and PUPPIS , G. 2003 . “ Towards compact and tractable automaton-based representations of time granularities ” . In ICTCS 2003, vol. 2841 of Lecture Notes in Computer Science , 72 – 85 . Berlin : Springer .
   Google Scholar
• LEROUX , J. and SUTRE , G. 2005 . “ Flat counter systems are everywhere! ” . In ATVA'05, vol. 3707 of Lecture Notes in Computer Science , Springer .
   Google Scholar
• LICHTENSTEIN , O. and PNUELI , A. 2000 . Propositional Temporal Logics: Decidability and Completeness . Logic Journal of the IGPL , 8 ( 1 ) : 55 – 85 .
   Google Scholar
• LISITSA , A. and POTAPOV , I. Temporal logic with predicate δ-abstraction . 12th Int. Symp. on Temporal Representation and Reasoning . Burlington , Vermont . pp. 147 – 155 . IEEE Computer Society Press .
   Google Scholar
• LUTZ , C. 2003 . “ Description Logics with Concrete Domains—A Survey ” . In Advances in Modal Logics Volume 4 , 265 – 296 . King's College Publications .
   Google Scholar
• LUTZ , C. 2004 . NEXPTIME-complete description logics with concrete domains . ACM Transactions on Computational Logic , 5 ( 4 ) : 669 – 705 .
   Google Scholar
• LUTZ , C. and MILIČIĆ , M. 2005 . “ A Tableau algorithm for description logics with concrete domains and GCIs ” . In TABLEAUX'05, vol. 3702 of Lecture Notes in Computer Science , 201 – 216 . Springer .
   Google Scholar
• LUTZ , C. , WALTHER , D. and WOLTER , F. 2005 . “ Quantitative temporal logics: PSPACE and below ” . In TIME'05 138 – 146 .
   Google Scholar
• MINSKY , M. 1967 . Computation, Finite and Infinite Machines , Prentice Hall .
   Google Scholar
• MÜLLER-OLM , M. and SEIDL , H. 2005 . “ Analysis of Modular Arithmetic ” . In ESOP'05, vol. 3444 of Lecture Notes in Computer Science , 46 – 60 . Springer .
   Google Scholar
• NIEZETTE , M. and STEVENNE , J. An efficient symbolic representation of periodic time . Proc. of the International Conference on Information and Knowledge Management, Baltimore, Maryland, vol. 752 ofLecture Notes in Computer Science . pp. 161 – 168 . Springer .
   Google Scholar
• OHSAKI , H. , TALBOT , J. , TISON , S. and ROOS , Y. Monotone AC-Tree Automata . 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR'05), Montego Bay (Jamaica), vol. 3835 of Lecture Notes in Artificial Intelligence . pp. 337 – 351 . Springer .
   Google Scholar
• PACUIT , E. and SALAME , S. 2004 . “ Majority logic ” . In KR'04 , 598 – 605 . AAAI Press .
   Google Scholar
• PNUELI , A. The temporal logic of programs . 18th Annual Symposium on Foundations of Computer Science . pp. 46 – 57 . IEEE Computer Society Press .
   Google Scholar
• POTAPOV , I. 2004 . “ From Post Systems to the Reachability Problems for Matrix Semigroups and Multicounter Automata ” . In DTL'04, vol. 3340 of Lecture Notes in Computer Science , 345 – 356 . Springer .
   Google Scholar
• PRESBURGER , M. 1929 . “ Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt ” . In Comptes Rendus du premier congrès de mathématiciens des Pays Slaves, Warszawa 92 – 101 .
   Google Scholar
• PUPPIS , G. March 2006 . Automata for branching and layered temporal structures , March , Universitá Degli Studi Di Udine . PhD thesis
   Google Scholar
• REVESZ , P. 2002 . Introduction to Constraint Databases , New York : Springer .
   Google Scholar
• REYNOLDS , M. 2003 . The complexity of the temporal logic with until over general linear time . Journal of Computer and System Sciences , 66 ( 2 ) : 393 – 426 .
   Web of Science ®Google Scholar
• SCHNOEBELEN , P. 2002 . Verifying lossy channel systems has nonprimitive recursive complexity . Information Processing Letters , 83 ( 5 ) : 251 – 261 .
   Web of Science ®Google Scholar
• SCHNOEBELEN , P. 2003 . “ The complexity of temporal logic model checking ” . In Advances in Modal Logic, vol. 4, selected papers from 4th Conf. Advances in Modal Logic (AiML'2002), Sep.-Oct. 2002, Toulouse, France , 437 – 459 . King's College Publication .
   Google Scholar
• SCHRÖDER , L. and PATTINSON , D. 2006 . “ PSPACE bounds for rank-1 modal logics ” . In CS'06 , 231 – 240 . IEEE .
   Google Scholar
• SEIDL , H. , SCHWENTICK , T. , MUSCHOLL , A. and HABERMEHL , P. 2004 . “ Counting in Trees for free ” . In ICALP'04, vol. 3142 of Lecture Notes in Computer Science 1136 – 1149 . http://www.mathematik.uni-marburg.de/~tick/
   Google Scholar
• SERRE , O. 2004 . Contribution à l'étude des jeux sur des graphes de processus de pile , Université Paris 7 - Denis Diderot . PhD thesis
   Google Scholar
• SERRE , O. 2006 . “ Parity games played on transition graphs of one-counter processes ” . In FOSSACS'06, vol. 3921 of Lecture Notes in Computer Science , 337 – 351 . Springer .
   Google Scholar
• SISTLA , A. and CLARKE , E. 1985 . The complexity of propositional linear temporal logic . Journal of the Association for Computing Machinery , 32 ( 3 ) : 733 – 749 .
   Web of Science ®Google Scholar
• TOMAN , D. and CHOMICKI , J. 1998 . DATALOG with integer periodicity constraints . Journal of Logic Programming , 35 ( 3 ) : 263 – 290 .
   Google Scholar
• TRAHTENBROT , B. 1963 . Impossibility of an algorithm for the decision problem in finite classes . AmericanMathematical Society - Translation Series , 23 ( 2 ) : 1 – 5 .
   Google Scholar
• VARDI , M. A temporal fixpoint calculus . 15th Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages . San Diego . pp. 250 – 259 . ACM .
   Google Scholar
• VARDI , M. and WOLPER , P. 1994 . Reasoning about Infinite Computations . Information and Computation , 115 : 1 – 37 .
   Web of Science ®Google Scholar
• WAKATSUKI , M. , TERAGUCHI K. and TOMITA , E. Polynomial time identification of strict deterministic restricted one-counter automata in some class from positive data . International Colloquium on Grammatical Inference (ICGI 2004), Athens, vol. 3264 of Lecture Notes in Artificial Intelligence . pp. 260 – 272 . Springer .
   Google Scholar
• WALUKIEWICZ , I. 2001 . Pushdown processes: games and model-checking . Information and Computation , 164 ( 2 ) : 234 – 263 .
   Web of Science ®Google Scholar
• WIJSEN , J. A string based-model for infinite granularities . AAAI Workshop on Spatial and Temporal Granularity . pp. 9 – 16 . AAAI Press .
   Google Scholar
• WOLPER , P. 1983 . Temporal logic can be more expressive . Information and Computation , 56 : 72 – 99 .
   Google Scholar
• WOLTER , F. and ZAKHARYASCHEV , M. 2000 . “ Spatio-temporal representation and reasoning based on RCC-8 ” . In KR'00 3 – 14 .
   Google Scholar
• WOLTER , F. and ZAKHARYASCHEV , M. 2002 . Axiomatizing the monodic fragment of firstorder temporal logic . Annals of Pure and Applied Logic , 118 ( 133–145 )
   Google Scholar
• ZILIO , S. D. and LUGIEZ , D. 2006 . XML schema, tree logic and sheaves automata . Applicable Algebra in Engineering, Communication and Computing (AAECC) , to appear
   Web of Science ®Google Scholar