Modal Semirings and Applications

The book serves as a systematic exposition of modal semirings. Next to motivating the definitions, developing the basic calculus and discussing the most interesting examples of modal semirings, it presents a wide variety of applications. On the side of program semantics, Hoare Logic, the theory of general and partial correctness, demonic semantics and various temporal logics such as PDL, LTL and CTL* are treated. The book is situated in the general area of formal methods. Among the many approaches there, it concentrates on a strongly calculational style using algebra as its main ingredient. This field is often called algebraic logic. Its aim is to compact series of small steps of general logical inference into larger (in) equational steps. Moreover, it attempts to replace tedious model-theoretic argumentation, in particular, element-wise argumentation, by more abstract and compact reasoning. The structure of the book is as follows: Part I presents the basic theory. Part II contains applications to program semantics, graph-theoretic algorithms, Epistemic Logic, game analysis and databases with preference relations. Part III deals with infinite computations as well as their application to the above-mentioned temporal logics and Neighbourhood Logic as used in the description of hybrid systems. Part IV presents further applications to program semantics and terminations analysis. Finally, Part V contains some advanced theoretical material. Whereas Part I should be read sequentially, the chapters in the other parts are more or less independent of each other.