@article(AlurH93,
 author       = {R.~Alur and T.~A. Henzinger},
 year         = {1993},
 title        = {Real-Time Logics: Complexity and Expressiveness},
 journal      = {Information and Computation},
 volume       = {104},
 number       = {1},
 pages        = {35--77},
 doi          = {10.1006/inco.1993.1025},
)
@article(AlurH94,
 author       = {R.~Alur and T.~A. Henzinger},
 year         = {1994},
 title        = {{A Really Temporal Logic}},
 journal      = {Journal of the {ACM}},
 volume       = {41},
 number       = {1},
 pages        = {181--204},
 doi          = {10.1145/174644.174651},
)
@inproceedings(BertelloGMR16,
 author       = {M.~Bertello and N.~Gigante and A.~Montanari and M.~Reynolds},
 year         = {2016},
 title        = {Leviathan: {A} New {LTL} Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau},
 booktitle    = {Proc. of the 25\textsuperscript{th} International Joint Conference on Artificial Intelligence},
 publisher    = {{IJCAI/AAAI} Press},
 pages        = {950--956},
)
@book(Tableau99,
 editor       = {M.~D'Agostino and D.M. Gabbay and R.~H{\"a}hnle and J.~Posegga},
 year         = {1999},
 title        = {Handbook of Tableau Methods},
 publisher    = {Springer},
 doi          = {10.1023/A:1017520120752},
)
@inproceedings(DellaMonicaGMSS17,
 author       = {D.~{Della Monica} and N.~Gigante and A.~Montanari and P.~Sala and G.~Sciavicco},
 year         = {2017},
 title        = {Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints},
 booktitle    = {Proc. of the 26\textsuperscript{th} International Joint Conference on Artificial Intelligence},
 pages        = {1008--1014},
 doi          = {10.24963/ijcai.2017/140},
)
@inproceedings(GiganteMR17,
 author       = {N.~Gigante and A.~Montanari and M.~Reynolds},
 year         = {2017},
 title        = {A One-Pass Tree-Shaped Tableau for LTL+Past},
 booktitle    = {Proc.\ of 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning},
 series       = {EPiC Series in Computing},
 volume       = {46},
 pages        = {456--473},
 doi          = {10.29007/3hb9},
)
@inproceedings(KestenMMP93,
 author       = {Y.~Kesten and Z.~Manna and H.~McGuire and A.~Pnueli},
 year         = {1993},
 title        = {{A Decision Algorithm for Full Propositional Temporal Logic}},
 booktitle    = {{Proc. of the 5\textsuperscript{th} International Conference on Computer Aided Verification}},
 series       = {LNCS},
 volume       = {697},
 publisher    = {Springer},
 pages        = {97--109},
 doi          = {10.1007/3-540-56922-7\_9},
)
@article(LichtensteinP00,
 author       = {O.~Lichtenstein and A.~Pnueli},
 year         = {2000},
 title        = {{Propositional Temporal Logics: Decidability and Completeness}},
 journal      = {Logic Journal of the {IGPL}},
 volume       = {8},
 number       = {1},
 pages        = {55--85},
 doi          = {10.1093/jigpal/8.1.55},
)
@book(MannaPnueli95,
 author       = {Z.~Manna and A.~Pnueli},
 year         = {1995},
 title        = {{Temporal Verification of Reactive Systems - Safety}},
 publisher    = {Springer},
 doi          = {10.1007/978-1-4612-4222-2},
)
@inproceedings(McCabeDanstedR17,
 author       = {McCabe{-}Dansted, J.~Christopher and M.~Reynolds},
 year         = {2017},
 title        = {A Parallel Linear Temporal Logic Tableau},
 editor       = {P.~Bouyer and A.~Orlandini and P.~San Pietro},
 booktitle    = {Proceedings 8\textsuperscript{th} International Symposium on Games, Automata, Logics and Formal Verification},
 series       = {{EPTCS}},
 volume       = {256},
 pages        = {166--179},
 doi          = {10.4204/EPTCS.256.12},
)
@inproceedings(Reynolds16a,
 author       = {M.~Reynolds},
 year         = {2016},
 title        = {{A New Rule for {LTL} Tableaux}},
 booktitle    = {Proc. of the 7\textsuperscript{th} International Symposium on Games, Automata, Logics and Formal Verification},
 series       = {{EPTCS}},
 volume       = {226},
 pages        = {287--301},
 doi          = {10.4204/EPTCS.226.20},
)
@inproceedings(Schwendimann98,
 author       = {S.~Schwendimann},
 year         = {1998},
 title        = {A New One-Pass Tableau Calculus for {PLTL}},
 booktitle    = {Proc. of the 7\textsuperscript{th} International Conference on Automated Reasoning with Analytic Tableaux and Related Methods},
 series       = {LNCS},
 volume       = {1397},
 publisher    = {Springer},
 pages        = {277--292},
 doi          = {10.1007/3-540-69778-0\_28},
)