國立高雄大學圖資館 |

Language: English

Back

Symbolic algorithms for verification and control

Record Type:	Electronic resources : Monograph/item
Title/Author:	Symbolic algorithms for verification and control
Author:	Majumdar, Rupak.
Description:	201 p.
Notes:	Chair: Thomas A. Henzinger.
Notes:	Source: Dissertation Abstracts International, Volume: 65-02, Section: B, page: 0843.
Contained By:	Dissertation Abstracts International65-02B.
Subject:	Computer Science.
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3121592
ISBN:	0496689436

Symbolic algorithms for verification and control
Majumdar, Rupak.

Symbolic algorithms for verification and control [electronic resource] - 201 p.

Chair: Thomas A. Henzinger.

Thesis (Ph.D.)--University of California, Berkeley, 2003.

Methods for the formal specification and verification of systems are indispensible for the development of complex yet correct systems. In formal verification, the designer describes the system in a modeling language with a well-defined semantics, and this system description is analyzed against a set of correctness requirements. Model checking is an algorithmic technique to check that a system description indeed satisfies correctness requirements given as logical specifications. While successful in hardware verification, the potential for model checking for software and embedded systems has not yet been realized. This is because traditional model checking focuses on systems modeled as finite state-transition graphs. While a natural model for hardware (especially synchronous hardware), state-transition graphs often do not capture software and embedded systems at an appropriate level of granularity. This dissertation considers two orthogonal extensions to finite state-transition graphs making model checking techniques applicable to both a wider class of systems and a wider class of properties.

ISBN: 0496689436Subjects--Topical Terms:

212513
Computer Science.

Symbolic algorithms for verification and control
LDR:03251nmm _2200289 _450 001 162424
005 20051017073445.5
008 230606s2003 eng d
020 $a 0496689436
035 $a 00148925
035 $a 162424
040 $a UnM $c UnM
100 0 $a Majumdar, Rupak. $3 227560
245 1 0 $a Symbolic algorithms for verification and control $h [electronic resource]
300 $a 201 p.
500 $a Chair: Thomas A. Henzinger.
500 $a Source: Dissertation Abstracts International, Volume: 65-02, Section: B, page: 0843.
502 $a Thesis (Ph.D.)--University of California, Berkeley, 2003.
520 # $a Methods for the formal specification and verification of systems are indispensible for the development of complex yet correct systems. In formal verification, the designer describes the system in a modeling language with a well-defined semantics, and this system description is analyzed against a set of correctness requirements. Model checking is an algorithmic technique to check that a system description indeed satisfies correctness requirements given as logical specifications. While successful in hardware verification, the potential for model checking for software and embedded systems has not yet been realized. This is because traditional model checking focuses on systems modeled as finite state-transition graphs. While a natural model for hardware (especially synchronous hardware), state-transition graphs often do not capture software and embedded systems at an appropriate level of granularity. This dissertation considers two orthogonal extensions to finite state-transition graphs making model checking techniques applicable to both a wider class of systems and a wider class of properties.
520 # $a The first direction is an extension to infinite-state structures finitely represented using constraints and operations on constraints. Infinite state arises when we wish to model variables with unbounded range (e.g., integers), or data structures, or real time. We provide a uniform framework of symbolic region algebras to study model checking of infinite-state systems. We also provide sufficient language-independent termination conditions for symbolic model checking algorithms on infinite state systems.
520 # $a The second direction supplements verification with game theoretic reasoning. Games are natural models for interactions between components. We study game theoretic behavior with winning conditions given by temporal logic objectives both in the deterministic and in the probabilistic context. For deterministic games, we provide an extremal model characterization of fixpoint algorithms that link solutions of verification problems to solutions for games. For probabilistic games we study fixpoint characterization of winning probabilities for games with o-regular winning objectives, and construct (epsilon-)optimal winning strategies.
590 $a School code: 0028.
650 # 0 $a Computer Science. $3 212513
690 $a 0984
710 0 # $a University of California, Berkeley. $3 212474
773 0 # $g 65-02B. $t Dissertation Abstracts International
790 $a 0028
790 1 0 $a Henzinger, Thomas A., $e advisor
791 $a Ph.D.
792 $a 2003
856 4 0 $u http://libsw.nuk.edu.tw/login?url=http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3121592 $z http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3121592