Skip to main content Accessibility help

We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings.

Close cookie message
×
  1. Home
  2. Series
  3. Cambridge Tracts in Theoretical Computer Science

This series offers books on theoretical computer science, that part of computer science concerned with fundamental mathematical questions about computers, programs, algorithms, data, and information processing systems in general. Computers and programs are inherently mathematical objects, and an understanding of their mathematical basis is essential to the appreciation of the foundations of computer science.The series covers the complete field of theoretical computer science, including mathematical foundations of computer science, formal methods of reasoning about programs and data, and formal semantics of programs and data, including formal semantics for natural language, pictures, and sound.

  • Associate Editors: S. Abramsky, Oxford University
  • Editorial Boards: P. H. Aczel, University of Manchester, Y. Gurevich, Microsoft Research, J. V. Tucker, Swansea University

Refine search

Refine search

Content type:
Publication date:
Subject: Show more
Journals Show more
Publishers: Show more
Series: Show more
Collections: Show more

Actions for selected content:

Select all | Deselect all
  • View selected items
  • Export citations
  • Download PDF (zip)
  • Save to Kindle
  • Save to Dropbox
  • Save to Google Drive

Save Search

You can save your searches here and later view and run them again in "My saved searches".

Please provide a title, maximum of 40 characters.
Cancel
×

43 results in Cambridge Tracts in Theoretical Computer Science

Page 1 of 3

Syntax and Semantics of Petri Nets
  • Roberto Gorrieri
  • Coming soon
  • Expected online publication date:
    August 2025
    Print publication:
    31 August 2025
  • Petri nets are one of the most popular tools for modeling distributed systems. This book provides a modern look at the theory behind them, by studying three classes of nets that model (i) sequential systems, (ii) non-communicating parallel systems, and (iii) communicating parallel systems. A decidable and causality respecting behavioral equivalence is presented for each class, followed by a modal logic characterization for each equivalence. The author then introduces a suitable process algebra for the corresponding class of nets and proves that the behavioral equivalence proposed for each class is a congruence for the operator of the corresponding process algebra. Finally, an axiomatization of the behavioral congruence is proposed. The theory is introduced step by step, with ordinary-language explanations and examples provided throughout, to remain accessible to readers without specialized training in concurrency theory or formal logic. Exercises with solutions solidify understanding, and the final chapter hints at extensions of the theory.

Initial Algebras and Terminal Coalgebras
  • The Theory of Fixed Points of Functors
  • Jiří Adámek, Stefan Milius, Lawrence S. Moss
  • Published online:
    30 January 2025
    Print publication:
    06 February 2025
  • Providing an in-depth treatment of an exciting research area, this text's central topics are initial algebras and terminal coalgebras, primary objects of study in all areas of theoretical computer science connected to semantics. It contains a thorough presentation of iterative constructions, giving both classical and new results on terminal coalgebras obtained by limits of canonical chains, and initial algebras obtained by colimits. These constructions are also developed in enriched settings, especially those enriched over complete partial orders and complete metric spaces, connecting the book to topics like domain theory. Also included are an extensive treatment of set functors, and the first book-length presentation of the rational fixed point of a functor, and of lifting results which connect fixed points of set functors with fixed points of endofunctors on other categories. Representing more than fifteen years of work, this will be the leading text on the subject for years to come.

Topological Duality for Distributive Lattices
  • Theory and Applications
  • Mai Gehrke, Sam van Gool
  • Published online:
    16 February 2024
    Print publication:
    07 March 2024
  • Introducing Stone–Priestley duality theory and its applications to logic and theoretical computer science, this book equips graduate students and researchers with the theoretical background necessary for reading and understanding current research in the area. After giving a thorough introduction to the algebraic, topological, logical, and categorical aspects of the theory, the book covers two advanced applications in computer science, namely in domain theory and automata theory. These topics are at the forefront of active research seeking to unify semantic methods with more algorithmic topics in finite model theory. Frequent exercises punctuate the text, with hints and references provided.

