Информатика и вычислительная техника
  • формат pdf
  • размер 1.79 МБ
  • добавлен 03 января 2012 г.
Bowman H., Gomez R. Concurrency Theory. Calculi and Automata for Modelling Untimed and Timed Concurrent Systems
Издательство Springer, 2006, -444 pp.

In the world we live in concurrency is the norm. For example, the human body is a massively concurrent system, comprising a huge number of cells, all simultaneously evolving and independently engaging in their individual biological processing. In addition, in the biological world, truly sequential systems rarely arise. However, they are more common when manmade artefacts are considered. In particular, computer systems are often developed from a sequential perspective. Why is this? The simple reason is that it is easier for us to think about sequential, rather than concurrent, systems. Thus, we use sequentiality as a device to simplify the design process.
However, the need for increasingly powerful, flexible and usable computer systems mitigates against simplifying sequentiality assumptions. A good example of this is the all-powerful position held by the Inteet, which is highly concurrent at many different levels of decomposition. Thus, the mode computer scientist (and indeed the mode scientist in general) is forced to think about concurrent systems and the subtle and intricate behaviour that emerges from the interaction of simultaneously evolving components.
Over a period of 25 years, or so, the field of concurrency theory has been involved in the development of a set of mathematical techniques that can help system developers to think about and build concurrent systems. These theories are the subject matter of this book.
Our motivation in writing this book was twofold. (1) We wished to synthesise into a single coherent story, a body of research that is scattered across a set of joual and conference publications. (2) We have also sought to highlight newer research (mainly undertaken by the authors) on concurrency theory models of real-time systems. The first of these aspects yields the text book style of the first three parts of the book, whereas the second has motivated the approach of the fourth part, which has more of the flavour of a research monograph.
There are other books on concurrency theory, but these have tended to have a different focus from this book. Most relevant in this respect are classic works by Milner on the Calculus of Communicating Systems (CCS) [148], Hoare on first generation Communicating Sequential Processes (CSP) [96], Roscoe on the mature CSP theory [171] and Schneider on Timed CSP [176]. However, all of these have a tighter focus than this book, being directed at specific theories. Although one point of major focus in this book is the process calculus LOTOS (which, by the way, has not previously been presented in book format), our approach is broader in scope than these earlier texts. For example, we consider both untimed and timed approaches (in the same book), we highlight the process calculus approach along with communicating finite and infinite state automata and we present a spectrum of different semantic theories, including traces, transition systems, refusals and true concurrency models. The latter of these semantic models being particularly noteworthy, because the bundle event structure true concurrency theory we consider is not as well-known as it should be.
Another difference with previous concurrency theory texts is that this book is less focused on proof systems. There are a number of reasons for this. First, proof systems are not as well behaved in LOTOS as they are in CCS and CSP; e.g. testing equivalence is not a congruence in LOTOS. Second, we would argue that the issue of finding complete proof systems has actually tued out to be less important than once seemed to be the case. This is because of the development of powerful state-space exploration methods, such as model-checking and equivalence-checking, which are not proof system dependent. As a reflection of this trend, we also consider finite and infinite state communicating automata approaches, which have recently taken a prominent place in concurrency theory, because of their amenability to formal verification. These techniques were not considered in the previous process calculus texts.
Due to the breadth of scope that we have sought in this book, by necessity, certain topics have had to be treated in less depth than would be optimum. As just discussed, one of these is the topic of proof systems. In addition, when, in a denotational style, we interpret recursive definitions semantically, we do not present the full details of the fixed point theories that we use. However, at all such points in the text, we give pointers to the required definitions and include references to complete presentations of the necessary theory.
In terms of target readership, this book is partially a textbook and partially a research monograph. It is particularly suitable for masters and doctoral level programmes with an emphasis on parallel processing, distributed systems, networks, formal methods and/or concurrency in general. We assume a basic knowledge of set theory, logic and discrete mathematics, as found in a textbook such as [86]. However, we do include a list of notation to help the reader.
The material presented here has partially grown out of a set of course notes used in an MSc-level course on formal methods taught in the Computing Laboratory at the University of Kent. Consequently, we would like to thank the students who have taken this course over a number of years. The feedback from these students has helped these notes to be refined, which has, in tu, benefited this book.

Part I Introduction
Background on Concurrency Theory
Part II Concurrency Theory – Untimed Models
Process Calculi: LOTOS
Basic Interleaved Semantic Models .
True Concurrency Models: Event Structures
Testing Theory and the Linear Time – Branching Time Spectrum
Part III Concurrency Theory – Further Untimed Notations
Beyond pbLOTOS
Comparison of LOTOS with CCS and CSP
Communicating Automata
Part IV Concurrency Theory – Timed Models
Timed Process Calculi, a LOTOS Perspective
Semantic Models for tLOTOS
Timed Communicating Automata
Timelocks in Timed Automata
Discrete Timed Automata
Похожие разделы
Смотрите также

Adamatzky A. etc. Automata-2008. Theory and Applications of Cellular Automata

  • формат pdf
  • размер 14.97 МБ
  • добавлен 01 ноября 2011 г.
Издательство Luniver Press, 2008, -636 pp. The book offers a unique collection of papers presented at the Automata-2008 workshop held in Bristol, June 12-14, 2008. The event was supported by the Engineering and Physical Sciences Research Council (EPSRC), the UK Government’s leading funding agency for research and training in engineering and the physical sciences. Automata 2008 is the 14th workshop in a series of AUTOMATA workshops established in...

Ginzburg A. Algebraic Theory of Automata

  • формат djvu
  • размер 1.89 МБ
  • добавлен 01 ноября 2011 г.
Издательство Academic Press, 1968, -173 pp. This monograph is intended to provide a graduate student and a newcomer to the field with ideas, methods, and results of algebraic theory of automata ; nevertheless, people working in the area may find the book useful, too, especially the chapters about regular expressions and the decomposition theory of Krohn and Rhodes. The book can serve as a text for a one-semester course in Automata Theory. The...

Kaynar D.K., Lynch N., Segala R., Vaandrage F. The Theory of Timed I-O Automata

  • формат pdf
  • размер 690.8 КБ
  • добавлен 01 ноября 2011 г.
Издательство Morgan & Claypool, 2006, -114 pp. This monograph presents the timed input/output automaton (TIOA) modeling framework, a basic mathematical framework to support description and analysis of timed (computing) systems. Timed systems are systems in which desirable correctness or performance properties of the system depend on the timing of events, not just on the order of their occurrence. Timed systems are employed in a wide range of...

Kobrinskii N.E., Trakhtenbrot B.A. Introduction to the Theory of Finite Automata

  • формат djvu
  • размер 2.09 МБ
  • добавлен 01 ноября 2011 г.
Издательство North Holland, 1963, -342 pp. In recent years, intensive work has been in progress at a number of centres to develop and apply various automatic digital systems for information processing. Such systems form the basis of digital computers, various control devices operating to a specified algorithm, and of models which simulate the activity of a living organism (termed robots). These automata take the form of independent special-purpo...

Mikolajczak B. Algebraic and structural automata theory

  • формат djvu
  • размер 2.16 МБ
  • добавлен 01 ноября 2011 г.
Издательство North Holland, 1991, -424 pp. The subject of research in automata theory is a design of mathematical models describing methods of information transformation in digital systems. Automata theory is especially concerned with abstract models of systems working by means of discrete signals, known as digital signals. Special emphasis has been put on digital computers, digital systems of control for technological processes, and digital sys...

Pin J.E. (ed.) Formal Properties of Finite Automata and Applications

  • формат djvu
  • размер 2.38 МБ
  • добавлен 01 ноября 2011 г.
Издательство Springer, 1989, -268 pp. The subject of the sixteenth School is the theory of finite automata and its applications. However two important parts of this theory are not treated in this volume, because they were already the subject of two earlier Spring Schools : "Automata on infinite words" (Spring School 1984) and "Automata Networks" (Spring School 1986). The proceedings have been divided into three sections. The first section is de...

Salcido A. (ed.) Cellular Automata - Simplicity Behind Complexity

  • формат pdf
  • размер 13.92 МБ
  • добавлен 29 октября 2011 г.
Издательство InTech, 2011, -580 pp. In the early 1950s, at the suggestion of Stanislaw Ulam, John Von Neumann introduced the cellular automata as simple mathematical models to investigate self-organisation and self-reproduction. Cellular automata make up a very important class of completely discrete dynamical systems. The physical environment of cellular automata is constituted of a finite-dimensional lattice, with each site having a finite numb...

Salomaa A., Wood D., Yu S. (eds.) A Half-Century of Automata Theory. Сelebration and Inspiration

  • формат djvu
  • размер 608.85 КБ
  • добавлен 01 ноября 2011 г.
Издательство World Scientific Publishing, 2001, -164 pp. In the past half century, automata theory has been established as one of the most important foundations of computer science, and its applications have spread to almost all areas of computer science. Research in automata theory and related areas has also reached a crucial point where researchers are searching for new directions. To celebrate the achievements in automata theory in the past h...

Subramanian K.G., Rangarajan K., Mukund M. (eds.) Formal Models, Languages and Applications

  • формат pdf
  • размер 16.46 МБ
  • добавлен 10 декабря 2011 г.
Издательство World Scientific, 2006, -420 pp. This volume of contributed papers commemorates the 75th birthday of Prof. Rani Siromoney, one of the foremost theoretical computer scientists in India and a leading authority on Formal Languages and Automata Theory. Over a period spanning four decades, she has made tremendous technical contributions to the field through her research. She has also inspired generations of students in Chennai with her t...

Taubner D. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets

  • формат djvu
  • размер 1.31 МБ
  • добавлен 01 ноября 2011 г.
Издательство Springer, 1989, -167 pp. There are two main approaches to a theory of concurrent distributed computations: the theory of Petri nets and the Milner/Hoare theory of CCS/CSP. They are based on different philosophies and emerged from two different classical notions of computability. The Petri net approach developed (in the early 60s) from the ideas around Turing machines and automata; it has concurrency and causality as its basic concep...