非表示:
キーワード:
-
要旨:
In this paper we show that states, transitions and behavior of
concurrent systems can often be modeled as sheaves over a
suitable topological space (where the topology expresses how the
interacting systems share the information). This allows us to use
results from categorical logic (and in particular geometric
logic) to describe which type of properties are transferred, if
valid locally in all component systems, also at a global level,
to the system obtained by interconnecting the individual systems.
The main area of application is to modular verification of
complex systems.
We illustrate the ideas by means of an example involving
a family of interacting controllers for trains on a rail track.
