NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
A Game-Theoretic Approach to Branching Time Abstract-Check-Refine ProcessSince the complexity of software systems continues to grow, most engineers face two serious problems: the state space explosion problem and the problem of how to debug systems. In this paper, we propose a game-theoretic approach to full branching time model checking on three-valued semantics. The three-valued models and logics provide successful abstraction that overcomes the state space explosion problem. The game style model checking that generates counter-examples can guide refinement or identify validated formulas, which solves the system debugging problem. Furthermore, output of our game style method will give significant information to engineers in detecting where errors have occurred and what the causes of the errors are.
Document ID
20100024468
Acquisition Source
Ames Research Center
Document Type
Conference Paper
Authors
Wang, Yi (Tokyo Univ. Japan)
Tamai, Tetsuo (Tokyo Univ. Japan)
Date Acquired
August 24, 2013
Publication Date
April 1, 2009
Publication Information
Publication: Proceedings of the First NASA Formal Methods Symposium
Subject Category
Mathematical And Computer Sciences (General)
Distribution Limits
Public
Copyright
Public Use Permitted.

Related Records

IDRelationTitle20100024454Collected WorksProceedings of the First NASA Formal Methods Symposium
No Preview Available