Finite-State Techniques
  • Automata, Transducers and Bimachines
  • Stoyan Mihov, Klaus U. Schulz
  • Published online:
    29 July 2019
    Print publication:
    01 August 2019
  • Finite-state methods are the most efficient mechanisms for analysing textual and symbolic data, providing elegant solutions for an immense number of practical problems in computational linguistics and computer science. This book for graduate students and researchers gives a complete coverage of the field, starting from a conceptual introduction and building to advanced topics and applications. The central finite-state technologies are introduced with mathematical rigour, ranging from simple finite-state automata to transducers and bimachines as 'input-output' devices. Special attention is given to the rich possibilities of simplifying, transforming and combining finite-state devices. All algorithms presented are accompanied by full correctness proofs and executable source code in a new programming language, C(M), which focuses on transparency of steps and simplicity of code. Thus, by enabling readers to obtain a deep formal understanding of the subject and to put finite-state methods to real use, this book closes the gap between theory and practice.

Introduction to Coalgebra
  • Towards Mathematics of States and Observation
  • Bart Jacobs
  • Published online:
    22 December 2016
    Print publication:
    27 October 2016
  • The area of coalgebra has emerged within theoretical computer science with a unifying claim: to be the mathematics of computational dynamics. It combines ideas from the theory of dynamical systems and from the theory of state-based computation. Although still in its infancy, it is an active area of research that generates wide interest. Written by one of the founders of the field, this book acts as the first mature and accessible introduction to coalgebra. It provides clear mathematical explanations, with many examples and exercises involving deterministic and non-deterministic automata, transition systems, streams, Markov chains and weighted automata. The theory is expressed in the language of category theory, which provides the right abstraction to make the similarity and duality between algebra and coalgebra explicit, and which the reader is introduced to in a hands-on manner. The book will be useful to mathematicians and (theoretical) computer scientists and will also be of interest to mathematical physicists, biologists and economists.

Temporal Logics in Computer Science
  • Finite-State Systems
  • Stéphane Demri, Valentin Goranko, Martin Lange
  • Published online:
    13 October 2016
    Print publication:
    13 October 2016
  • This comprehensive text provides a modern and technically precise exposition of the fundamental theory and applications of temporal logics in computer science. Part I presents the basics of discrete transition systems, including constructions and behavioural equivalences. Part II examines the most important temporal logics for transition systems and Part III looks at their expressiveness and complexity. Finally, Part IV describes the main computational methods and decision procedures for model checking and model building - based on tableaux, automata and games - and discusses their relationships. The book contains a wealth of examples and exercises, as well as an extensive annotated bibliography. Thus, the book is not only a solid professional reference for researchers in the field but also a comprehensive graduate textbook that can be used for self-study as well as for teaching courses.

Modal Logic
  • Patrick Blackburn, Maarten de Rijke, Yde Venema
  • Published online:
    05 July 2014
    Print publication:
    28 June 2001
  • This is an advanced 2001 textbook on modal logic, a field which caught the attention of computer scientists in the late 1970s. Researchers in areas ranging from economics to computational linguistics have since realised its worth. The book is for novices and for more experienced readers, with two distinct tracks clearly signposted at the start of each chapter. The development is mathematical; prior acquaintance with first-order logic and its semantics is assumed, and familiarity with the basic mathematical notions of set theory is required. The authors focus on the use of modal languages as tools to analyze the properties of relational structures, including their algorithmic and algebraic aspects, and applications to issues in logic and computer science such as completeness, computability and complexity are considered. Three appendices supply basic background information and numerous exercises are provided. Ideal for anyone wanting to learn modern modal logic.

Process Algebra: Equational Theories of Communicating Processes
  • J. C. M. Baeten, T. Basten, M. A. Reniers
  • Published online:
    05 July 2014
    Print publication:
    16 December 2009
  • Process algebra is a widely accepted and much used technique in the specification and verification of parallel and distributed software systems. This book sets the standard for the field. It assembles the relevant results of most process algebras currently in use, and presents them in a unified framework and notation. The authors describe the theory underlying the development, realization and maintenance of software that occurs in parallel or distributed systems. A system can be specified in the syntax provided, and the axioms can be used to verify that a composed system has the required external behaviour. As examples, two protocols are completely specified and verified in the text: the Alternating-Bit Protocol for Data Communication, and Fischer's Protocol of Mutual Exclusion. The book serves as a reference text for researchers and graduate students in computer science, offering a complete overview of the field and referring to further literature where appropriate.

Nominal Sets
  • Names and Symmetry in Computer Science
  • Andrew M. Pitts
  • Published online:
    05 July 2013
    Print publication:
    30 May 2013
  • Nominal sets provide a promising new mathematical analysis of names in formal languages based upon symmetry, with many applications to the syntax and semantics of programming language constructs that involve binding, or localising names. Part I provides an introduction to the basic theory of nominal sets. In Part II, the author surveys some of the applications that have developed in programming language semantics (both operational and denotational), functional programming and logic programming. As the first book to give a detailed account of the theory of nominal sets, it will be welcomed by researchers and graduate students in theoretical computer science.

