Title :
Improving Pattern-Based LTL Formulas for Automata Model Checking
Author :
Salamah, Salamah ; Gates, Ann Q. ; Roach, Steve
Author_Institution :
Embry-Riddle Aeronaut. Univ., Daytona Beach
Abstract :
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 Buchi automaton generated for the formula. Minimizing the size of the Buchi automata for an LTL specification provides a significant support to the area of model checking.
Keywords :
formal specification; software tools; temporal logic; Buchi automata; Buchi automaton; Property Specification tool; Prospec tool; automata model checking; formal specifications; linear temporal logic; pattern-based LTL formulas; Automata; Computer science; Counting circuits; Formal specifications; Information technology; Logic; Software engineering; Software systems; Specification languages; Writing; B¨uchi Automaton; Composite Propositions; LTL; Pattern; Prospec; Scope;
Conference_Titel :
Information Technology: New Generations, 2008. ITNG 2008. Fifth International Conference on
Conference_Location :
Las Vegas, NV
Print_ISBN :
0-7695-3099-0
DOI :
10.1109/ITNG.2008.228
