Springer Publishing Company, Incorporated, Berlin, Germany, 2009. 231 pp.

F.4.1 Mathematical logic - modal and temporal logic

The basic formula in action-indexed modal logic is
⟨*a*⟩*F*,
which asks at a state *s* whether there
is a successor state, reachable by an action
*a*, where the property
*F* holds.
For stochastic modal logic, the formula
⟨*a*⟩_{p} *F*
asks at a state *s*
whether there is a successor state, reachable by an action
*a* with probability at least
*p*, where
*F* holds.
One could think of a more complex formulation, such as whether there is
a path from state *s* such that,
with probability *p*,
some property is satisfied along the path, or some reward
*r* is obtainable with probability at least
*p*.
Stochastic coalgebraic logic generically allows such formulations to be
defined by a coalgebra. This compact, four-chapter monograph packs in
many mathematical details about such logics.

The first chapter contains mathematical background material that covers categories, topological spaces, σ-algebras, measure, and (sub)probabilities. The key definition of a stochastic relation (between measurable spaces) appears unheralded on page 33.

Chapter 2 is on bisimulation and modal logics. The reader who decides
to skip the first chapter and start with this one is in for a surprise,
since the treatment is kept at an abstract level and requires many of
the concepts from the introductory chapter. For example, bisimulation is
defined using morphisms of a mediating relation as a “pullback”
in a categorical setting. Section 2.3.1 on examples is of some help here,
as it deals with modal, temporal, and arrow logics as instantiations
of the author's general scheme, which unifies ordinary relations
with the stochastic ones. Also, the author always uses the most general
setting—*n*-ary modalities rather than binary ones, or fixed points
rather than just the “until” modality—which makes the text
pretty dense with notation. In Section 2.6 (an appendix) the author is
able to generalize results on behavioral equivalence (of systems) and
formula equivalence (of logics) to the setting of measurable spaces,
in a stronger way than achieved in other works.

Chapter 3 generalizes further the setting of randomized and ergodic morphisms that, according to the author, arise in economics and systems biology when dealing with the behavior of populations rather than individuals. Notions of behavioral equivalence and distributional equivalence (generalizing logical equivalence) are related.

Finally, the author arrives at stochastic coalgebraic logic, the subject of the monograph, in chapter 4. The main idea is that the modal as well as temporal operators are dealt with in one swoop, using natural transformations in the category-theoretic setting, and the coalgebra handles ordinary and stochastic relations in a uniform functorial way.

The treatment is mathematical throughout, with the author pointing out the key concepts used in proofs. This book may be a good reference for theoretical researchers interested in the mathematical underpinnings of this area. However, for the more modest researcher who is trying to understand, for example, the theory behind the verification of stochastic systems, I would recommend Panangaden's book [1], since it covers background material at a much gentler pace. For the researcher who wants to understand how model-checking stochastic systems work, there is a nice chapter in Baier and Katoen's book [2], at a tutorial level.

[1] Panangaden, P.
*Labelled Markov processes*. Imperial College Press, London, UK, 2009.

[2] Baier, C.; Katoen, J-.P.
*Principles of model checking*.
MIT Press, Cambridge, MA, 2008.