×

Model checking logics for communicating sequential agents. (English) Zbl 0932.03028

Thomas, Wolfgang (ed.), Foundations of software science and computation structures. 2nd international conference, FOSSACS ’99. Held as part of the joint European conferences on Theory and practice of software, ETAPS ’99, Amsterdam, the Netherlands, March 22–28, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1578, 227-242 (1999).
Summary: We present a model checking algorithm for \({\mathcal L}_{\text{CSA}}\), a temporal logic for communicating sequential agents (CSAs) introduced by Lodaya, Ramanujam, and Thiagarajan. \({\mathcal L}_{\text{CSA}}\) contains temporal modalities indexed with a local point of view of one agent 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 modularization of \({\mathcal L}_{\text{CSA}}\) 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 be checked with standard techniques.
For the entire collection see [Zbl 0911.00045].

MSC:

03B70 Logic in computer science
03B44 Temporal logic
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite