DocumentCode
648613
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
fYear
2013
fDate
27-30 Sept. 2013
Firstpage
1
Lastpage
4
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Design & Test Symposium, 2013 East-West
Conference_Location
Rostov-on-Don
Print_ISBN
978-1-4799-2095-2
Type
conf
DOI
10.1109/EWDTS.2013.6673198
Filename
6673198
Link To Document