Mitra, Johnson win 2012 best FORTE paper

CSL 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 (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 (right)

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

In the paper, 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 group at CSL and the Department of Electrical and Computer Engineering.