×

Temporal logics for communicating sequential agents. I. (English) Zbl 0754.68085

Summary: We introduce a class of distributed systems called Communicating Sequential Agents (CSAs). Sound and complete axiomatizations are provided for various subclasses using a family of indexed temporal logics. Some of the important features of these logics are:
\(\bullet\) Both the formulas and the structures for the logics reflect the fact that a system is composed out of a number of participating sequential agents.
\(\bullet\) Formulas of the logics are interpreted only at local states.
\(\bullet\) An agent makes a definite assertion about another agent only if it has received — directly or indirectly — some communication from that agent supporting that assertion.

MSC:

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