Seminar

Thursday, 23 November 2023, Aula G (Ca’ Vignal 2).

17:00

Epistemic Ensembles

in cooperation with A. Knapp (Univ. of Augsburg) and M. Wirsing (LMU Munich)

An ensemble is formed by a collection of agents which run concurrently to accomplish (together) a certain task. For that purpose agents must collaborate in some way, for instance by explicit interaction via message passing. In this talk we present an epistemic approach where collaboration is based on the knowledge that agents have about themselves, about other agents and about their environment. Any change of knowledge caused by an action of one agent may influence the behaviour of other agents. Hence, interaction is implicit.

For specifying properties of epistemic ensembles we propose a dynamic logic style such that necessary and possible ensemble behaviours are expressed by modalities on (complex) epistemic actions. Our semantic models are labelled transition systems with ensemble actions as labels. Such transitions model two aspects, (i) the control flow of an ensemble and (ii) changes of epistemic information caused by the epistemic effect of an agent action.

Epistemic ensembles are implemented by epistemic processes, one for each ensemble agent, which are composed in parallel to form an ensemble realisations. We provide a structured operational semantics for such processes which allows us to introduce a (formal) correctness notion: An ensemble realisation is correct w. r. t. an ensemble specification if its semantics is an epistemic model of the specification. Two ensemble realisations are equivalent, if their models are epistemically bisimilar. We show that this can be checked by checking bisimilarity of their single processes in the usual sense of process algebra.