KIT | KIT-Bibliothek | Impressum | Datenschutz

Model checking gossip modalities

Huhn, Michaela; Niebert, Peter; Wallner, Frank


We present a model checking technique for LRT, a
temporal logic for communicating sequential agents (CSAs)
introduced by Lodaya, Ramanujam, and Thiagarajan. LRT contains
temporal modalities indexed with a local point of view of one
and allows to refer to properties of other agents according to
the latest gossip which is related to local knowledge.

The model checking procedure relies on a modularisation of LRT
into temporal and gossip modalities. We introduce a hierarchy
of formulae and a
corresponding hierarchy of equivalences, which allows to
compute for each formula and finite state distributed system a
finite multi modal Kripke structure, on which the formula can
checked with standard techniques.

Volltext §
DOI: 10.5445/IR/176598
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Rechnerentwurf und Fehlertoleranz (IRF)
Publikationstyp Forschungsbericht/Preprint
Publikationsjahr 1998
Sprache Englisch
Identifikator ISSN: 1432-7864
KITopen-ID: 176598
Verlag Universität Karlsruhe (TH)
Umfang 22 S.
Serie Interner Bericht. Universität Karlsruhe, Fakultät für Informatik ; 1998, 21
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page