@article(All83,
 author       = {J. F. Allen},
 year         = {1983},
 title        = {Maintaining Knowledge about Temporal Intervals},
 journal      = {Communications of the ACM},
 volume       = {26(11)},
 pages        = {832--843},
 doi          = {10.1145/182.358434},
)
@inproceedings(bmmps16,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2016},
 title        = {{Interval Temporal Logic Model Checking: the Border Between Good and Bad HS Fragments}},
 booktitle    = {IJCAR},
 series       = {LNAI 9706},
 publisher    = {Springer},
 pages        = {389--405},
 doi          = {10.1007/978-3-319-40229-1\_27},
 url          = {https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/1.2016/},
)
@techreport(techrep,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2016},
 title        = {{Model Checking the Logic of Allen's Relations Meets and Started-by is $\PTIME^{\NP}$-Complete}},
 type         = {Technical Report},
 institution  = {University of Udine, Udine, Italy},
 url          = {https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/3488/},
)
@article(DBLP:journals/amai/BresolinMGMS14,
 author       = {D. Bresolin and {Della Monica}, D. and V. Goranko and A. Montanari and G. Sciavicco},
 year         = {2014},
 title        = {The dark side of interval temporal logic: marking the undecidability border},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 volume       = {71(1-3)},
 pages        = {41--83},
 doi          = {10.1007/s10472-013-9376-4},
)
@article(BGMS10,
 author       = {D. Bresolin and V. Goranko and A. Montanari and P. Sala},
 year         = {2010},
 title        = {Tableaux for Logics of Subinterval Structures over Dense Orderings},
 journal      = {Journal of Logic and Computation},
 volume       = {20(1)},
 pages        = {133--166},
 doi          = {10.1093/logcom/exn063},
)
@article(BGMS09,
 author       = {D. Bresolin and V. Goranko and A. Montanari and G. Sciavicco},
 year         = {2009},
 title        = {Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {161(3)},
 pages        = {289--304},
 doi          = {10.1016/j.apal.2009.07.003},
)
@article(emerson1986sometimes,
 author       = {E. A. Emerson and J. Y. Halpern},
 year         = {1986},
 title        = {``{S}ometimes'' and ``not never'' revisited: on branching versus linear time temporal logic},
 journal      = {Journal of the ACM},
 volume       = {33},
 number       = {1},
 pages        = {151--178},
 doi          = {10.1145/4904.4999},
)
@inproceedings(DBLP:conf/ecp/GiunchigliaT99,
 author       = {F. Giunchiglia and P. Traverso},
 year         = {1999},
 title        = {Planning as Model Checking},
 booktitle    = {ECP},
 series       = {LNCS 1809},
 publisher    = {Springer},
 pages        = {1--20},
 doi          = {10.1007/10720246\_1},
)
@article(gottlob1995,
 author       = {G. Gottlob},
 year         = {1995},
 title        = {{NP} {T}rees and {C}arnap's {M}odal {L}ogic},
 journal      = {Journal of the ACM},
 volume       = {42},
 number       = {2},
 pages        = {421--457},
 doi          = {10.1145/201019.201031},
)
@article(HS91,
 author       = {J. Y. Halpern and Y. Shoham},
 year         = {1991},
 title        = {A Propositional Modal Logic of Time Intervals},
 journal      = {Journal of the ACM},
 volume       = {38(4)},
 pages        = {935--962},
 doi          = {10.1145/115234.115351},
)
@inproceedings(LMS01,
 author       = {F. Laroussinie and N. Markey and P. Schnoebelen},
 year         = {2001},
 title        = {Model Checking {CTL}$^+$ and {FCTL} is Hard},
 booktitle    = {{FOSSACS}},
 pages        = {318--331},
 doi          = {10.1007/3-540-45315-6\_21},
)
@inproceedings(LM13,
 author       = {A. Lomuscio and J. Michaliszyn},
 year         = {2013},
 title        = {An Epistemic {H}alpern-{S}hoham Logic},
 booktitle    = {IJCAI},
 pages        = {1010--1016},
)
@inproceedings(LM14,
 author       = {A. Lomuscio and J. Michaliszyn},
 year         = {2014},
 title        = {Decidability of model checking multi-agent systems against a class of {EHS} specifications},
 booktitle    = {{ECAI}},
 pages        = {543--548},
 doi          = {10.3233/978-1-61499-419-0-543},
)
@inproceedings(LM16,
 author       = {A. Lomuscio and J. Michaliszyn},
 year         = {2016},
 title        = {Model Checking Multi-Agent Systems against Epistemic {HS} Specifications with Regular Expressions},
 booktitle    = {{KR}},
 pages        = {298--308},
)
@inproceedings(DBLP:conf/tacas/LomuscioR06,
 author       = {A. Lomuscio and H. Qu and F. Raimondi},
 year         = {2009},
 title        = {{MCMAS}: A Model Checker for the Verification of Multi-Agent Systems},
 booktitle    = {CAV},
 publisher    = {Springer},
 pages        = {682--688},
 doi          = {10.1007/978-3-642-02658-4\_55},
)
@article(MMMPP15,
 author       = {A. Molinari and A. Montanari and A. Murano and G. Perelli and A. Peron},
 year         = {2016},
 title        = {Checking interval properties of computations},
 journal      = {Acta Informatica},
 doi          = {10.1007/s00236-015-0250-1},
 url          = {http://arxiv.org/abs/1601.03195},
 note         = {Accepted for publication},
)
@inproceedings(MMP15B,
 author       = {A. Molinari and A. Montanari and A. Peron},
 year         = {2015},
 title        = {{Complexity of ITL model checking: some well-behaved fragments of the interval logic HS}},
 booktitle    = {TIME},
 pages        = {90--100},
 doi          = {10.1109/TIME.2015.12},
 url          = {http://arxiv.org/abs/1601.03202},
)
@inproceedings(MMP15,
 author       = {A. Molinari and A. Montanari and A. Peron},
 year         = {2015},
 title        = {A Model Checking Procedure for Interval Temporal Logics based on Track Representatives},
 booktitle    = {CSL},
 pages        = {193--210},
 doi          = {10.4230/LIPIcs.CSL.2015.193},
)
@inproceedings(MMPS16,
 author       = {A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2016},
 title        = {{Model Checking Well-Behaved Fragments of HS: the (Almost) Final Picture}},
 booktitle    = {KR},
 pages        = {473--483},
)
@phdthesis(digital_circuits_thesis,
 author       = {B. Moszkowski},
 year         = {1983},
 title        = {Reasoning About Digital Circuits},
 school       = {Stanford University},
 address      = {Stanford, CA},
)
@inproceedings(pnueli1977temporal,
 author       = {A. Pnueli},
 year         = {1977},
 title        = {The temporal logic of programs},
 booktitle    = {FOCS},
 organization = {IEEE Computer Society},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@article(DBLP:journals/ai/Pratt-Hartmann05,
 author       = {Pratt{-}Hartmann, I.},
 year         = {2005},
 title        = {Temporal prepositions and their logic},
 journal      = {Artificial Intelligence},
 volume       = {166(1-2)},
 pages        = {1--36},
 doi          = {10.1016/j.artint.2005.04.003},
)
@article(Roe80,
 author       = {P. Roeper},
 year         = {1980},
 title        = {Intervals and Tenses},
 journal      = {J. of Philosophical Logic},
 volume       = {9},
 pages        = {451--469},
 doi          = {10.1007/BF00262866},
)
@inproceedings(schnoebelen2003,
 author       = {P. Schnoebelen},
 year         = {2003},
 title        = {Oracle Circuits for Branching-Time Model Checking},
 booktitle    = {ICALP},
 series       = {LNCS 2719},
 publisher    = {Springer},
 pages        = {790--801},
 doi          = {10.1007/3-540-45061-0\_62},
)
@book(DBLP:series/eatcs/ChaochenH04,
 author       = {C. Zhou and M. R. Hansen},
 year         = {2004},
 title        = {Duration Calculus - {A} Formal Approach to Real-Time Systems},
 series       = {Monographs in Theoretical Computer Science. An {EATCS} Series},
 publisher    = {Springer},
)