Abstract
This chapter gives an introduction to modal logics as seen from the context of relation algebra. We illustrate this viewpoint with an example application: verification of reactive systems. In the design of safety-critical software systems formal semantics and proofs are mandatory. Whereas for functional systems (computing a certain function) usually denotational semantics and Hoare-style reasoning is employed, reactive systems (reacting to an environment) mostly are modelled in an automata-theoretic framework, with a modal or temporal logic proof system. Much of the success of these logics in the specification of reactive systems is due to their ability to express properties without explicit use of first-order variables. For example, consider a program defined by the following transition system:
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer-Verlag Wien
About this chapter
Cite this chapter
Schlingloff, H., Heinle, W. (1997). Relation Algebra and Modal Logics. In: Brink, C., Kahl, W., Schmidt, G. (eds) Relational Methods in Computer Science. Advances in Computing Sciences. Springer, Vienna. https://doi.org/10.1007/978-3-7091-6510-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-7091-6510-2_5
Publisher Name: Springer, Vienna
Print ISBN: 978-3-211-82971-4
Online ISBN: 978-3-7091-6510-2
eBook Packages: Springer Book Archive