Improving Pattern-Based LTL Formulas for Automata Model Checking
2008Vol. 89, pp. 9–14
Citations Over TimeTop 23% of 2008 papers
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.
Related Papers
- → Model checking for extended timed temporal logics(1996)19 cited
- Verifying Temporal Properties without using Temporal Logic(2001)
- Logics for Mazurkiewicz Traces(2002)
- A Model Checking of Real-Time Systems in Linear Temporal Logic with Clocks(2002)
- Linear Temporal Logic and Buchi Automata(2009)