Actlab: verifying reactive systems by talking to them

In this paper the verification environment ACTLab is presented. ACTLab is centered around the ACTL Model Checker for the branching time action-based temporal logic ACTL. Tha AMC checks, in linear time, whether a given LTS satisfies a property expressed by an ACTL formula. The helpful explanation facllity is available in AMC; also, an interface with the behavioural verification tool AUTO is provided. ACTLab has been designed having a precise purpose in mind: make the specification and the verification of temporal logic formulae easy for the user. Propertlas of raactiva systems are oftan expressed by naturallanguage sentences, thus many impreclslons oceur in the passage tram informai expresslons of system propertles to temporal logie formulae. We thus developed a proto, type translator, NL2ACTL, from Naturallanguage expressions to Temporal Loglc formulae, that would help to generate ! logic formulae, by working aut ambiguitles by maans of interactions with the usar. NL2ACTL has bean intagratad Into ACTlab, providing a way to make tha axprasslon of properties In the logie easier far the user.