Compositional Safety Logics

Authors

  • Jørgen H. Andersen
  • Kim G. Larsen

DOI:

https://doi.org/10.7146/brics.v4i13.18804

Abstract

In this paper we present a generalisation of a promising compositional
model-checking technique introduced for finite-state systems by Andersen
in [And95] and extended to networks of timed
automata by Larsen et al in [LPY95a, LL95, LPY95b, KLL+97a].
In our generalized setting, programs are modelled as arbitrary
(possibly infinite-state) transition systems and verified with respect
to properties of a basic safety logic. As the fundamental
prerequisite of the compositional technique, it is shown how logical
properties of a parallel program may be transformed into
necessary and sufficient properties of components of the program.
Finally, a set of axiomatic laws are provided useful for
simplifying formulae and complete with respect to validity and
unsatisfiability.

Downloads

Published

1997-01-13

How to Cite

Andersen, J. H., & Larsen, K. G. (1997). Compositional Safety Logics. BRICS Report Series, 4(13). https://doi.org/10.7146/brics.v4i13.18804