Model checking software ; 14th International SPIN Workshop, Berlin, Germany, July 1-3, 2007, Proceedings
This book presents the proceedings of the 14th International SPIN workshop on Model Checking Software, held in Berlin, Germany. The papers are organized into topical sections covering directed model checking, partial order reduction, program analysis, exploration advances, modeling and case studies, and tool demonstrations.
Discrete-Time Markov Chains : Two-Time-Scale Methods and Applications
The motivation stems from existing and emerging applications in optimization and control of complex hybrid Markovian systems in manufacturing, wireless communication, and financial engineering. Much effort in this book is devoted to designing system models arising from these applications, analyzing them via analytic and probabilistic techniques, and developing feasible computational algorithms so as to reduce the inherent complexity. This book presents results including asymptotic expansions of probability vectors, structural properties of occupation measures, exponential bounds, aggregation and decomposition and associated limit processes, and interface of discrete-time and continuous-time systems. One of the salient features is that it contains a diverse range of applications on filtering, estimation, control, optimization, and Markov decision processes, and financial engineering.
Control of Spatially Structured Random Processes and Random Fields with Applications
This book is devoted to the study and optimization of spatiotemporal stochastic processes, that is, processes which develop simultaneously in space and time under random influences. These processes are seen to occur almost everywhere when studying the global behavior of complex systems.Classical stochastic dynamic optimization forms the framework of the book. Taken as a whole, the project undertaken in the book is to establish optimality or near-optimality for Markovian policies in the control of spatiotemporal Markovian processes. The authors apply this general principle to different frameworks of Markovian systems and processes. Depending on the structure of the systems and the surroundings of the model classes the authors arrive at different levels of simplicity for the policy classes which encompass optimal or nearly optimal policies. A set of examples accompanies the theoretical findings, and these examples should demonstrate some important application areas for the theorems discussed.


