Członkowie Zespołu

	prof. dr hab. inż. Wojciech Penczek - kierownik zespołu
	doc. dr hab. Stanisław Ambroszkiewicz
	mgr Waldemar Bartyna
	dr hab. Marek Bednarczyk
	prof. dr hab. Piotr Dembiński
	doc. dr hab. Barbara Dunin-Kęplicz
	mgr Marek Faderewski
	mgr Marek Gawkowski
	mgr Michał Knapik
	mgr Daniel Kocieliński
	prof. dr hab. Antoni Mazurkiewicz
	dr inż. Maciej Szreter

	VERICS
	VERICS: prototypowy system weryfikacyjny (do zastosowań badawczych - na razie) do weryfikacji systemów rozproszonych specyfikowanych przez automaty czasowe lub w języku specyfikacji ESTELLE. Obecna wersja systemu umożliwia weryfikację własności osiągalności. Więcej o VERICS.
	enTish
	enTish - prototyp implementujący ideę Web services. System jest dostępny poprzez www na stronie http://www.ipipan.waw.pl/mas/.

Tematyka badawcza
Działalność i zainteresowania członków tej grupy koncentrują się wokół następujących tematów: modele systemów rozproszonych, logiki temporalne dla systemów współbieżnych, modelowanie wiedzy i przekonań, automatyczna weryfikacja i weryfikacja modelowa systemów współbieżnych, projektowanie i analiza protokołów kryptograficznych, dzielenie się informacjami poufnymi, systemy wieloagentowe, programowanie sieciowe, wirtualne organizacje agentowe.

W szczególności, badania nad systemami wieloagentowymi koncentrują się na architekturze składowych, na językach komunikacji i specyfikacji i ich implementacji, na językach dla specyfikacji i analizy systemów wieloagentowych, na metodach efektywnej weryfikacji protokołów komunikacyjnych, oraz na integracji wielofunkcyjnych i wielowęzłowych systemów agentowych. W ramach podstaw systemów wieloagentowych prowadzone są badania nad lokalnymi obliczeniami w grafach, w szczególności problemami elekcji, numeracji i negocjacji.

Wiodącymi badaczami w tym zakresie są: S. Ambroszkiewicz, M. Bednarczyk, P. Dembiński, W. Drabent, B. Dunin-Kęplicz, B. Konikowska, A. Mazurkiewicz, E. Ochmański, W. Penczek, M. Srebrny, A. Tarlecki, J. Winkowski.