20 maja 2016 12:15
Seminaria TIBAD: Panagiotis Kouvaros 20.05 i Lidia Tendera 3.06
On Friday, 20.05, Panagiotis Kouvaros, a postdoc at Imperial College London, will give a talk on Parameterised Verification for Multi-Agent Systems. Two weeks later, on Friday, 3.06.16, Lidia Tendera from Opole University will give a talk "Quine’s Fluted Fragment is Non-elementary". Both talks will start at 12:15 in room 310. The abstracts are below.
You are all most welcome!
Friday 20th May, 12:15, room 310
Panagiotis Kouvaros, Imperial College London
Parameterised Verification for Multi-Agent Systems
Abstract. In the past ten years several methods have been put forward for the efficient model checking of multiagent systems against agent-based specifications. Yet, since the number of states is exponential in the number of agents in the system, the model checking problem remains intractable for systems of many agents. This is particularly problematic when wishing to reason about unbounded systems where the number of components is not known at design time. Systems ranging from robotic swarms to e-commerce applications constitute typical examples in which the number of participants is independent of the design process.
In this talk I will introduce a semantics that captures unbounded multiagent systems. The semantics extends interpreted systems in a parameterised setting where the number of agents is the parameter. I will then present parameterised model checking techniques for the validation of multiagent systems irrespective of the number of the agents present. Finally, I will discuss MCMAS-P, a tool realising these techniques; MCMAS-P has been applied to cache coherence protocols, mutual exclusion protocols, swarm foraging and aggregation algorithms.
----------
Friday 3rd June, 12:15, room 310
Lidia Tendera, University of Opole
Quine’s Fluted Fragment is Non-elementary
Abstract. The fluted fragment is a decidable fragment of first-order logic, originally identified by W.V. Quine, in which, roughly speaking, the order of quantification of variables matches their order of appearance as arguments to predicates. We show that the satisfiability problem for this fragment has non-elementary complexity, thus refuting an earlier published claim by W.C. Purdy that it is in NEXPTIME.
Based on a recent joint work with Ian Pratt-Hartmann and Wiesław Szwast.