Journal
Scientific and technical journal of information technologies, mechanics and optics
UDK004.4’242
Issue:6 (64)
MODEL CHECKING AUTOMATA-BASED PROGRAMS USING REDUCED TRANSITION GRAPH CONSTRUCTION
Annotation
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
Постоянный URL
Articles in current issue
- GENERALIZED COMPUTER MODEL STRUCTURE OF OPTICAL ELECTRONIC SYSTEMS
- INACCURACY STUDY OF MARKS CONGRUENCE UNDER LATERAL PICKUPS
- UNIT FOR EXPERIMENTAL OBSERVATION OF CHEMILUMINESCENT SPECTRUMS
- FLUORESCENCE LIFETIME OF CdSe/ZnS QUANTUM DOTS AND THEIR COMPLEXES WITH ORGANIC MOLECULES IN THIN POLYMER FILMS
- METHOD OF THE CRACK LOCATION DEFINITION AND THERMAL CONNECTION QUALITY CONTROL ON THE BASIS OF MAGNETIC MEASUREMENTS
- MODELING AND IMPROVING THE DYNAMIC CHARACTERISTICS OF SPINDLE UNITS BASED ON HYDROSTATIC BEARINGS
- DECISION-MAKING INFORMATION SUPPORT SOFTWARE FOR TYPICAL FLIGHT PATH ASSESSMENT
- THE INFLUENCE OF YLP - LASER RADIATION ON THE CURRENT-VOLTAGE CHARACTERISTICS OF THE SILICON-SILICON DIOXIDE SYSTEM
- MULTIUNIT DETECTORS ON THE BASIS OF LEAD SELENIDE FOR THE SPECTRUM AREA OF 2 - 5 MICRONS
- THE STUDY OF THE COVERS OPTICAL PROPERTIES BASED ON GIDROGENIOS CARBONEUM MODIFIED BY METAL NANOPARTICLES
- DISPERSIVE ALUMINIUM FILLING MATERIAL INFLUENCE ON THE POLYPROPYLENE STRUCTURE AND PROPERTIES
- THE SEMANTIC WEB AND ARTIFICIAL INTELLIGENCE
- A MULTI-AGENT TECHNOLOGY FOR VIRTUAL BUSINESS PLATFORMS FORMATION IN THE SHARED INFO-COMMUNICATION ENVIRONMENT OF INNOVATIONS DEVELOPMENT
- BUSINESS ORGANIZATION SUSTAINABLE DEVELOPMENT IMPLEMENTATION ON THE BASIS OF CONTROLLING AND SELF-ORGANIZATION MECHANISMS INTERRELATION
- 4 "RE-'S " OF CHANGING BUSINESS: REFORMING, REORGANIZATION, RESTRUCTURING, REENGINEERING
- MODERN STATE OF THE ENTERPRISE COMPETITIVENESS CONTROL PROBLEMS
- MACROECONOMIC EFFECTS OF LARGE-SCALE PROJECTS REALIZATION
- TYPICAL WEB-PORTAL CREATION OF THE UNIVERSITY INNOVATIVE EDUCATIONAL PROGRAM AND ITS INSTALLATION IN THE UNIVERSITY NETWORK INFRASTRUCTURE