In conversation with a (highly passionate) temporal logician
Dr Kristin Y. Rozier is a temporal logician based within the Department of Aerospace Engineering at Iowa State University in the US. Her work encompasses many different fields, but all are aimed at making people’s lives better and safer.
If you have 100 socks in a drawer, 50 of which are red and 50 black, how many will you have to pull out to guarantee you have a pair? We will give you a second to think about it… Okay, time is up. Let us work through this logically. You pull out one sock and it is red. Now, the next sock could be red, making two socks to make a pair. However, you could pick out a black sock, meaning you do not have a pair. Regardless, the next sock you pick will be either a red or a black sock, which would guarantee you have a pair. The answer is three.
That gives us a simple logic puzzle we can all understand, but somebody who understands logic to a far greater degree is Dr Kristin Y. Rozier, associate professor within the Department of Aerospace Engineering at Iowa State University in the US. A recipient of the Initiative-Inspiration-Impact Award from Women in Aerospace, Kristin’s main passion (and foundation to her approach to life) is temporal logic; Kristin absolutely LOVES solving puzzles in order to make life better and safer for people.
WHY DOES KRISTIN DESCRIBE HERSELF AS A TEMPORAL LOGICIAN?
Kristin’s research spans a wide range of applications and theoretical domains, but the one thing they all have in common is temporal logic – that is, an unambiguous, mathematically precise way of describing and reasoning about systems that change over time. By adopting this approach, Kristin is able to solve meaningful problems in aerospace engineering, robotics, cybersecurity, theoretical computer science, mathematics, virtual reality, and more. “Think about solving an air traffic control problem, where you have to direct all of the planes to a configuration where they are safely separated from each other but still progressing toward their final destinations,” says Kristin. “You can come up with a solution (a configuration for all of the planes) but then they move! The planes keep flying! You have to come up with a series of solutions for the continuously changing airspace.”
Temporal logic provides a way of capturing critical details about puzzles so researchers can devise solutions and prove that they accomplish a project’s aim, such as keeping all the passengers safe in the air traffic control scenario.
FASCINATING FORMAL METHODS
Formal methods are mathematically rigorous techniques for the specification, design, validation, and verification of cyber-physical systems (systems that are made of hardware, software, or a combination of the two). They are vital to Kristin’s work as they enable her to prove both the presence of behaviours she wants a system to exhibit and the absence of behaviours she does not (such as something that would make a system unsafe). “Many people think you verify a system by testing; you give the system some input and observe that it does what you wanted in response. This works if you want to verify that – if there’s an obstacle on the left, the plane will turn right to avoid it. But what if the behaviour you want to verify is that the automated air traffic control system is incapable of telling two planes to get dangerously close to each other, under any circumstances?” explains Kristin. “Think about it: you cannot test for the absence of a behaviour you don’t want your system to have, but you can formally verify that, and you get to solve fun temporal logic puzzles in the process.”
Ultimately, Kristin’s research involves developing new algorithms to reason about safety-critical systems so that people can use and be around technology that makes their lives better and adheres to certain requirements at the same time.
WHERE WILL KRISTIN‘S RESEARCH LEAD TO IN THE FUTURE?
Or should that be, where does Kristin not see it heading in the future? One of the major challenges of Kristin’s work is that as technology becomes more advanced, it is necessary to advance formal methods to keep up. In that regard, her work is never-ending. “Wherever technology interacts with humans, or critically needs to work correctly, my research will be aimed at tackling that challenge. This includes future aircraft, robots, rovers, satellites, spacecraft, medical devices, automated cars, even Internet of Things (IoT) devices like the video doorbells and smart appliances in every-day houses,” says Kristin. “Systems that exhibit high levels of autonomy or learn and adapt to their environments present a new frontier for formal methods that I am very excited to explore.”
Kristin’s passion for problem solving is inspiring – will you be joining her to explore the logic puzzles of the future?
DR KRISTIN Y. ROZIER
Associate Professor, Department of Aerospace Engineering, Iowa State University, USA
FIELDS OF RESEARCH: Temporal Logic and Formal Methods
RESEARCH PROJECT: Designing algorithms to approach a range of research questions – including those in aerospace engineering, robotics, cybersecurity, theoretical computer science, mathematics, and virtual reality – from a logician’s standpoint
ABOUT TEMPORAL LOGIC
The key difference between logic and temporal logic is the quality of time (hence temporal). While logic is a precise and unambiguous means of describing a system, temporal logic describes systems that change over time. Many of the most challenging puzzles in life have this property – they are reactive systems that respond to their environments and therefore change over time.
Kristin firmly believes that puzzles have real-life analogues; when you complete a puzzle (like sudoku or matrix logic) or a level on a game, you will reach a screen that congratulates you for winning. Imagine, instead, that the clues you use to solve these puzzles were sensor data from a spacecraft and solving the puzzle means you can know that something is going wrong with the mission, even though you cannot directly see the fault. Instead of a ‘congratulations’ screen, your reward would be contributing to a scientific breakthrough that makes people’s lives better – you would enable the spacecraft to figure out by itself that something is wrong, and save the mission!
HOW DOES TEMPORAL LOGIC ENABLE KRISTIN’S RESEARCH?
Computer scientists have a way of classifying the hardness of problems, with the caveat that every problem in a particular hardness class has a proof that it is equivalent to other problem(s) in the same class. Puzzles and games that we find fun are most often in the class called ‘NP-Complete’ which is a meaningless acronym designating the class of problems that are challenging, but solvable, with the satisfying characteristic that if we are presented with a solution, it is easy to tell that that solution is correct. “The cool thing is that many of the world’s most impactful problems are also in the class NP-Complete or are at least helped by being able to solve problems in this class better,” explains Kristin. “If you develop strategies for efficiently solving these kinds of problems, you could apply those strategies to games and puzzles, or you could apply them to real-world problems – it’s really the same thing, except that it is so much more rewarding to use the same skills, have fun and have real-world impact!”
HOW TO BECOME A TEMPORAL LOGICIAN
• We highly recommend reading through the NASA website – it is a brilliant resource and provides a great way of learning more about specific projects that are currently underway.
• The Aerospace Industries Association is a great place to start if you are looking for opportunities in the future.
• According to Payscale, the average salary for an aerospace systems engineer is $81,000.
PATHWAY FROM SCHOOL TO TEMPORAL LOGIC
Kristin recommends studying logic and problem-solving (both inside and outside academia), which will help you to develop the ability to learn new things with deeper understanding and to practise using your brain in new ways. It is unlikely your school or college will offer specific ‘temporal logic’ classes, but Kristin says studying computer science, mathematics (especially mathematical logic), algorithms, and philosophy will help nurture the thinking involved in her work. Analysing the connections between events in history is also related.
“Shying away from mathematics and science classes will cut off your future opportunities, so study hard and do well in those classes to ensure you can choose what you want to do in the future,” says Kristin. “I suffered terribly during my 12th grade mathematics class (due to the teaching style and others telling me I couldn’t do math), but I am glad I persevered, as I earned an A and got accepted to the College of William and Mary, where I was able to study calculus again in a better environment. Ultimately, that set me on the path to the computer science programme that changed my life and set me on my current trajectory.”
HOW DID KRISTIN BECOME A TEMPORAL LOGICIAN?
WHAT WERE YOUR INTERESTS AS A CHILD?
I loved logic puzzles! I never thought that would amount to anything – I am so glad I was wrong. When I design an algorithm now, I am solving a huge, complex matrix logic puzzle for every point in time!
Reference
https://doi.org/10.33424/FUTURUM316
 temporal logician - https://futurumcareers.com/in-conversation-with-a-highly-passionate-temporal-logician){kind=link}
