L. Bozzelli, A. Molinari, A. Montanari, A. Peron & P. Sala (2016):
Model Checking the Logic of Allen's Relations Meets and Started-by is ^-Complete.
Technical Report.
University of Udine, Udine, Italy.
Available at https://www.dimi.uniud.it/la-ricerca/pubblicazioni/preprints/3488/.
D. Bresolin, D. Della Monica, V. Goranko, A. Montanari & G. Sciavicco (2014):
The dark side of interval temporal logic: marking the undecidability border.
Annals of Mathematics and Artificial Intelligence 71(1-3),
pp. 41–83,
doi:10.1007/s10472-013-9376-4.
D. Bresolin, V. Goranko, A. Montanari & P. Sala (2010):
Tableaux for Logics of Subinterval Structures over Dense Orderings.
Journal of Logic and Computation 20(1),
pp. 133–166,
doi:10.1093/logcom/exn063.
D. Bresolin, V. Goranko, A. Montanari & G. Sciavicco (2009):
Propositional interval neighborhood logics: Expressiveness, decidability, and undecidable extensions.
Annals of Pure and Applied Logic 161(3),
pp. 289–304,
doi:10.1016/j.apal.2009.07.003.
E. A. Emerson & J. Y. Halpern (1986):
``Sometimes'' and ``not never'' revisited: on branching versus linear time temporal logic.
Journal of the ACM 33(1),
pp. 151–178,
doi:10.1145/4904.4999.
F. Giunchiglia & P. Traverso (1999):
Planning as Model Checking.
In: ECP,
LNCS 1809.
Springer,
pp. 1–20,
doi:10.1007/10720246_1.
G. Gottlob (1995):
NP Trees and Carnap's Modal Logic.
Journal of the ACM 42(2),
pp. 421–457,
doi:10.1145/201019.201031.
J. Y. Halpern & Y. Shoham (1991):
A Propositional Modal Logic of Time Intervals.
Journal of the ACM 38(4),
pp. 935–962,
doi:10.1145/115234.115351.
F. Laroussinie, N. Markey & P. Schnoebelen (2001):
Model Checking CTL^+ and FCTL is Hard.
In: FOSSACS,
pp. 318–331,
doi:10.1007/3-540-45315-6_21.
A. Lomuscio & J. Michaliszyn (2013):
An Epistemic Halpern-Shoham Logic.
In: IJCAI,
pp. 1010–1016.
A. Lomuscio & J. Michaliszyn (2014):
Decidability of model checking multi-agent systems against a class of EHS specifications.
In: ECAI,
pp. 543–548,
doi:10.3233/978-1-61499-419-0-543.
A. Lomuscio & J. Michaliszyn (2016):
Model Checking Multi-Agent Systems against Epistemic HS Specifications with Regular Expressions.
In: KR,
pp. 298–308.
A. Lomuscio, H. Qu & F. Raimondi (2009):
MCMAS: A Model Checker for the Verification of Multi-Agent Systems.
In: CAV.
Springer,
pp. 682–688,
doi:10.1007/978-3-642-02658-4_55.
A. Molinari, A. Montanari, A. Murano, G. Perelli & A. Peron (2016):
Checking interval properties of computations.
Acta Informatica,
doi:10.1007/s00236-015-0250-1.
Available at http://arxiv.org/abs/1601.03195.
Accepted for publication.
A. Molinari, A. Montanari & A. Peron (2015):
Complexity of ITL model checking: some well-behaved fragments of the interval logic HS.
In: TIME,
pp. 90–100,
doi:10.1109/TIME.2015.12.
Available at http://arxiv.org/abs/1601.03202.
A. Molinari, A. Montanari & A. Peron (2015):
A Model Checking Procedure for Interval Temporal Logics based on Track Representatives.
In: CSL,
pp. 193–210,
doi:10.4230/LIPIcs.CSL.2015.193.
A. Molinari, A. Montanari, A. Peron & P. Sala (2016):
Model Checking Well-Behaved Fragments of HS: the (Almost) Final Picture.
In: KR,
pp. 473–483.
B. Moszkowski (1983):
Reasoning About Digital Circuits.
Stanford University,
Stanford, CA.
A. Pnueli (1977):
The temporal logic of programs.
In: FOCS.
IEEE Computer Society,
pp. 46–57,
doi:10.1109/SFCS.1977.32.
I. Pratt-Hartmann (2005):
Temporal prepositions and their logic.
Artificial Intelligence 166(1-2),
pp. 1–36,
doi:10.1016/j.artint.2005.04.003.
P. Roeper (1980):
Intervals and Tenses.
J. of Philosophical Logic 9,
pp. 451–469,
doi:10.1007/BF00262866.
P. Schnoebelen (2003):
Oracle Circuits for Branching-Time Model Checking.
In: ICALP,
LNCS 2719.
Springer,
pp. 790–801,
doi:10.1007/3-540-45061-0_62.
C. Zhou & M. R. Hansen (2004):
Duration Calculus - A Formal Approach to Real-Time Systems.
Monographs in Theoretical Computer Science. An EATCS Series.
Springer.
eptcs@eptcs.org