Mathematical Theory of Domains
  • V. Stoltenberg-Hansen, I. Lindström, E. R. Griffor
  • Published online:
    05 June 2012
    Print publication:
    22 September 1994
  • Domain theory is an established part of theoretical computer science, used in giving semantics to programming languages and logics. In mathematics and logic it has also proved to be useful in the study of algorithms. This book is devoted to providing a unified and self-contained treatment of the subject. The theory is presented in a mathematically precise manner which nevertheless is accessible to mathematicians and computer scientists alike. The authors begin with the basic theory including domain equations, various domain representations and universal domains. They then proceed to more specialized topics such as effective and power domains, models of lambda-calculus and so on. In particular, the connections with ultrametric spaces and the Kleene–Kreisel continuous functionals are made precise. Consequently the text will be useful as an introductory textbook (earlier versions have been class-tested in Uppsala, Gothenburg, Passau, Munich and Swansea), or as a general reference for professionals in computer science and logic.

Basic Proof Theory
  • 2nd edition
  • A. S. Troelstra, H. Schwichtenberg
  • Published online:
    05 June 2012
    Print publication:
    27 July 2000
  • This introduction to the basic ideas of structural proof theory contains a thorough discussion and comparison of various types of formalization of first-order logic. Examples are given of several areas of application, namely: the metamathematics of pure first-order logic (intuitionistic as well as classical); the theory of logic programming; category theory; modal logic; linear logic; first-order arithmetic and second-order logic. In each case the aim is to illustrate the methods in relatively simple situations and then apply them elsewhere in much more complex settings. There are numerous exercises throughout the text. In general, the only prerequisite is a standard course in first-order logic, making the book ideal for graduate students and beginning researchers in mathematical logic, theoretical computer science and artificial intelligence. For the new edition, many sections have been rewritten to improve clarity, new sections have been added on cut elimination, and solutions to selected exercises have been included.

Domains and Lambda-Calculi
  • Roberto M. Amadio, Pierre-Louis Curien
  • Published online:
    05 November 2011
    Print publication:
    02 July 1998
  • This book describes the mathematical aspects of the semantics of programming languages. The main goals are to provide formal tools to assess the meaning of programming constructs in both a language-independent and a machine-independent way, and to prove properties about programs, such as whether they terminate, or whether their result is a solution of the problem they are supposed to solve. In order to achieve this the authors first present, in an elementary and unified way, the theory of certain topological spaces that have proved of use in the modelling of various families of typed lambda calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is known as Domain Theory, and was founded as a subject by Scott and Plotkin. One of the main concerns is to establish links between mathematical structures and more syntactic approaches to semantics, often referred to as operational semantics, which is also described. This dual approach has the double advantage of motivating computer scientists to do some mathematics and of interesting mathematicians in unfamiliar application areas from computer science.

Information Flow
  • The Logic of Distributed Systems
  • Jon Barwise, Jerry Seligman
  • Published online:
    05 November 2011
    Print publication:
    28 July 1997
  • Information is a central topic in computer science, cognitive science and philosophy. In spite of its importance in the 'information age', there is no consensus on what information is, what makes it possible, and what it means for one medium to carry information about another. Drawing on ideas from mathematics, computer science and philosophy, this book addresses the definition and place of information in society. The authors, observing that information flow is possible only within a connected distribution system, provide a mathematically rigorous, philosophically sound foundation for a science of information. They illustrate their theory by applying it to a wide range of phenomena, from file transfer to DNA, from quantum mechanics to speech act theory.

Advanced Topics in Bisimulation and Coinduction
  • Edited by Davide Sangiorgi, Jan Rutten
  • Published online:
    05 November 2011
    Print publication:
    13 October 2011
  • Coinduction is a method for specifying and reasoning about infinite data types and automata with infinite behaviour. In recent years, it has come to play an ever more important role in the theory of computing. It is studied in many disciplines, including process theory and concurrency, modal logic and automata theory. Typically, coinductive proofs demonstrate the equivalence of two objects by constructing a suitable bisimulation relation between them. This collection of surveys is aimed at both researchers and Master's students in computer science and mathematics and deals with various aspects of bisimulation and coinduction, with an emphasis on process theory. Seven chapters cover the following topics: history, algebra and coalgebra, algorithmics, logic, higher-order languages, enhancements of the bisimulation proof method, and probabilities. Exercises are also included to help the reader master new material.

Data Refinement
  • Model-Oriented Proof Methods and their Comparison
  • Willem-Paul de Roever, Kai Engelhardt
  • Published online:
    03 May 2010
    Print publication:
    03 December 1998
  • The goal of this book is to provide a comprehensive and systematic introduction to the important and highly applicable method of data refinement and the simulation methods used for proving its correctness. The authors concentrate in the first part on the general principles needed to prove data refinement correct. They begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation. The book's second part contains a detailed survey of important methods in this field, which are carefully analysed, and shown to be either incomplete, with counterexamples to their application, or to be always applicable whenever data refinement holds. This is shown by proving, for the first time, that all these methods can be described and analysed in terms of two simple notions: forward and backward simulation. The book is self-contained, going from advanced undergraduate level and taking the reader to the state of the art in methods for proving simulation.

Algebraic Specification of Communication Protocols
  • Edited by S. Mauw, G. J. Veltink
  • Published online:
    03 May 2010
    Print publication:
    16 September 1993
  • Modern computer networks now circle the world, but the transmission of information between them depends on the many different protocols that define the behaviour of the sender and receiver. It is clear therefore, that the accurate description of these protocols is important if harmonious communication is to be maintained. In this book the authors use the formal specification language PSF to provide an unambiguous description of several communication protocols of varying levels of complexity, ranging from the alternating bit protocol to the token ring protocol. Beginners, as well as professionals in the field of communication protocols, will benefit from both the methods of specification described and the protocols discussed in this book.

Updating Logical Databases
  • Marianne Winslett
  • Published online:
    22 March 2010
    Print publication:
    26 October 1990
  • This book tackles the problems of update algorithms for databases. How can one construct and maintain a database of facts, capable of incorporating new information and getting rid of all outdated information, and yet in the process not disturb any other information in the database? The author has produced a formal method for specifying the desired change intentionally, using a 'formula-based' approach to updating needs rather than a 'model-based' technique. The complexity of the algorithms, choice of semantics and a means of enforcing integrity constraints are also discussed. The book will be of value to all involved in database research.

Hybrid Graph Theory and Network Analysis
  • Ladislav Novak, Alan Gibbons
  • Published online:
    20 March 2010
    Print publication:
    02 September 1999
  • First published in 1999, this book combines traditional graph theory with the matroidal view of graphs and throws light on mathematical aspects of network analysis. This approach is called here hybrid graph theory. This is essentially a vertex-independent view of graphs naturally leading into the domain of graphoids, a generalisation of graphs. This enables the authors to combine the advantages of both the intuitive view from graph theory and the formal mathematical tools from the theory of matroids. A large proportion of the material is either new or is interpreted from a fresh viewpoint. Hybrid graph theory has particular relevance to electrical network analysis, which was one of the earliest areas of application of graph theory. It was essentially out of developments in this area that hybrid graph theory evolved.

Programs, Recursion and Unbounded Choice
  • Wim H. Hesselink
  • Published online:
    11 March 2010
    Print publication:
    21 May 1992
  • This book is a complete account of the predicate transformation calculus semantics of sequential programs, including repetitions, recursive procedures, computational induction and unbounded nondeterminacy. Predicate transformation semantics are the best specification method for the development of correct and well-structured computer programs. The author develops this theory to a greater depth than has been achieved before, and describes it in a way that makes it readily compatible with programming rules for partial and total correctness of repetitions and recursive procedures, supplies new rules for proving incorrectness, and a stronger rule for proving that two programs satisfy the same specifications. Finally, the semantics are extended so that non-terminating programs can be specified as well. This will be essential reading for all computer scientists working in specification and verification of programs.

Design Theory and Computer Science
  • Subrata Dasgupta
  • Published online:
    10 February 2010
    Print publication:
    16 May 1991
  • The logic and methodology of design is examined in this book from the perspective of computer science. Computers provide the context for this examination both by discussion of the design process for hardware and software systems and by consideration of the role of computers in design in general. The central question posed by the author is whether or not we can construct a theory of design. This book concentrates upon the relationship between design, mathematics and science and thus its audience must include designers and software designers as well as computer scientists.

Page 1 of 3