@Article{Meyer1969,
  title={A note on star-free events},
  author={Meyer, Albert R},
  journal={Journal of the ACM (JACM)},
  volume={16},
  number={2},
  pages={220--225},
  year={1969},
  publisher={ACM}
}

@Article{Krohn1965,
  title={Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines},
  author={Krohn, Kenneth and Rhodes, John},
  journal={Transactions of the American Mathematical Society},
  volume={116},
  pages={450--464},
  year={1965},
  publisher={JSTOR}
}

@InCollection{Maler2010,
  title={On the krohn-rhodes cascaded decomposition theorem},
  author={Maler, Oded},
  booktitle={Time for verification},
  pages={260--278},
  year={2010},
  publisher={Springer}
}

@InCollection{Roggenbach2002,
  title={Determinization of B{\"u}chi-automata},
  author={Roggenbach, Markus},
  booktitle={Automata logics, and infinite games},
  pages={43--60},
  year={2002},
  publisher={Springer}
}

@Article{McNaughton1966,
  title={Testing and generating infinite sequences by a finite automaton},
  author={McNaughton, Robert},
  journal={Information and control},
  volume={9},
  number={5},
  pages={521--530},
  year={1966},
  publisher={Elsevier}
}

@InProceedings{Maler1990,
  title={Tight bounds on the complexity of cascaded decomposition of automata},
  author={Maler, Oded and Pnueli, Amir},
  booktitle={Foundations of Computer Science, 1990. Proceedings., 31st Annual Symposium on},
  pages={672--682},
  year={1990},
  organization={IEEE}
}

@InProceedings{Maler1994,
  title={On the Cascaded Decomposition of Automata, its Complexity and its Application to Logic},
  author={Maler, Oded and Pnueli, Amir},
  booktitle={ACTS Mobile Communication},
  year={1994},
  organization={Citeseer}
}

@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},
}

@phdthesis{Kamp1968,
  title={Tense logic and the theory of linear order},
  author={Kamp, Johan Anthony Wilem},
  year={1968}
}

@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}
}

@article{Sistla1985,
	author    = {Sistla, A. P. and Clarke, E. M.},
	title     = {The Complexity of Propositional Linear Temporal Logics},
	journal   = {Journal of the ACM},
	volume    = 32,
	issue     = 3,
	year      = 1985,
	pages     = {733--749}
}

@article{Kupferman2001,
	author    = {Kupferman, Orna and Vardi, Moshe Y.},
	title     = {Model Checking of Safety Properties},
	journal   = {Formal Methods in System Design},
	volume    = 19,
	issue     = 3,
	year      = 2001,
	pages     = {291--314}
}

@inproceedings{Latvala2003,
	author    = {Latvala, Timo},
	title     = {Efficient Model Checking of Safety Properties},
	booktitle = {Model Checking Software. SPIN 2003},
	editor    = {Ball, Thomas and Rajamani, Sriram K.},
	year      = 2003,
	pages     = {74--88}
}

@inproceedings{Safra1988,
	author    = {Safra, S.},
	title     = {On The Complexity of $\omega$-Automata},
	booktitle = {29th Annual Symposium on Foundations of Computer Science},
	pages     = {319--327},
	year      = 1988
}