MODEL CHECKING AUTOMATA-BASED PROGRAMS USING REDUCED TRANSITION GRAPH CONSTRUCTION
Read the full article
This article is concentrated on techniques of converting automata-based program models to Kripke models designed for checking properties related to system behavior. The definition of these properties is considered by means of temporal logic formulas. We propose an efficient technique of such converting and property stating that allows construction of small Kripke models and sufficiently fast checking of such models.
Keywords: model checking, temporal logic, automata-based programming