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

fYear

2008

fDate

7-9 April 2008

Firstpage

9

Lastpage

14

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Information Technology: New Generations, 2008. ITNG 2008. Fifth International Conference on

Conference_Location

Las Vegas, NV

Print_ISBN

0-7695-3099-0

Type

conf

DOI

10.1109/ITNG.2008.228

Filename

4492447