Mitra and Johnson win award for research on machine models

 Subscribe to ECE ILLINOIS News

By Elise King, Coordinated Science Lab
October 10, 2012

  • ECE Assistant Professor Sayan Mitra and his graduate student Taylor Johnson recently won the best paper award at the IFIP International Conference on Formal Techniques for Distributed Systems.
  • Their paper examined the problem of verifying invariant properties of infinite collections of interacting state machine models called rectangular hybrid automata (RHA).
  • Their software, Passel, automatically checks invariants of RHA networks modeling an air traffic control landing protocol.

Sayan  Mitra
Sayan Mitra

ECE Assistant Professor Sayan Mitra and ECE graduate student Taylor Johnson recently won the best paper award at the IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE ’12). The paper was chosen out of three collocated conferences in Stockholm under the umbrella of the International Federated Conference on Distributed Computing Techniques.

Taylor Johnson
Taylor Johnson

In the winning paper, titled, “A Small Model Theorem for Rectangular Hybrid Automata Networks,” Mitra, a researcher in the Coordinated Science Lab (CSL), and Johnson looked at the problem of verifying invariant properties of infinite collections of interacting state machine models called rectangular hybrid automata (RHA). RHA networks can model, for example, timing-based network protocols, traffic control protocols and robotic swarms.

Mitra and Johnson show that the problem of verifying an invariant for an arbitrarily large collection of automata can be reduced to checking a finite collection, for some restricted classes of RHAs. The size of the finite collection that has to be checked depends on the syntactic structure of the automaton and the invariant. This "small model" result relies on demonstrating that any violation of the invariant by a larger system can be mimicked by a violation in a smaller system.

The paper also discusses the implementation of a software prototype, called Passel, which Mitra and Johnson created for automatically checking invariants of RHA networks modeling an air traffic control landing protocol, as well as several distributed mutual exclusion algorithms. Moving forward, Mitra and Johnson plan to continue to develop Passel and investigate methods for finding invariant properties for RHA networks.

Mitra and Johnson are in the Reliable and High Performance Computing group at CSL.

Editor's note: media inquiries should be directed to Brad Petersen, Director of Communications, at bradp@illinois.edu or (217) 244-6376.

 Subscribe to ECE ILLINOIS News