@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},
)
@article(AlurETP01,
 author       = {R. Alur and K. Etessami and S. La Torre and D.A.. Peled},
 year         = {2001},
 title        = {Parametric temporal logic for "model measuring"},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {2},
 number       = {3},
 pages        = {388--407},
 doi          = {10.1145/377978.377990},
)
@article(BozzelliL10,
 author       = {L. Bozzelli and R. Lanotte},
 year         = {2010},
 title        = {Complexity and succinctness issues for linear-time hybrid logics},
 journal      = {Theor. Comput. Sci.},
 volume       = {411},
 number       = {2},
 pages        = {454--469},
 doi          = {10.1016/j.tcs.2009.08.009},
)
@article(BozzelliMMP20,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron},
 year         = {2020},
 title        = {Model checking interval temporal logics with regular expressions},
 journal      = {Information and Computation},
 volume       = {272},
 pages        = {104498},
 doi          = {10.1016/j.ic.2019.104498},
)
@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    = {Proc. 8th IJCAR},
 series       = {LNAI 9706},
 publisher    = {Springer},
 pages        = {389--405},
 doi          = {10.1007/978-3-319-40229-1\_27},
)
@article(BozzelliMMPS18,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2018},
 title        = {Model checking for fragments of the interval temporal logic {HS} at the low levels of the polynomial time hierarchy},
 journal      = {Information and Computation},
 volume       = {262},
 number       = {Part},
 pages        = {241--264},
 doi          = {10.1016/j.ic.2018.09.006},
)
@article(BozzelliMMPS19,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2019},
 title        = {Interval vs. {P}oint {T}emporal {L}ogic {M}odel {C}hecking: {A}n {E}xpressiveness {C}omparison},
 journal      = {{ACM} Trans. Comput. Log.},
 volume       = {20},
 number       = {1},
 pages        = {4:1--4:31},
 doi          = {10.1145/3281028},
)
@article(BozzelliMMPS19b,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2019},
 title        = {Which fragments of the interval temporal logic {HS} are tractable in model checking?},
 journal      = {Theor. Comput. Sci.},
 volume       = {764},
 pages        = {125--144},
 doi          = {10.1016/j.tcs.2018.04.011},
)
@article(BozzelliMMPS22,
 author       = {L. Bozzelli and A. Molinari and A. Montanari and A. Peron and P. Sala},
 year         = {2022},
 title        = {Satisfiability and Model Checking for the Logic of Sub-Intervals under the Homogeneity Assumption},
 journal      = {Log. Methods Comput. Sci.},
 volume       = {18},
 number       = {1},
 doi          = {10.46298/lmcs-18(1:24)2022},
)
@article(BozzelliMP21,
 author       = {L. Bozzelli and A. Montanari and A. Peron},
 year         = {2021},
 title        = {Complexity analysis of a unifying algorithm for model checking interval temporal logic},
 journal      = {Inf. Comput.},
 volume       = {280},
 pages        = {104640},
 doi          = {10.1016/j.ic.2020.104640},
)
@inproceedings(BozMPS2021,
 author       = {L. Bozzelli and A. Montanari and A. Peron and P. Sala},
 year         = {2021},
 title        = {Adding the {R}elation {M}eets to the {T}emporal {L}ogic of {P}refixes and {I}nfixes makes it {EXPSPACE}-{C}omplete},
 booktitle    = {Proc. 12th GandALF},
 series       = {{EPTCS} 346},
 pages        = {179--194},
 doi          = {10.4204/EPTCS.346.12},
)
@inproceedings(BozzelliMPS21,
 author       = {L. Bozzelli and A. Montanari and A. Peron and P. Sala},
 year         = {2021},
 title        = {{Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes}},
 booktitle    = {Proc. 28th {TIME}},
 series       = {LIPIcs 206},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
 pages        = {9:1--9:19},
 doi          = {10.4230/LIPIcs.TIME.2021.9},
)
@article(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},
)
@inproceedings(BresolinMSS11,
 author       = {D. Bresolin and A. Montanari and P. Sala and G. Sciavicco},
 year         = {2011},
 title        = {Optimal Tableau Systems for Propositional Neighborhood Logic over All, Dense, and Discrete Linear Orders},
 booktitle    = {Proc. 20th {TABLEAUX}},
 series       = {LNCS 6973},
 publisher    = {Springer},
 pages        = {73--87},
 doi          = {10.1007/978-3-642-22119-4_8},
)
@inproceedings(Clarke81ctl,
 author       = {E.M. Clarke and E.A. Emerson},
 year         = {1981},
 title        = {Design and {S}ynthesis of {S}ynchronization {S}keletons {U}sing {B}ranching {T}ime {T}emporal {L}ogic},
 booktitle    = {Proc. {L}ogics of {P}rograms},
 series       = {LNCS 131},
 pages        = {52--71},
 doi          = {10.1007/BFb0025774},
)
@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},
)
@article(EtessamiVW02,
 author       = {K. Etessami and M.Y. Vardi and T. Wilke},
 year         = {2002},
 title        = {First-{O}rder {L}ogic with {T}wo {V}ariables and {U}nary {T}emporal {L}ogic},
 journal      = {Inf. Comput.},
 volume       = {179},
 number       = {2},
 pages        = {279--295},
 doi          = {10.1006/inco.2001.2953},
)
@inproceedings(FRS03,
 author       = {M. Franceschet and {M. de} Rijke and B.H. Schlingloff},
 year         = {2003},
 title        = {Hybrid {L}ogics on {L}inear {S}tructures: {E}xpressivity and {C}omplexity},
 booktitle    = {Proc. 10th {TIME-ICTL}},
 publisher    = {{IEEE} Computer Society},
 pages        = {166--173},
 doi          = {10.1109/TIME.2003.1214893},
)
@inproceedings(GiampaoloTN10,
 author       = {B. Di Giampaolo and S. La Torre and M. Napoli},
 year         = {2010},
 title        = {Parametric {M}etric {I}nterval {T}emporal {L}ogic},
 booktitle    = {Proc. 4th {LATA}},
 series       = {LNCS 6031},
 publisher    = {Springer},
 pages        = {249--260},
 doi          = {10.1007/978-3-642-13089-2\_21},
)
@article(HS91,
 author       = {J.Y. Halpern and Y. Shoham},
 year         = {1991},
 title        = {A {P}ropositional {M}odal {L}ogic of {T}ime {I}ntervals},
 journal      = {Journal of the ACM},
 volume       = {38(4)},
 pages        = {935--962},
 doi          = {10.1145/115234.115351},
)
@book(kamp1968tense,
 author       = {J.A.W. Kamp},
 year         = {1968},
 title        = {Tense logic and the theory of linear order},
 publisher    = {University of California, Los Angeles},
)
@article(Koymans90,
 author       = {R. Koymans},
 year         = {1990},
 title        = {Specifying Real-Time Properties with Metric Temporal Logic},
 journal      = {Real Time Syst.},
 volume       = {2},
 number       = {4},
 pages        = {255--299},
 doi          = {10.1007/BF01995674},
)
@article(KupfermanPV09,
 author       = {O. Kupferman and N. Piterman and M.Y. Vardi},
 year         = {2009},
 title        = {From liveness to promptness},
 journal      = {Formal Methods Syst. Des.},
 volume       = {34},
 number       = {2},
 pages        = {83--103},
 doi          = {10.1007/s10703-009-0067-z},
)
@inproceedings(Lod00,
 author       = {K. Lodaya},
 year         = {2000},
 title        = {Sharpening the Undecidability of Interval Temporal Logic},
 booktitle    = {Proc. 6th ASIAN},
 series       = {LNCS 1961},
 publisher    = {Springer},
 pages        = {290--298},
 doi          = {10.1007/3-540-44464-5_21},
)
@inproceedings(LM13,
 author       = {A. Lomuscio and J. Michaliszyn},
 year         = {2013},
 title        = {An Epistemic {H}alpern-{S}hoham Logic},
 booktitle    = {Proc. 23rd IJCAI},
 publisher    = {{IJCAI}/{AAAI}},
 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    = {Proc. 21st {ECAI}},
 publisher    = {{IOS} Press},
 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    = {Proc. 15th {KR}},
 publisher    = {{AAAI} Press},
 pages        = {298--308},
 url          = {http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12823},
)
@article(MM14,
 author       = {J. Marcinkowski and J. Michaliszyn},
 year         = {2014},
 title        = {The Undecidability of the Logic of Subintervals},
 journal      = {Fundamenta Informaticae},
 volume       = {131(2)},
 pages        = {217--240},
 doi          = {10.3233/FI-2014-1011},
)
@article(MolinariMMPP16,
 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},
 volume       = {53},
 number       = {6-8},
 pages        = {587--619},
 doi          = {10.1007/s00236-015-0250-1},
)
@inproceedings(MolinariMPS16,
 author       = {Alberto Molinari and Angelo Montanari and Adriano Peron and Pietro Sala},
 year         = {2016},
 title        = {Model Checking Well-Behaved Fragments of {HS:} The (Almost) Final Picture},
 editor       = {Chitta Baral and James P. Delgrande and Frank Wolter},
 booktitle    = {Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, {KR} 2016, Cape Town, South Africa, April 25-29, 2016},
 publisher    = {{AAAI} Press},
 pages        = {473--483},
 url          = {http://www.aaai.org/ocs/index.php/KR/KR16/paper/view/12792},
)
@article(MontanariPS15,
 author       = {A. Montanari and G. Puppis and P. Sala},
 year         = {2015},
 title        = {A decidable weakening of Compass Logic based on cone-shaped cardinal directions},
 journal      = {Logical Methods in Computer Science},
 volume       = {11},
 number       = {4},
 doi          = {10.2168/LMCS-11(4:7)2015},
)
@phdthesis(DigitalCircuitsThesis,
 author       = {B. Moszkowski},
 year         = {1983},
 title        = {Reasoning About Digital Circuits},
 school       = {Dept. of Computer Science, Stanford University},
 address      = {Stanford, CA},
)
@inproceedings(pnueli1977temporal,
 author       = {A. Pnueli},
 year         = {1977},
 title        = {The temporal logic of programs},
 booktitle    = {Proc. 18th {FOCS}},
 publisher    = {{IEEE} Computer Society},
 pages        = {46--57},
 doi          = {10.1109/SFCS.1977.32},
)
@article(Pratt-Hartmann05,
 author       = {Pratt{-}Hartmann, I.},
 year         = {2005},
 title        = {Temporal propositions and their logic},
 journal      = {Artificial Intelligence},
 volume       = {166(1-2)},
 pages        = {1--36},
 doi          = {10.1016/j.artint.2005.04.003},
)
@inproceedings(Queille81verification,
 author       = {J.P. Queille and J. Sifakis},
 year         = {1982},
 title        = {Specification and verification of concurrent programs in {CESAR}},
 booktitle    = {Proc. 5th SP},
 series       = {LNCS 137},
 publisher    = {Springer},
 pages        = {337--351},
 doi          = {10.1007/3-540-11494-7\_22},
)
@article(Roe80,
 author       = {P. Roeper},
 year         = {1980},
 title        = {Intervals and Tenses},
 journal      = {Journal of Philosophical Logic},
 volume       = {9},
 pages        = {451--469},
)
@inproceedings(SW07,
 author       = {T. Schwentick and V. Weber},
 year         = {2007},
 title        = {Bounded-{V}ariable {F}ragments of {H}ybrid {L}ogics},
 booktitle    = {Proc. 24th {STACS}},
 series       = {LNCS 4393},
 volume       = {4393},
 publisher    = {Springer},
 pages        = {561--572},
 doi          = {10.1007/978-3-540-70918-3\_48},
)
@article(Ven90,
 author       = {Y. Venema},
 year         = {1990},
 title        = {Expressiveness and {C}ompleteness of an {I}nterval {T}ense {L}ogic},
 journal      = {Notre Dame Journal of Formal Logic},
 volume       = {31(4)},
 pages        = {529--547},
 doi          = {10.1305/ndjfl/1093635589},
)