Model-Checking TRIO specifications in SPIN

We present a novel application on model checking through SPIN as a means for verifying purely descriptive specifications written in TRIO, a first order, linear-time temporal logic with both future and past operators and a quantitative metric on time. The approach is based on the translation of TRIO formulae into Promela programs guided by an equivalence between TRIO and 2-way alternating Büchi automata. An optimization technique based on the modularized TRIO specifications is also shown. The results of our experimentation are quite encouraging, as we are able to verify properties of the Railway Crossing Problem, a well-known benchmark used in the Formal Methods community, for values of the temporal constants that make the verification totally infeasible with traditional tools and approaches.