loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fifth International Conference on Information Technology: New Generations (itng 2008)
Improving Pattern-Based LTL Formulas for Automata Model Checking
April 07-April 09
ISBN: 978-0-7695-3099-4
ASCII Text
x 
 
Salamah Salamah, Ann Q. Gates, Steve Roach, "Improving Pattern-Based LTL Formulas for Automata Model Checking," Information Technology: New Generations, Third International Conference on, pp. 9-14, Fifth International Conference on Information Technology: New Generations (itng 2008), 2008.
 
 
BibTex
x
 
@article{ 10.1109/ITNG.2008.228,
author = {Salamah Salamah and Ann Q. Gates and Steve Roach},
title = {Improving Pattern-Based LTL Formulas for Automata Model Checking},
journal ={Information Technology: New Generations, Third International Conference on},
volume = {0},
year = {2008},
isbn = {978-0-7695-3099-4},
pages = {9-14},
doi = {http://doi.ieeecomputersociety.org/10.1109/ITNG.2008.228},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Information Technology: New Generations, Third International Conference on
TI - Improving Pattern-Based LTL Formulas for Automata Model Checking
SN - 978-0-7695-3099-4
SP9
EP14
A1 - Salamah Salamah,
A1 - Ann Q. Gates,
A1 - Steve Roach,
PY - 2008
KW - LTL
KW - B?uchi Automaton
KW - Pattern
KW - Scope
KW - Prospec
KW - Composite Propositions
VL - 0
JA - Information Technology: New Generations, Third International Conference on
ER -
 
The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et. al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the B?uchi automaton generated for the formula. Minimizing the size of the B?uchi automata for an LTL specification provides a significant support to the area of model checking.
Index Terms:
LTL, B?uchi Automaton, Pattern, Scope, Prospec, Composite Propositions
Citation:
Salamah Salamah, Ann Q. Gates, Steve Roach, "Improving Pattern-Based LTL Formulas for Automata Model Checking," itng, pp.9-14, Fifth International Conference on Information Technology: New Generations (itng 2008), 2008
Usage of this product signifies your acceptance of the Terms of Use.