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 andCTL* 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 \emph{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.​