Intelligent agents in safety critical systems
In recent years intelligent agents have been the focus of much attention from the Artificial Intelligence
(AI) and many other communities. In AI research, agent-based systems technology has emerged as a
new paradigm for conceptualizing, designing, and implementing sophisticated software systems. Furthermore,
there has been a move of these systems into safety-critical domains including healthcare,
emergency scenarios, and disaster recovery. While agents provide great bene ts in developing many
complex software applications (e.g., systems that have multiple components, distributed over networks,
exhibit dynamic changes, and require autonomous behaviour), they also present new challenges to application
developers, namely verifying requirements and ensuring functional correctness. These problems
become even more challenging in the case of multi-agent systems (MASs), where agents exchange information
via messages. Systematic, formal approaches to their specification and verification can allow
addressing these problems.
Intelligent context-aware systems
It is widely acknowledged that computer systems are becoming increasingly nomadic and pervasive.
The vision of this next generation technology intends to provide invisible computing environments so
that a user can utilize services at any time and everywhere. In these systems information can be
collected by using tiny resource-bounded devices, such as, e.g., PDAs, smart phones, and wireless sensor
nodes. In recent years much research in pervasive computing has been focused on incorporation of
context-awareness features into pervasive applications. There is an extensive body of work in adapting
the Semantic Web technologies to model context-aware systems. In the pursuit
of making context-aware system much more useful we need to make its various devises communicate
with each other and with the surrounding environment in a cooperative manner. In achieving this goal,
agent-based techniques can be seen as a promising approach for developing context-aware applications
in complex domains. To develop smarter and reliable application of contextaware systems, we need a
rigorous study not only on formal representation of such systems but also their formal specification and
PhD thesis abstract:
presents frameworks for the modelling and verification of resource-bounded
reasoning agents. The resources considered include the time, memory, and communication
bandwidth required by agents to achieve a goal. The scalability and expressiveness
of standard model checking techniques is investigated using two typical multiagent
reasoning problems which can be easily parameterised to increase or decrease
the problem size. Both a complexity analysis and experimental results suggest that
reasonably sized problem instances are unlikely to be tractable for a standard model
checker without steps to reduce the branching factor of the state space. We propose
two approaches to address this problem: the use of abstract specifications to model the
behaviour of some of the agents in the system, and exploiting information about the
reasoning strategy adopted by the agents. Abstract specifications are given as Linear
Temporal Logic (LTL) formulae which describe the external behaviour of the agents,
allowing their temporal behaviour to be compactly modelled. Conversely, reasoning
strategies allow the detailed specification of the ordering of steps in the agent's reasoning
process. Both approaches have been combined in an automated verification tool
TVRBA for rule-based multi-agent systems which allows the designer to specify information
about agents' interaction, behaviour, and execution strategy at different levels
of abstraction. The TVRBA tool generates an encoding of the system for the Maude
LTL model checker, allowing properties of the system to be verified. The scalability of
the new approach is illustrated using three case studies.
In our research we use Maude, NuSMV, and Mocha model checker.
Wireless Sensor Networks
Teaching and duties:
- IFAAMAS Student Session Program Committee member at EASSS'10
- IFAAMAS Student Session Program Committee member at EASSS'09
- IFAAMAS Student Session Program Committee member at EASSS'08
- 2009-10 Spring
G64DBS Tutor DBMS
- 2008-09 Autumn
G64DBS Tutor DBMS
- 2007-08 Spring
G51DBS Tutor DBMS
- Automated verification of resource requirements in multi-agent systems using abstraction, MoChArt'10, July 2010, Atlanta, Georgia, USA.
- Verifying resource requirements for distributed rule-based systems ( pdf ), RuleML'08, October 2008, Orlando, USA.
- Verification of resource bounded multi-agent systems ( pdf ), ARW'08, July 2008, University of Birmingham, UK.
- Verifying resource requirements of distributed rule-based reasoners ( pdf), EASSS'08, May 2008, New University of Lisbon, Portugal.
- Verification of Resource Requirements of Distributed Reasoning Agents ( pdf), QAPL'08, March 2008, Budapest, Hungary.
- MoChArt'10 , July 11, 2010, Atlanta, Georgia, USA.
- FAUSt'09 , September 14-15, 2009, Imperial College, London, U.K.
- RuleML-2008 , October 30-31, 2008, Orlando, Florida, USA.
- British Logic Colloquium 2008 , September 4-6, 2008, Nottingham, U.K.
- ESSLLI-2008 , August 4-15, 2008 , Hamburg, Germany.
- ARW'08 , July 30-31, 2008, University of Birmingham, UK.
- AAMAS'08 , May 12-18, 2008, Estoril,Portugal.
- EASSS'08 , May 5-9, 2008,Portugal.
- QAPL'08 ,March 29-30, 2008,Budapest, Hungary.
- EASSS'07 ,August 26-31, 2007, Durham, U.K
- MALLOW'07 , September 2-7, 2007, Durham, U.K
- ESSLLI'07 , August 6-17, 2007, Trinity College, Dublin, Ireland.
This file is maintained by Abdur Rakib Last modified: 30th-June-2011