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 \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.

Employs infinite iteration in reasoning on hybrid systems in algebraic version of Neighbourhood Logic Utilizes Separation Logic to reason on linked data structures Presents a wide variety of applications

Autorentext

Their extremely fruitful cooperation started in 1999. Since then, they have been involved in the conference series "Mathematics of Program Construction" and "Relational and Algebraic Methods in Computer Science", and others, which are right in the centre of their research interests. They have edited several proceedings for these series as well as special issues of the Journal of Logic and Algebraic Programming (later called Journal of Logical and Algebraic Methods in Programming), and Science of Computer Programming on these. The book is hence a coherent presentation of all this research.

Inhalt

Idempotent Left Semirings.- Tests, (Co)Domain and Modal Operators .- Iteration: Kleene and Omega Algebras.- Simple Graph Algorithms.- Partial Correctness of Imperative Programs.- Knowledge Algebra.- Two-Player Game Analysis.- Game Algebra and Predicate Transformers.- Preferences in Databases.- Purely Finite and Purely Infinite Elements.- Temporal Logics.- Algebraic Neighbourhood Logic.- General and Total Correctness.- Demonic Semantics.- Advanced Termination Analysis.- Existence of Predomain.- Alternative Axiomatisations of (Pre-)Domain.- More Results on (Pre)Codomain.- More on Modal Operators.- Kleene Modules and Related Structures.- Odds and Ends.