---
_id: '4414'
abstract:
- lang: eng
text: "This dissertation investigates game-theoretic approaches to the algorithmic
analysis of concurrent, reactive systems. A concurrent system comprises a number
of components working concurrently; a reactive system maintains an ongoing interaction
with its environment. Traditional approaches to the formal analysis of concurrent
reactive systems usually view the system as an unstructured state-transition graphs;
instead, we view them as collections of interacting components, where each one
is an open system which accepts inputs from the other components. The interactions
among the components are naturally modeled as games.\r\n\r\nAdopting this game-theoretic
view, we study three related problems pertaining to the verification and synthesis
of systems. Firstly, we propose two novel game-theoretic techniques for the model-checking
of concurrent reactive systems, and improve the performance of model-checking.
The first technique discovers an error as soon as it cannot be prevented, which
can be long before it actually occurs. This technique is based on the key observation
that "unpreventability" is a local property to a module: an error is
unpreventable in a module state if no environment can prevent it. The second technique
attempts to decompose a model-checking proof into smaller proof obligations by
constructing abstract modules automatically, using reachability and "unpreventability"
information about the concrete modules. Three increasingly powerful proof decomposition
rules are proposed and we show that in practice, the resulting abstract modules
are often significantly smaller than the concrete modules and can drastically
reduce the space and time requirements for verification. Both techniques fall
into the category of compositional reasoning.\r\n\r\nSecondly, we investigate
the composition and control of synchronous systems. An essential property of synchronous
systems for compositional reasoning is non-blocking. In the composition of synchronous
systems, however, due to circular causal dependency of input and output signals,
non-blocking is not always guaranteed. Blocking compositions of systems can be
ruled out semantically, by insisting on the existence of certain fixed points,
or syntactically, by equipping systems with types, which make the dependencies
between input and output signals transparent. We characterize various typing mechanisms
in game-theoretic terms, and study their effects on the controller synthesis problem.
We show that our typing systems are general enough to capture interesting real-life
synchronous systems such as all delay-insensitive digital circuits. We then study
their corresponding single-step control problems --a restricted form of controller
synthesis problem whose solutions can be iterated in appropriate manners to solve
all LTL controller synthesis problems. We also consider versions of the controller
synthesis problem in which the type of the controller is given. We show that the
solution of these fixed-type control problems requires the evaluation of partially
ordered (Henkin) quantifiers on boolean formulas, and is therefore harder (nondeterministic
exponential time) than more traditional control questions.\r\n\r\nThirdly, we
study the synthesis of a class of open systems, namely, uninitialized state machines.
The sequential synthesis problem, which is closely related to Church's solvability
problem, asks, given a specification in the form of a binary relation between
input and output streams, for the construction of a finite-state stream transducer
that converts inputs to appropriate outputs. For efficiency reasons, practical
sequential hardware is often designed to operate without prior initialization.
Such hardware designs can be modeled by uninitialized state machines, which are
required to satisfy their specification if started from any state. We solve the
sequential synthesis problem for uninitialized systems, that is, we construct
uninitialized finite-state stream transducers. We consider specifications given
by LTL formulas, deterministic, nondeterministic, universal, and alternating Buechi
automata. We solve this uninitialized synthesis problem by reducing it to the
well-understood initialized synthesis problem. While our solution is straightforward,
it leads, for some specification formalisms, to upper bounds that are exponentially
worse than the complexity of the corresponding initialized problems. However,
we prove lower bounds to show that our simple solutions are optimal for all considered
specification formalisms. The lower bound proofs require nontrivial generic reductions."
article_processing_charge: No
author:
- first_name: Freddy
full_name: Mang, Freddy
last_name: Mang
citation:
ama: Mang F. Games in open systems verification and synthesis. 2002:1-116.
apa: Mang, F. (2002). *Games in open systems verification and synthesis*. University
of California, Berkeley.
chicago: Mang, Freddy. “Games in Open Systems Verification and Synthesis.” University
of California, Berkeley, 2002.
ieee: F. Mang, “Games in open systems verification and synthesis,” University of
California, Berkeley, 2002.
ista: Mang F. 2002. Games in open systems verification and synthesis. University
of California, Berkeley.
mla: Mang, Freddy. *Games in Open Systems Verification and Synthesis*. University
of California, Berkeley, 2002, pp. 1–116.
short: F. Mang, Games in Open Systems Verification and Synthesis, University of
California, Berkeley, 2002.
date_created: 2018-12-11T12:08:44Z
date_published: 2002-05-01T00:00:00Z
date_updated: 2021-01-12T07:56:48Z
day: '01'
extern: '1'
language:
- iso: eng
month: '05'
oa_version: None
page: 1 - 116
publication_status: published
publisher: University of California, Berkeley
publist_id: '315'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Games in open systems verification and synthesis
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2002'
...
---
_id: '4411'
abstract:
- lang: eng
text: "Model checking algorithms for the verification of reactive systems proceed
by a systematic and exhaustive exploration of the system state space. They do
not scale to large designs because of the state explosion problem --the number
of states grows exponentially with the number of components in the design. Consequently,
the model checking problem is PSPACE-hard in the size of the design description.
This dissertation proposes three novel techniques to combat the state explosion
problem.\r\n\r\nOne of the most important advances in model checking in recent
years has been the discovery of symbolic methods, which use a calculus of expressions,
such as binary decision diagrams, to represent the state sets encountered during
state space exploration. Symbolic model checking has proved to be effective for
verifying hardware designs. Traditionally, symbolic checking of temporal logic
specifications is performed by backward fixpoint reasoning with the operator Pre.
Backward reasoning can be wasteful since unreachable states are explored. We suggest
the use of forward fixpoint reasoning based on the operator Post. We show how
all linear temporal logic specifications can be model checked symbolically by
forward reasoning. In contrast to backward reasoning, forward reasoning performs
computations only on the reachable states.\r\n\r\nHeuristics that improve algorithms
for application domains, such as symbolic methods for hardware designs, are useful
but not enough to make model checking feasible on industrial designs. Currently,
exhaustive state exploration is possible only on designs with about 50-100 boolean
state variables. Assume-guarantee verification attempts to combat the state explosion
problem by using the principle of "divide and conquer," where the components
of the implementation are analyzed one at a time. Typically, an implementation
component refines its specification only when its inputs are suitably constrained
by other components in the implementation. The assume-guarantee principle states
that instead of constraining the inputs by implementation components, it is sound
to constrain them by the corresponding specification components, which can be
significantly smaller. We extend the assume-guarantee proof rule to deal with
the case where the specification operates at a coarser time scale than the implementation.
Using our model checker Mocha, which implements this methodology, we verify VGI,
a parallel DSP processor chip with 64 compute processors each containing approximately
800 state variables and 30K gates.\r\n\r\nOur third contribution is a systematic
model checking methodology for verifying the abstract shared-memory interface
of sequential consistency on multiprocessor systems with three parameters --number
of processors, number of memory locations, and number of data values. Sequential
consistency requires that some interleaving of the local temporal orders of read/write
events at different processors be a trace of serial memory. Therefore, it suffices
to construct a non-interfering serializer that watches and reorders read/write
events so that a trace of serial memory is obtained. While in general such a serializer
must be unbounded even for fixed values of the parameters --checking sequential
consistency is undecidable!-- we show that the paradigmatic class of snoopy cache
coherence protocols has finite-state serializers. In order to reduce the arbitrary-parameter
problem to the fixed-parameter problem, we develop a novel framework for induction
over the number of processors and use the notion of a serializer to reduce the
problem of verifying sequential consistency to that of checking language inclusion
between finite state machines."
article_processing_charge: No
author:
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: Qadeer S. Algorithms and Methodology for Scalable Model Checking. 1999:1-150.
apa: Qadeer, S. (1999). *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley.
chicago: Qadeer, Shaz. “Algorithms and Methodology for Scalable Model Checking.”
University of California, Berkeley, 1999.
ieee: S. Qadeer, “Algorithms and Methodology for Scalable Model Checking,” University
of California, Berkeley, 1999.
ista: Qadeer S. 1999. Algorithms and Methodology for Scalable Model Checking. University
of California, Berkeley.
mla: Qadeer, Shaz. *Algorithms and Methodology for Scalable Model Checking*.
University of California, Berkeley, 1999, pp. 1–150.
short: S. Qadeer, Algorithms and Methodology for Scalable Model Checking, University
of California, Berkeley, 1999.
date_created: 2018-12-11T12:08:43Z
date_published: 1999-10-01T00:00:00Z
date_updated: 2021-01-12T07:56:47Z
day: '01'
extern: '1'
language:
- iso: eng
main_file_link:
- url: http://mtc.epfl.ch/~tah/Students/qadeer.pdf
month: '10'
oa_version: None
page: 1 - 150
publication_status: published
publisher: University of California, Berkeley
publist_id: '321'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
- first_name: Robert
full_name: Bryton, Robert
last_name: Bryton
- first_name: John
full_name: Steel, John
last_name: Steel
title: Algorithms and Methodology for Scalable Model Checking
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1999'
...
---
_id: '4419'
article_processing_charge: No
author:
- first_name: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: Kopke P. The Theory of Rectangular Hybrid Automata. 1996.
apa: Kopke, P. (1996). *The Theory of Rectangular Hybrid Automata*. Cornell
University.
chicago: Kopke, Peter. “The Theory of Rectangular Hybrid Automata.” Cornell University,
1996.
ieee: P. Kopke, “The Theory of Rectangular Hybrid Automata,” Cornell University,
1996.
ista: Kopke P. 1996. The Theory of Rectangular Hybrid Automata. Cornell University.
mla: Kopke, Peter. *The Theory of Rectangular Hybrid Automata*. Cornell University,
1996.
short: P. Kopke, The Theory of Rectangular Hybrid Automata, Cornell University,
1996.
date_created: 2018-12-11T12:08:45Z
date_published: 1996-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:50Z
day: '01'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
publication_status: published
publisher: Cornell University
publist_id: '312'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: The Theory of Rectangular Hybrid Automata
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1996'
...
---
_id: '4428'
abstract:
- lang: eng
text: "Hybrid systems are real-time systems that react to both discrete and continuous
activities (such as analog signals, time, temperature, and speed). Typical examples
of hybrid systems are embedded systems, timing-based communication protocols,
and digital circuits at the transistor level. Due to the rapid development of
microprocessor technology, hybrid systems directly control much of what we depend
on in our daily lives. Consequently, the formal specification and verification
of hybrid systems has become an active area of research. This dissertation presents
the first general framework for the formal specification and verification of hybrid
systems, as well as the first hybrid-system analysis tool--HyTech. The framework
consists of a graphical finite-state-machine-like language for modeling hybrid
systems, a temporal logic for modeling the requirements of hybrid systems, and
a computer procedure that verifies modeled hybrid systems against modeled requirements.
The tool HyTech is the implementation of the framework using C++ and Mathematica.\r\n\r\nMore
specifically, our hybrid-system modeling language, Hybrid Automata, is an extension
of timed automata with discrete and continuous variables whose dynamics are governed
by differential equations. Our requirement modeling language, ICTL, is a branching-time
temporal logic, and is an extension of TCTL with stop-watch variables. Our verification
procedure is a symbolic model-checking procedure that verifies linear hybrid automata
against ICTL formulas. To make HyTech more efficient and effective, we use model-checking
strategies and abstract operators that can expedite the verification process.
To enable HyTech to verify nonlinear hybrid automata, we introduce two translations
from nonlinear hybrid automata to linear hybrid automata. We have applied HyTech
to analyze more than 30 hybrid-system benchmarks. In this dissertation, we present
the application of HyTech to three nontrivial hybrid systems taken from the literature."
article_processing_charge: No
author:
- first_name: Pei
full_name: Ho, Pei
last_name: Ho
citation:
ama: Ho P. Automatic Analysis of Hybrid Systems. 1995:1-188. doi:CSD-TR95-1536
apa: Ho, P. (1995). *Automatic Analysis of Hybrid Systems*. Cornell University.
https://doi.org/CSD-TR95-1536
chicago: Ho, Pei. “Automatic Analysis of Hybrid Systems.” Cornell University, 1995.
https://doi.org/CSD-TR95-1536.
ieee: P. Ho, “Automatic Analysis of Hybrid Systems,” Cornell University, 1995.
ista: Ho P. 1995. Automatic Analysis of Hybrid Systems. Cornell University.
mla: Ho, Pei. *Automatic Analysis of Hybrid Systems*. Cornell University, 1995,
pp. 1–188, doi:CSD-TR95-1536.
short: P. Ho, Automatic Analysis of Hybrid Systems, Cornell University, 1995.
date_created: 2018-12-11T12:08:48Z
date_published: 1995-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:54Z
day: '01'
doi: CSD-TR95-1536
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 188
publication_status: published
publisher: Cornell University
publist_id: '304'
status: public
supervisor:
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000-0002-2985-7724
title: Automatic Analysis of Hybrid Systems
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '1995'
...
---
_id: '4516'
author:
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Henzinger TA. The Temporal Specification and Verification of Real-time Systems
. 1991.
apa: Henzinger, T. A. (1991). *The Temporal Specification and Verification of
Real-time Systems *. Stanford University.
chicago: Henzinger, Thomas A. “The Temporal Specification and Verification of Real-Time
Systems .” Stanford University, 1991.
ieee: T. A. Henzinger, “The Temporal Specification and Verification of Real-time
Systems ,” Stanford University, 1991.
ista: Henzinger TA. 1991. The Temporal Specification and Verification of Real-time
Systems . Stanford University.
mla: Henzinger, Thomas A. *The Temporal Specification and Verification of Real-Time
Systems *. Stanford University, 1991.
short: T.A. Henzinger, The Temporal Specification and Verification of Real-Time
Systems , Stanford University, 1991.
date_created: 2018-12-11T12:09:15Z
date_published: 1991-08-01T00:00:00Z
date_updated: 2021-01-12T07:59:23Z
day: '01'
extern: 1
main_file_link:
- open_access: '0'
url: http://mtc.epfl.ch/~tah/Publications/the_temporal_specification_and_verification_of_real-time_systems.pdf
month: '08'
publication_status: published
publisher: Stanford University
publist_id: '210'
quality_controlled: 0
status: public
title: 'The Temporal Specification and Verification of Real-time Systems '
type: dissertation
year: '1991'
...
---
_id: '4337'
author:
- first_name: Nicholas H
full_name: Nicholas Barton
id: 4880FE40-F248-11E8-B48F-1D18A9856A87
last_name: Barton
orcid: 0000-0002-8548-5240
citation:
ama: Barton NH. A hybrid zone in the alpine grasshopper Podisma pedestris. 1979.
apa: Barton, N. H. (1979). *A hybrid zone in the alpine grasshopper Podisma pedestris*.
University of East Anglia.
chicago: Barton, Nicholas H. “A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris.”
University of East Anglia, 1979.
ieee: N. H. Barton, “A hybrid zone in the alpine grasshopper Podisma pedestris,”
University of East Anglia, 1979.
ista: Barton NH. 1979. A hybrid zone in the alpine grasshopper Podisma pedestris.
University of East Anglia.
mla: Barton, Nicholas H. *A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris*.
University of East Anglia, 1979.
short: N.H. Barton, A Hybrid Zone in the Alpine Grasshopper Podisma Pedestris, University
of East Anglia, 1979.
date_created: 2018-12-11T12:08:20Z
date_published: 1979-01-01T00:00:00Z
date_updated: 2021-01-12T07:56:14Z
day: '01'
extern: 1
month: '01'
publication_status: published
publisher: University of East Anglia
publist_id: '1694'
quality_controlled: 0
status: public
title: A hybrid zone in the alpine grasshopper Podisma pedestris
type: dissertation
year: '1979'
...