This paper describes an attempt to compare two toolsets allowing generation of finite labeled transition systems from underlying concurrent specification languages. The comparison is done on a specification of the leader election protocol from Home Audio/Video interoperability (HAVi) architecture. Some important semantical differences of PROMELA and $mu$CRL are identified, that lead to big differences in size of the state spaces generated for equivalent specifications.

Theory of computing (msc 68Qxx), Formal languages and automata (msc 68Q45), Specification and verification (program logics, model checking, etc.) (msc 68Q60)
CWI
Software Engineering [SEN]
Specification and Analysis of Embedded Systems

Usenko, Y.S. (1999). A comparison of Spin and the $ mu $ CRL toolset on HAVi leader election protocol. Software Engineering [SEN]. CWI.