Since 2014
Compositional Safety Logics
BRICS Report Series
View Archive Info| Field | Value | |
| Title |
Compositional Safety Logics
|
|
| Creator |
Andersen, Jørgen H.
Larsen, Kim G. |
|
| Description |
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.
|
|
| Publisher |
Aarhus University
|
|
| Date |
1997-01-13
|
|
| Type |
info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion |
|
| Format |
application/pdf
|
|
| Identifier |
https://tidsskrift.dk/brics/article/view/18804
10.7146/brics.v4i13.18804 |
|
| Source |
BRICS Report Series; No 13 (1997): RS-13 Compositional Safety Logics
BRICS Report Series; Nr. 13 (1997): RS-13 Compositional Safety Logics 1601-5355 0909-0878 |
|
| Language |
eng
|
|
| Relation |
https://tidsskrift.dk/brics/article/view/18804/16449
|
|