The Love and Romance of LTL

Very recently, I've seen an intense integration of my work life and my personal life. My boyfriend, who is another graduate student in my department, is presenting at meetings in my research group. The purpose of these presentations is to educate my group's professors and graduate students on the main ideas of another research area of Computer Science.

This week, his presentation was rather reminiscent of how we met. We met during the qualification exam. We had been assigned the same paper to present to our respective committees; 61 pages of satanic verses on the topic of the synthesis of fault-tolerant concurrent programs. Recently, I heard the original copy of the paper was actually printed on human skin.

If you know me personally, you'll know that my research area has very little to do directly with Kripke structures, AND/OR graphs, CTL, or soundness and completeness. One could argue that any field of Computer Science is related to these fundamental methods of formalization, but such an argument annoys me. Instead, put yourself in the shoes of a second-year CS grad with a background in Electrical Engineering. It took me a couple of days to realize that the "U" in that paper was "Until" and not "Union." It was dire. It was not good. I was going to fail.

And so, that first time we met, he stood at a whiteboard and described the main points of Linear Temporal Logic. He spoke deliberately and quietly, with a slight Southern accent. I was in love, but it took me two more years to tell him so. Weeks later, I was presenting the paper like a pro, thanks in part to that lovely man.

It is very likely that no other person in this week's research meeting found my boyfriend's presentation romantic, but it really was.