TY - JOUR AU - Andersen, Jørgen H. AU - Larsen, Kim G. PY - 1997/01/13 Y2 - 2024/03/29 TI - Compositional Safety Logics JF - BRICS Report Series JA - BRICS VL - 4 IS - 13 SE - Articles DO - 10.7146/brics.v4i13.18804 UR - https://tidsskrift.dk/brics/article/view/18804 SP - AB - In this paper we present a generalisation of a promising compositional<br /> model-checking technique introduced for finite-state systems by Andersen<br /> in [And95] and extended to networks of timed<br />automata by Larsen et al in [LPY95a, LL95, LPY95b, KLL+97a].<br />In our generalized setting, programs are modelled as arbitrary<br />(possibly infinite-state) transition systems and verified with respect<br />to properties of a basic safety logic. As the fundamental<br />prerequisite of the compositional technique, it is shown how logical<br />properties of a parallel program may be transformed into<br />necessary and sufficient properties of components of the program.<br />Finally, a set of axiomatic laws are provided useful for<br />simplifying formulae and complete with respect to validity and<br />unsatisfiability. ER -