MARC 主機 00000nam 2200000 a 4500
001 AAI3121592
005 20051017073445.5
008 051017s2003 s eng d
020 0496689436
035 (UnM)AAI3121592
040 UnM|cUnM
100 1 Majumdar, Rupak
245 10 Symbolic algorithms for verification and control
|h[electronic resource]
300 201 p
500 Source: Dissertation Abstracts International, Volume: 65-
02, Section: B, page: 0843
500 Chair: Thomas A. Henzinger
502 Thesis (Ph.D.)--University of California, Berkeley, 2003
520 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 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 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 School code: 0028
650 4 Computer Science
690 0984
710 20 University of California, Berkeley
773 0 |tDissertation Abstracts International|g65-02B
856 40 |uhttps://pqdd.sinica.edu.tw/twdaoapp/servlet/
advanced?query=3121592
912 PQDT
