Compositional Safety Logics

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 timedautomata 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 respectto properties of a basic safety logic. As the fundamentalprerequisite of the compositional technique, it is shown how logicalproperties of a parallel program may be transformed intonecessary and sufficient properties of components of the program.Finally, a set of axiomatic laws are provided useful forsimplifying formulae and complete with respect to validity andunsatisfiability