@Article{Markey2003, author = {Markey, Nicolas}, title = {Temporal logic with past is exponentially more succinct}, journal = {EATCS Bulletin}, year = {2003}, volume = {79}, pages = {122--128}, publisher = {European Association for Theoretical Computer Science}, } @InProceedings{Gabbay1989, author = {Gabbay, Dov}, title = {The declarative past and imperative future: executable temporal logic for interactive systems}, booktitle = {Temporal logic in specification}, year = {1989}, organization = {Springer}, pages = {409--448}, } @InProceedings{Lichtenstein1985, author = {Lichtenstein, Orna and Pnueli, Amir and Zuck, Lenore}, title = {The glory of the past}, booktitle = {Workshop on Logic of Programs}, year = {1985}, organization = {Springer}, pages = {196--218}, } @InProceedings{Gabbay1980, author = {Gabbay, Dov and Pnueli, Amir and Shelah, Saharon and Stavi, Jonathan}, title = {On the temporal analysis of fairness}, booktitle = {Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, year = {1980}, organization = {ACM}, pages = {163--173}, } @Article{Moser1994, author = {Moser, Louise E. and Melliar-Smith, PM and Kutty, George and Ramakrishna, YS}, title = {Completeness and soundness of axiomatizations for temporal logics without next}, journal = {Fundamenta Informaticae}, year = {1994}, volume = {21}, number = {4}, pages = {257--305}, publisher = {IOS Press}, } @InProceedings{Laroussinie2002, author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Schnoebelen, Philippe}, title = {Temporal logic with forgettable past}, booktitle = {Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on}, year = {2002}, organization = {IEEE}, pages = {383--392}, } @Book{Prior1957, author = {Prior, Arthur N}, title = {Time and modality}, year = {1957}, publisher = {Clarendon Press}, } @inproceedings{FiterauBrostean2017, author = {Fiterau-Brostean, Paul and Lenaerts, Toon and Poll, Erik and De Ruiter, Joeri and Vaandrager, Frits and Verleg, Patrick}, title = {Model Learning and Model Checking of SSH Implementations}, booktitle = {Proceedings 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 13--14 July 2017, Santa Barbara, USA}, year = 2017, pages = {142--151} } @inproceedings{Havelund2002, author = {Havelund, Klaus and Ro\c{s}u, Grigore}, title = {Synthesizing Monitors for Safety Properties}, booktitle = {International Conference on Tools and Algorithms for the Contruction and Analysis of Systems, TACAS 2002}, year = 2002, pages = {342--356} } @article{Etessami2002, author = {Etessami, Kousha and Vardi, Moshe Y. and Wilke, Thomas}, title = {First-Order Logic with Two Variables and Unary Temporal Logic}, journal = {Information and Computation}, volume = 179, issue = 2, year = 2002, pages = {279--295} }