MODEL CHECKING AUTOMATA-BASED PROGRAMS USING REDUCED TRANSITION GRAPH CONSTRUCTION

Sergey Velder, Shalyto Anatoly A.

2009 , VOLUME 09, NUMBER 6 ( NOVEMBER-DECEMBER )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Publications

Editor-in-Chief

Nikiforov
Vladimir O.
D.Sc., Prof.

Partners

MODEL CHECKING AUTOMATA-BASED PROGRAMS USING REDUCED TRANSITION GRAPH CONSTRUCTION

S. Velder, A. A. Shalyto

Read the full article

Abstract

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

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License