Title :
Verification of specifications in the language L with respect to temporal properties expressible by GR(1) formulas
Author :
Chebotarev, Alexander
Author_Institution :
Glushkov Inst. of Cybern., Kiev, Ukraine
Abstract :
The verification methods for reactive algorithms specifications in the logical language L are considered. The verification is performed with respect to properties expressed in the GR(1) class of temporal logic LTL, and is reduced to satisfiability checking L formulas.
Keywords :
computability; formal verification; specification languages; temporal logic; GR(1) formulas; LTL; language specification verification method; linear temporal logic; logical language; reactive algorithms specifications; satisfiability checking L formulas; temporal properties;
Conference_Titel :
Design & Test Symposium, 2013 East-West
Conference_Location :
Rostov-on-Don
Print_ISBN :
978-1-4799-2095-2
DOI :
10.1109/EWDTS.2013.6673198
