Mark Bouwman: Verifying the EULYNX level crossing

Event Details

Even though the behaviour of the EULYNX specification of the level crossing is conceptually quite simple, the state space associated to the mCRL2 model is enormous. This Thursday I will present the reasons for the state space explosion and the measures we took to drastically reduce it. Moreover, I will present the verification efforts, which includes some interesting results.