The Internet of Things, or IoT, refers to the network of physical devices, from smartphones and personal fitness trackers to home alarm systems and smart refrigerators, even vehicles. Collectively, these devices can make our environment smarter.
“The promise of IoT is that it will make our lives easier,” says Sheila McIlraith (pictured top right), a professor of computer science at the University of Toronto. “But these devices need to be programmed, instructed and customized, and most people don’t know how to program – nor should they have to.”
To solve this problem, McIlraith says Alberto Camacho (pictured top left), a PhD student in U of T's department of computer science who she supervises, is looking for synergies between fast, effective algorithms in artificial intelligence (AI) for automated planning – developed by their research group for tasking robots – and program synthesis, the task of generating a computer program automatically from a specification of user intent.
Camacho presented their work at two international conferences this summer. Their paper, Finite LTL Synthesis as Planning – with contributions from U of T computer science alumni Jorge A. Baier, now an assistant professor at the Pontificia Universidad Católica de Chile, and Christian Muise, now a researcher with IBM Research AI – was presented and demonstrated at the International Conference on Automated Planning and Scheduling in Delft, the Netherlands. Camacho’s system, SynKit, was awarded the conference’s prize for best demonstration.
A second paper, LTL Realizability via Safety and Reachability Games, that explores fundamental principles, was presented at the International Joint Conference on Artificial Intelligence.
Synthesis, explains Camacho, is a classical problem in computer science. It was first introduced by Princeton University Professor Alonzo Church in the 1950s in the context of synthesizing digital circuits from logical specifications. Software synthesis, which Camacho and his colleagues study, has the end goal of automatically constructing software that satisfies user intent.
“Synthesis has been very well studied and understood theoretically, but no practical solutions existed,” says Camacho. “New algorithmic approaches were introduced in 2006, and practical tools started to appear.”
To develop their practical tool for synthesis, Camacho uses linear temporal logic, or LTL, a form of logic that expresses what the user wants the program to do, such as “send me an alert if someone enters the house when I’m away this weekend,” or “switch off the lights when there’s no one in the room."
Instructions in LTL sound a lot like English-language instructions, explains McIlraith, but LTL is a formal language with well-defined semantics so there is no ambiguity in the LTL statements.
“I can say something to you, and if you misunderstand, we can have a conversation back and forth [to clarify],” says McIlraith. “But when we care about synthesizing safety-critical systems like a controller for a nuclear power plant, or for an autonomous car, it really matters that the system understands what we’re asking it to do.”
Camacho says they’re applying their state-of-the-art automated planning algorithms to LTL synthesis. The program which is generated is correct by construction, and every run of that program satisfies the LTL statements provided to it.
"We think the new techniques we are introducing will have some impact," says Camacho.
This research was funded in part by the Natural Sciences and Engineering Research Council of Canada (NSERC).