An algebraic theory for behavioral modeling and protocol synthesis in system design