I always wanted to travel and meet people, and I wanted to shape policies to make their lives better. I thought I might work for the United Nations, but STEM attracts the brightest minds from all over the planet. I get to collaborate with awesome people from many different countries and learn from their diverse perspectives. I get to present my research findings at international meetings and work with research labs in many different locations, learning about global challenges and publishing work that influences technology worldwide – it’s more fun than I ever dreamed as a kid. I wanted to be a professional ballerina (and I succeeded too – I taught ballet at a dance studio down the street from NASA Langley Research Center while I was a research scientist there). I also taught tap dance!
WHO OR WHAT INSPIRED YOU TO BECOME A SCIENTIST?
My parents gave me a book on Marie Curie that sparked my imagination. I ended up doing a James Monroe Scholarship project on her as an undergraduate at college, where I traced her life through Poland and France. My parents were both interested in STEM (my father was a technologist and my mother was a nurse), and I have crayon drawings that I made in elementary school of Bell Laboratories because my dad would tell me stories of the fascinating people who got to work there. Initially, I thought I could never have the impact I wanted as a scientist and thought I would have to become a lawyer at the UN or something like that, until I had the epiphany that I could do more as a scientist.
WHAT ATTRIBUTES HAVE MADE YOU SUCCESSFUL AS A SCIENTIST?
Seeing the world as a collection of giant puzzles, waiting to be solved! Once I had an education that allowed me to see the parts of the puzzles, the world started to look like a collection of challenges, some of which I might be able to solve. There are so many challenges out there, and the key is to take each one and ask, “Can I advance this one closer to a solution?” Most of the time, the answer is no, but sometimes I have a great idea that works. Even ideas that fail are great learning experiences that make you better at devising future solutions.
WHAT MOTIVATES YOU TO DO THE WORK YOU DO?
I get to push the bounds of human knowledge; I get to advance the state of the art and do things that have never been done before; I get to create new technology that makes life better, safer and more secure; and I get to collaborate with fascinating people who challenge me, from all different backgrounds, from all over the world. When we accomplish a mission together, we get to see something amazing, like a flight of a new aircraft or a spacecraft going where no one has gone before.
HOW DO YOU OVERCOME OBSTACLES IN YOUR WORK?
Failure is a wonderful thing – it teaches you more than success. I tell the students in my lab that failure is an opportunity to learn how to do it right next time and abject failure comes with the bonus of a great story to tell at the next party! I try to get things right, of course, but when I don’t, I try to learn as much from that experience as I can. As a woman, I’ve had a lot of people tell me I can’t do this job, which has presented a significant obstacle in my life. I have learned not to listen to them, and I’m still working on finding ways to keep those people from limiting the opportunities available to future scientists.
HOW DO YOU ‘SWITCH OFF’ FROM THE COMPLEXITIES OF YOUR WORK?
My brain never switches off! Sometimes it works better when I’m spotting a pirouette in ballet class, or climbing a mountain on my bicycle, or staring at a painting in one of my favourite museums.
WHAT AMBITIONS DO YOU STILL WANT TO ACHIEVE?
There are so many places I want to see, experiences I want to have, and people I want to meet. My ambition is to do the best that I can do and explore the opportunities that open up from there.
KRISTIN’S TOP TIPS
01 Mastering logic (mathematical logic, logical deduction, the skills you need to reliably solve matrix logic puzzles or Raymond Smullyan books, or even to have a good guess at the culprit in Agatha Christie novels) will serve you well in all areas of life.
02 Logic underlies all the challenges I tackle and allows me to break down the problems into sub-problems that I can solve. It even prevents me from arguing with other people; if you can logically deduce your point of view, and that of the other person, then there is nothing to argue about!
03 Logic and logical thinking can prevent you from becoming confused or taken advantage of; logic can instil an idea of making decisions based on reality and thought, as opposed to emotions, which will help you reach your goals.
Do you have a question for Kristin?
Write it in the comments box below and Kristin will get back to you. (Remember, researchers are very busy people, so you may have to wait a few days.)